Exercise 03: Hoare Logic. Building Formulas for Programs. One-Point Rule
(Continuing Lecture 03)
Slides: lecture03b.pptx, lecture03b.pdf
This is actually a lecture, not an exercise session.
Hoare Logic Basics - Hoare Triple, Strongest Postcondition, Weakest Precondition, Non-deterministic loops
Formulas
Formulas and Relations - Moving from abstract relation representations towards formulas that describe relations
Compositional VCG - Computing Formulas for Loop-Free Commands by Following Program Structure
(Continued in Lab 03)