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.
|