Deductive verification techniques in the style of Floyd and Hoare have the potential to give us concise, compositional, and scalable proofs of the correctness of various kinds of software systems like programs and control ...