LARA

Exercise 02

Continuing Lecture 02

Completed Loop Example and Normal Form Theorem

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)

References

Forward with Hoare - a nice survey paper

Continued in Lecture 03