The Axioms for Program Constructs

   { P[ x / y ] }   x = y   { P }

Axiom of Composition:

  If   { P }   S1   { Q }
  and  { Q }   S2   { R }
  then { P }   S1; S2  { R }

Axiom of Condition:

  If   { P and C }      S  { Q }
  and  { P and not C }  T  { Q }
  then { P }
         if C then
            S
         else
            T
         end
       { Q }

Axiom of Iteration:

  If   { P and C }   S   { P }
  then { P }  
         while C do 
             S 
         end  
       { not C and P }