LARA

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)