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 antecedent) 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
•
There are 5 rules, one for each kind of statement, and a rule of consequence.
• •
The rule for assignment is an axiom. {Qx→E }x:=E{Q}
The Assignment Rule
S ::= x := E | S;S | if B then S else S | while B do S end
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
Assignment Examples
{Qx→E }x:=E{Q}
Example:
{ x – 3 > 0 } x := x – 3 { x > 0}
{ x > 3 } x := x – 3 { x > 0} {0<=n and 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 6
Understanding Hoare Triples
{ ??? } z:=z+1 {z<=n} { a>b} a:=a–b { ??? }
CSI 3120, Axiomatic Semantics, page 7
Consequence and Sequence Rules
{ P } S { Q } P’ ⇒ P Q ⇒ Q’ { P’ } S { Q’ }
• The postcondition can always be weakened and the precondition can always be strengthened.
{P1 }S1 {P2 } {P2 }S2 {P3 } {P1 }S1 ;S2 {P3 }
CSI 3120, Axiomatic Semantics, page 8
The Conditional Statement Rule
{BandP}S1 {Q} {(notB)andP}S2 {Q} {P}ifBthenS1elseS2 {Q}
Example:
{x>0and?}S1 {y>0} {(not(x>0))and?}S2 {y>0}
::
{ ? } if x>0 then y:=y-1 else y:=y+1 { y > 0 }
CSI 3120, Axiomatic Semantics, page 9
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.
CSI 3120, Axiomatic Semantics, page 10
{ n >= 0 }
count := 0;
fact := 1;
while count <> n do
Example: Factorial
count := count+1;
fact := fact * count end
{ fact = n! }
CSI 3120, Axiomatic Semantics, page 11