Floyd Hoare Logic


Click here to start

Table of Contents

Floyd Hoare Logic



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


Skip & Abort

Sequential Composition


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)



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.