Exercise 02

Hoare Logic on Relations

Tony Hoare. As of 2012-02-28, the wikipedia picture is from Tony Hoare's lecture at EPFL:

Hoare Logic Basics - Hoare Triple, Strongest Postcondition, Weakest Precondition

Verification Condition Generation

VCG = Verification Condition Generation

Constructing formulas that describe the relations for programs:

Compositional VCG (for loop-free code)


Forward with Hoare - a nice survey paper

Continued in Lecture 03