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
