This is an old revision of the document!
Generating Verification Conditions
Review: Hoare triples, wp, sp from previous lecture03.
We will first consider programs without loops.
Normal Form of Loop-Free Programs
We continue with verification-condition generation in lecture04.