Floyd Hoare Logic

26/11/01


Click here to start


Table of Contents

Floyd Hoare Logic

Semantics

Example:

Wp(S, R) represents the set of all states such that execution of S beginning in any one of them is guaranteed to terminate in a finite amount of time satisfying R.

Command S is usually designed to establish the truth of a postcondition R. We may not be interested in wp(S,R). If we can find a stronger precondition Q that represents a subset of the set wp(S,R)and can show Q => wp(S,R) then we are content with Q as the postcondition.

Some properties of wp

Exercises

Skip & Abort

Sequential Composition

Examples:

Multiple Assignment

Execution of an expression may change only the variables indicated and evaluation of an expression may change no variables.

The if statement

Wp (If, R)

Example:

Exercises:

The Iterative Command

Let BB = B1 ? B2 ? ? Bn

Invariant {P} : Predicate that is true throughout the program

Loop Template

Program Verification

Loop Termination

Checklist for loops

Author: Computer Science Dept.