Lab 03 (actually exercises on Hoare Logic and a 1/2 lecture)
Background
Exercises
Verification-Condition Generation
Compositional VCG - Computing Formulas for Loop-Free Commands by Following Program Structure
Forward VCG - Strongest Postconditions rules
(Continued in Lecture 04)