Hoare Logic
COMP2111 Lecture 4b Session 1, 2013
Hoare Logic
Kai Engelhardt
Revision: 1.1
Hoare Logic
A Toy Language Syntax
Let us add assignments and guards as basic statements, and some form of loops (or recursion) to our imperative, sequential toy language. P Expr BoolExpr P ::= x := e | P ; P | P + P | | P e ::= 0 | 1 | . . . | x | . . . | e + e | e e | . . . ::= true | | | . . . | e < e | . . .
The above denitions are geared towards simplicity. When programming, we tend to use more familiar constructs such as while do P od for (; P ) ; and if then P else Q for (; P ) + (; Q ).
Hoare Logic
The Types of Semantic Functions
We introduce a family of functions from syntactic entities (programs, arithmetic expressions, and Boolean expressions) to semantic entities. [[.]] : P P( ) E [[.]] : Expr V B [[.]] : BoolExpr P()
Hoare Logic
A Denotational Semantics for P
Let s , t , x Var , e , f Expr , , BoolExpr , and P , Q P . Dene Q 0 = true and Q i +1 = Q i ; Q , for i N. (s , t ) [[x := e ]] i t = s [x E [[e ]]s ] (s , t ) [[P ; Q ]] i u ((s , u ) [[P ]] (u , t ) [[Q ]]) [[P + Q ]] = [[P ]] [[Q ]] (s , t ) [[]] i t = s s B [[]] [[P ]] =
def def
[[P i ]]
i N
where f [a b ] denotes the function that is the same as f , except for its value for the argument a, which is b .
Hoare Logic
Denotational semantics for Expr and BoolExpr
E [[0]]s = 0(I) E [[x ]]s = s (x ) E [[e f ]]s = E [[e ]]s (I) E [[f ]]s B [[true]] = B [[ ]] = B [[]] B [[ ]]
def def def def
def
E [[1]]s = 1(I) E [[e + f ]]s = E [[e ]]s +(I) E [[f ]]s
def def
def
B [[]] = \ B [[]] s B [[e < f ]] i E [[e ]]s <(I) E [[f ]]s
In the above, Ive decorated some entities on the RHS with (I) to indicate that they are semantic objects rather than syntax even though they look the same as some syntactic entities on the LHS. For instance, the symbol on the left is part of the alphabet to form arithmetic expressions, and the symbol (I) represents the multiplication function known from maths.
5
Hoare Logic
Reasoning about sequential programs
Predicates on states suce to express interesting properties of sequential programs. Hoare logic allows to formally derive properties from the program text. The Hoare triple {} P { } means: If program P is started in an initial state satisfying precondition and P terminates then the nal state satises postcondition . Example: {y = 22} x := y 17 {x = 5}
Hoare Logic
Syntax vs Semantics
On the syntactic level, we may axiomatize Hoare logic by giving a set of rules and axioms characterizing Hoare triples. On the semantic level, we may dene mathematically, what it means for a Hoare triple to be valid.
Hoare Logic
Axioms and Rules
The assignment axiom: {[e /x ]} x := e {} where [e /x ] is with x substituted by e e.g. (x = 5)[y 17 /x ] is y 17 = 5 The guard axiom: { } { }
8
ass
grd
Hoare Logic
Axioms and Rules contd
The sequential composition rule: {} P { } , { } Q {} {} P ; Q {} The choice rule: {} P { } , {} Q { } {} P + Q { } The while rule: { } P { } { } while do P od { } The consequence rule: , {} S { } , { } S { } cons loop choice seq
Hoare Logic
Trivial Example Proof
{y 17 = 5} x := y 17 {x = 5} {y = 22} x := y 17 {x = 5}
by ass by cons, math, (1)
(1) (2)
where math is used to justify y = 22 y 17 = 5.
10
Hoare Logic
Backing up with Semantics
To see whether our axiom and rules are any good, we need to give a formal interpretation to Hoare triples. {} P { } is valid if
the relational image of through P is contained in : { : B [[]] ((, ) [[P ]]) } B[[ ]]
11
Hoare Logic
Backing up with Semantics
To see whether our axiom and rules are any good, we need to give a formal interpretation to Hoare triples. {} P { } is valid if
the relational image of through P is contained in : { : B [[]] ((, ) [[P ]]) } B[[ ]]
12
Hoare Logic
Backing up with Semantics
To see whether our axiom and rules are any good, we need to give a formal interpretation to Hoare triples. {} P { } is valid if
the relational image of through P is contained in : { : B [[]] ((, ) [[P ]]) } B[[ ]]
13
Hoare Logic
Backing up with Semantics
To see whether our axiom and rules are any good, we need to give a formal interpretation to Hoare triples. {} P { } is valid if
the relational image of through P is contained in : { : B [[]] ((, ) [[P ]]) } B[[ ]]
14
Hoare Logic
Soundness and Completeness
Our proof system is sound (w.r.t. the semantics hinted at) because one can deduce only valid Hoare triples with it. Our proof system is complete (w.r.t. the semantics hinted at) if one can deduce all valid Hoare triples with it.
NB: As soon as we have (Peano) arithmetic over integers available in our assertion language, our system can hardly be complete. All one may hope for is relative completeness in the sense of Cook, i.e., completeness using an oracle for theorems from arithmetic. All this should be taught but isnt.
15
