Lab for Automated Reasoning and Analysis LARA

Lecture 03: Hoare Logic Using Relations

(Continuing Lecture 02. Review Homework 02)

Relational Semantics - Specifying meaning of programs using relations, their composition, union and transitive closure.

Using Relational Semantics - Applying Relational Semantics to Prove Program Properties

Hoare Logic Basics - Hoare Triple, Strongest Postcondition, Weakest Precondition, Non-deterministic loops

(Continued in Lecture 04. We also see some introduction to HOL and theorem proving in Lecture 03a)

sav09/lecture_03.txt · Last modified: 2009/03/10 18:00 by vkuncak
© EPFL 2018 - Legal notice