MES3033 Formal Methods
Hoare logic in
formal methodsGroup 3
Dr. Hafizul Fahri Bin Hanafi
Team
Amzar Lukman Zairie
1. Introduction
2. Definition
Today's 3. Type of Hoare's Logic
4. Advantages Hoare Logic
Agenda 5. Disadvantages Hoare
Logic
6. Conclusion
1. Introduction
In the modern information age, computer system
accuracy is crucial. Manual inspection of
complicated software is error-prone and costly.
There are tools that look at specific software system
executions in an effort to find design mistakes.
However, using Hoare logic for verifying the
correctness of computer programs is laborious.
Hoare Logic in Formal Method
2. Definition
2.1 Axiom
2.2 Rules
2. Definition
Hoare logic is one of the most used formal methods
for demonstrating soundness. Each programming
language has its own Hoare logic, which can be a
time-consuming process. We argue that and are
expressions in the assertion language and P is a
programme phrase in the programming language.
2.1 Axiom
{false} S{q} for any program “S” and any
postconditions “q”
{p} S{true} for any program “S” and any
precondition “p”
1
2.2 Rules
Assignment Statement Rule
2
Sequence Rule
3
Conditional Rule
2.2 Rules
4 5
Iteration Rule
Alternation Rule
6
Consequence Rule
Hoare Logic in Formal Methods
3. type of hoare's
logic
3.1 Relational Hoare Logic (RHL)
3.2 Probabilistic Hoare Logic
3.3 Probabilistic Relational Hoare Logic
3.1 Relational hoare logic rhl
Relational Hoare Logic (RHL) is a variant of traditional Hoare logic.
RHL compares two instructions (or programmes) based on whether
they map a specific pre-relation into a specific post-relation. The
central concept in RHL is what we may call a Hoare quadruple.
3.2 Probabilistic Hoare Logic
Probabilistic hoare logic is a formal system for reasoning about the
correctness of probabilistic programs. It is based on Hoare logic,
which is used to reason about imperative programs. Probabilistic
program is a sequence of statements that may include probabilities
such as flips of a coin or random numbers.
3.3 probabilistic relational hoare
triple
Probabilistic relational Hoare logic is a variant of probabilistic Hoare
logic that is used to reason about the correctness of probabilistic
programs that manipulate relational data.
Probabilistic Hoare triple is a statement of the form:\r {P} C {Q} where P
is a precondition, C is a probabilistic program, and Q is a
postcondition. Probabilistic programs can be used to reason about
correctness of algorithms that manipulate relational data.
Hoare Logic in Formal Methods
4. advantages
5. disadvantages
advantages
Precision Tool Support
Understandability
High-Assurance
Widely Accepted
disadvantages
Difficulty
Lack of Flexibility
Time-Consuming
Resource-intensive
Limited Applicability
Hoare Logic in Formal Methods
6. conclusion
CONCLUSION
Hoare logic is a powerful and widely used method for formally verifying the correctness of
computer programs. Its rules provide a precise and rigorous way to specify the behavior of
a program, and can be used to prove that a program will always produce the desired
output for a given input. Hoare logic uses a set of rules, known as the Hoare rules or Hoare
triples.
Assignment Statement Rule
Interpretation: If one “q” wants to hold after
execution of the assignment statement, when “S”
is replaced by “E(S)” , then “q(E(S))” must hold
before execution of the assignment; hence “p” the
precondition must imply “q(E(S))” .
Sequence Rule
The first program statement in a sequence must be
executed and its intermediate postcondition must be
satisfied before the second program statement can be
executed, and the postcondition of the sequence of
program statements must be satisfied after the
second program statement has been executed.
Conditional Rule
If the condition "b" of an if-then-else statement is
true, then the then-branch "S1" must be executed
and the postcondition "Q" must be satisfied.
If the condition "b" of an if-then-else statement is
false, then the else-branch "S2" must be executed
and the postcondition "Q" must also be satisfied.
Alternation Rule
The body of a while loop must be executed as long as
the condition of the while loop is true, and the
postcondition of the while loop must be satisfied when
the condition of the while loop is false.
Iteration Rule
Interpretation: The first and second premises create an
inductive argument that the predicate "inv" is true regardless of
how many times it is repeated. The third premise is that the
postcondition must logically follow from the combination of the
predicate "inv" and the negation of the loop condition upon
termination of the loop. An invariant assertion is the predicate
"inv". It must be selected so that it is both weak enough to fulfil
the first premise and strong enough to satisfy the third premise
(and the second).
Consequence Rule
If a statement "P" implies another statement "Q", and if
the statement "P" is known to be true, then the
statement "Q" must also be true.
THANKS FOR HEARING
OUR PRESENTATION
