An exercise in weakest preconditions
Robin W. Whitty · Software Testing Verification and Reliability · 1991
Abstract Weakest preconditions are used to formulate the requirements for a 2‐state memory cell and it is proved that the flip‐flop device meets these requirements. This is an exercise in the use of the weakest preconditions which is more realistic than the usual examples of non‐looping arithmetic algorithms.