subsections:

Substitutions


   \%f [x:=v](y)  ==
         v             if x = y
         \%f (y)        otherwise
slide: Substitution

Program state -- $%f$

  • %f \e %S : Var -> Value

State transformations -- operations $a_1,a_2,...,a_n$

  • %f_{0} -{a_1}-> %f_{1} ... -{a_n}-> %f_n

Correctness formulae -- Hoare logic

  • { P } S { Q }

Verification

  • %f_i -{a}-> %f_j /\ %f_i |= P => %f_j |= Q
slide: The verification of state transformations

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