Axiomatic Semantics
• Reasoning about imperative programs using Mathematical Logic
• Formulashavetheform{P}S{Q}whereSisa program and P and Q are formulas of predicate logic, called assertions.
• P is a precondition and Q is a postcondition.
• Q expresses a property that should hold about the
program. It often expresses program correctness.
• For example:
{ n >= 0 } factorial(n) { fact = n! }
{ x > 10 } sum = 2 * x + 1 { sum > 1 }
CSI 3120, Axiomatic Semantics, page 1
Programs and Assertions
• Grammars for assertions, booleans, expressions, and program statements:
P ::= B | P and P | P or P | not P | P => P
B ::= true | false | E = E | E <> E | E > E | E < E |
E <= E | E >= E | …
E ::= x | n | E + E | E – E | E * E | E / E | E! | … S ::= x := E | S;S | if B then S else S |
while B do S end
• Note that x represents a variable from an infinite set, and n represents a number. We assume that all numbers are integers.
• Note that arithmetic and boolean expressions have no side effects.
CSI 3120, Axiomatic Semantics, page 2
Weakest Precondition
• The weakest precondition is a precondition that is the least restrictive (contains the least amount of information) but still guarantees that the postcondition will be true.
• Example:
{ x > 10 } sum := 2 * x + 1 { sum > 1 }
• x > 10 is not the weakest precondition. Other preconditions that make the formula true include x > 50, x>1000,x>0. Thelastoneistheweakest precondition.
{ x > 0 } sum := 2 * x + 1 { sum > 1 }
CSI 3120, Axiomatic Semantics, page 3
Hoare Logic
• Axiomatic Semantics is also called Hoare Logic (developed by Hoare, 1969). { P } S { Q } is often called a Hoare triple.
• Reasoning is done using inference rules, of the form A1 A2 …An
A
• If A1, A2, … An are true, then A is also true.
• A1, A2, … An are premises (or antecedents) and A is the conclusion (or consequent)
• An axiom is a logical statement that is always true (an inference rule with only a conclusion and no premises).
CSI 3120, Axiomatic Semantics, page 4
•
The Assignment Rule
There are 5 rules, one for each kind of statement, and a rule of consequence.
S ::= x := E | S;S | if B then S else S | while B do S end
The rule for assignment is an axiom. {Qx®E }x:=E{Q}
Q x®E denotes substitution; it is the notation used in this chapter for [E/x]Q, which means that we replace all occurrences of x in Q with E.
• •
CSI 3120, Axiomatic Semantics, page 5
More Assignment Examples
{Qx®E }x:=E{Q}
Example:
{ x – 3 > 0 } x := x – 3 { x > 0}
{ x > 3 } x := x – 3 { x > 0} {n>0}
{0>=0 and 0<=n and n>0} x := 0
{x>=0 and x<=n and n>0}
CSI 3120, Axiomatic Semantics, page 8
Understanding Hoare Triples
{ ??? } z:=z+1 {z<=n} { a>b} a:=a–b { ??? }
CSI 3120, Axiomatic Semantics, page 9
Rule of Consequence
{ P } S { Q } P’ Þ P Q Þ Q’ { P’ } S { Q’ }
• The postcondition can always be weakened and the precondition can always be strengthened.
• Example:
{ x > 3 } x := x-3 { x > 0 } x > 5 Þ x > 3 x > 0 Þ x > 0
{ x > 5 } x := x-3 { x > 0 }
CSI 3120, Axiomatic Semantics, page 10
Sequences
{P1 }S1 {P2 } {P2 }S2 {P3 }
{P1 }S1 ;S2 {P3 }
• Example: Find the weakest precondition.
{?} y:=3*x+1; x:=y+3 {x<10}
{(3*x+1)+3<10} y:=3*x+1 {y+3<10} {y+3<10} x:=y+3 {x<10}
{(3*x+1)+3<10}y:=3*x+1; x:=y+3{x<10}
• Equivalently:
{x<2} y:=3*x+1 {y<7} {y<7} x:=y+3 {x<10}
{x<2}y:=3*x+1; x:=y+3{x<10}
CSI 3120, Axiomatic Semantics, page 11
The Conditional Statement Rule
{BandP}S1 {Q} {(notB)andP}S2 {Q} {P}ifBthenS1elseS2 {Q}
• Given an “if” statement and a postcondition, a strategy for finding a precondition and a proof is:
– Find preconditions P1 and P2 for the “then” and “else” branches (using Q as the postcondition):
{P1 }S1 {Q} {P2 }S2 {Q}
– Find an assertion P such that (B and P) Þ P1 and ((not B) and P) Þ P2. For example, use the weakest precondition:
P o (B Þ P1) and ((not B) Þ P2)
CSI 3120, Axiomatic Semantics, page 12
Example
::
{ x>0 and P } y:=y-1 { y>0 } { (not (x>0)) and P } y:=y+1 { y>0 } { P } if x>0 then y:=y-1 else y:=y+1 { y > 0 }
One solution is the weakest precondition: P o (x>0 Þ y>1) and ((not(x>0)) Þ y > -1)
Another solution is y>1.
Complete the proof with the Assignment and Consequence rules
Complete the proof with the Assignment and Consequence rules
CSI 3120, Axiomatic Semantics, page 13
The Complete Proof
LetPw o(x>0Þy>1)and((not(x>0))Þy>-1)
1. { y > 1 } y := y-1 { y > 0 }
2. (x > 0 and Pw) Þ (y > 1)
3. (y > 0) Þ (y > 0) 4.{x>0andPw }y:=y-1{y>0} 5. { y > -1 } y := y+1 { y > 0}
6. (not (x > 0)) and Pw Þ y > -1 7.{(not(x>0))andPw }y:=y+1{y>0}
by Assignment Rule by arithmetic/logic by logic
byConsequenceRule(from1,2,3) by Assignment Rule
by arithmetic/logic
by Consequence Rule (from 5,6,3) 8.{Pw }ifx>0theny:=y-1elsey:=y+1{y>0}
by If Rule (from 4,7)
CSI 3120, Axiomatic Semantics, page 14
The While Rule
{ I and B } S { I }
{ I } while B do S end { I and (not B) }
• I is a loop invariant. It expresses a relationship between the values of the variables in the loop. The values change, but the relationship stays the same.
• Let Q be the postcondition of the while loop. Let P be the weakest precondition of the loop body S. Then the proof usually has the form:
{ P} S { I } (I and B) Þ P I Þ I
{ I and B } S { I }
{ I } while B do S end { I and (not B) } I Þ I I and (not B) Þ Q { I } while B do S end { Q }
CSI 3120, Axiomatic Semantics, page 15
S1 : S2 : S3 :
Example: Factorial
{ n >= 0 }
count := 0;
fact := 1;
while count <> n do
S4 : count := count+1; S5 : fact := fact * count end
{ fact = n! }
{P1}S1 {P2 } n>=0ÞP1 P2ÞP2 {n>=0}S1 {P2 } {P2 }S2 {I}
{P1 }S1 ;S2 {I} {I}S3 {fact=n!} {n>=0}S1 ;S2 ;S3 {fact=n!}
CSI 3120, Axiomatic Semantics, page 16
Proving Correctness of Factorial
{P1}S1 {P2 } n>=0ÞP1 P2ÞP2 {n>=0}S1 {P2 } {P2 }S2 {I}
{P1 }S1 ;S2 {I} {I}S3 {fact=n!} {n>=0}S1 ;S2 ;S3 {fact=n!}
1. FindaninvariantIofthewhileloopS3.
2. Find the weakest precondition P2 of { P2 } S2 { I } by
applying the assignment rule.
3. Find the weakest precondition P1 of { P1 } S1 { P2 } by applying the assignment rule.
4. Makesurethatn>=0ÞP1.
CSI 3120, Axiomatic Semantics, page 17
Proving{I}S3 {fact=n!}
{P4 }S4 {P5 } (IandB)ÞP4 P5 ÞP5 {IandB}S4 {P5 }
{P5 } S5 {I} {I}whileBdoS4 ;S5end{Iand(notB) } IÞI (Iand(notB))Þfact=n!
{IandB}S4 ;S5 {I}
{I}S3:whileBdoS4 ;S5end{fact=n!} Note that B is (count <> n).
5. Find the weakest precondition P5 in { P5 } S5 { I } by applying the assignment rule.
6. Find the weakest precondition P4 in { P4 } S4 { P5 } by applying the assignment rule.
7. Make sure that I is strong enough to prove (I and (not (count <> n))) Þ fact = n!
8. Make sure that I is strong enough to prove (I and count <> n) Þ P4 CSI 3120, Axiomatic Semantics, page 18
The Complete Proof (1)
1. { 1 = 0! } count := 0 {1 = count! }
2. (n >= 0) Þ (1 = 0!)
3. (1 = count!) Þ (1 = count!)
4. { n >= 0 } count := 0 { 1 = count! } 5.{1=count!}fact:=1{fact=count!} byAssignmentRule 6.{n>=0}S1 ;S2 {fact=count!} bySequenceRule(from4,5) 7. { fact*(count+1)=(count+1)! } count := count + 1 { fact*count=count! }
by Assignment Rule 8. (fact = count!) and (count <> n) Þ (fact*(count+1)=(count+1)! )
by arithmetic/logic 9. (fact*count=count!) Þ (fact*count=count!) by logic
10. {(fact = count!) and (count <> n) } count := count + 1 { fact*count=count! }
by Consequence Rule (from 7,8.9)
by Assignment Rule by arithmetic/logic by logic
by Consequence Rule (from 1,2,3)
CSI 3120, Axiomatic Semantics, page 19
The Complete Proof (2)
11. { fact*count = count! } fact := fact * count { fact = count!}
by Assignment Rule
12.{(fact=count!)and(count<>n)}S4 ;S5 {fact=count!}
by Sequence Rule (from 10,11)
13.{(fact=count!)}whileBdoS4 ;S5 end
{ (fact = count!) and (not (count <> n)) }
by While Rule (from 12) 14. (fact = count!) Þ (fact = count!) by logic
15. (fact = count!) and (not (count <> n)) Þ fact = n!
by logic/arithmetic
16.{(fact=count!)}whileBdoS4 ;S5 end{fact=n!) }
by Consequence rule (from 13,14,15)
17.{n>=0}S1 ;S2 ;S3 {fact=n!} bySequenceRule(from6,16) CSI 3120, Axiomatic Semantics, page 20
Infinite Loops and Hoare Triples
{n>=0} {true} count := 0;
fact := 1;
while count <> n do
count := count+1;
fact := fact * count end
{ fact = n! }
• Note that if we replace the precondition with “true”, this Hoare triple is provable also.
• But if n < 0, the loop never terminates.
• Themeaningof{P}S{Q}isthatwheneverPholdsbefore
execution, if S terminates, then Q holds. This is called partial correctness.
CSI 3120, Axiomatic Semantics, page 21
{ n >= 0 }
count := 0;
fact := 1;
while count <> n do
Proving Termination
count := count+1;
fact := fact * count end
{ fact = n! }
• If the precondition holds, then the loop always terminates, because the value of the expression (n-count) goes down to 0.
• We can add termination to proofs of Hoare triples, but that is beyond the scope of this chapter.
• The meaning of { P } S { Q } becomes: whenever P holds before execution, then Q holds after, and S always terminates. This is called total correctness.
CSI 3120, Axiomatic Semantics, page 22