Axioms
assignment --
{ Q [x:=e] } x = e { Q }
composition --
{ P } S1 { R } /\ { R } S2 { Q } => { P } S1;S2 { Q }
conditional --
{ P /\ b } S { Q } => { P } if (b) S { Q }
iteration --
{ I /\ b } S { I } => { I } while (b) S { I /\ \neg b }
Consequence rules
P -> R /\ { R } S { Q } => { P } S { Q }
R -> Q /\ { P } S { R } => { P } S { Q }
Procedural abstraction
m(x) |-> S(x) /\ { P } S(e) { Q } => { P } m(e) { Q }
slide
:
The correctness calculus
