\BOOKMARK [1][]{section.1}{Introduction}{} \BOOKMARK [1][]{section.2}{Modelling Commands and Conditions}{} \BOOKMARK [1][]{section.3}{Commands as transformations of state}{} \BOOKMARK [2][]{subsection.3.1}{Monadic Types}{section.3} \BOOKMARK [2][]{subsection.3.2}{Refinement}{section.3} \BOOKMARK [2][]{subsection.3.3}{Strongest Postconditions}{section.3} \BOOKMARK [2][]{subsection.3.4}{Meaning of Commands}{section.3} \BOOKMARK [2][]{subsection.3.5}{Repetition and Iteration}{section.3} \BOOKMARK [2][]{subsection.3.6}{Monotonicity}{section.3} \BOOKMARK [2][]{subsection.3.7}{The while loop}{section.3} \BOOKMARK [1][]{section.4}{Frames and Variable Names}{} \BOOKMARK [2][]{subsection.4.1}{Assignment; the Syntactic View}{section.4} \BOOKMARK [2][]{subsection.4.2}{Normal Form}{section.4} \BOOKMARK [2][]{subsection.4.3}{Frames}{section.4} \BOOKMARK [1][]{section.5}{Conclusion}{} \BOOKMARK [1][]{section*.16}{References}{}