Programming Notes – Weakest Precondition
The Weakest Precondition model is a special case of the Weakest Liberal Precondition in which termination is guaranteed.
The Weakest Liberal Precondition is a condition that guarantees an expected result when the program statement terminates properly. The Weakest Precondition also guarantees that the program statement terminates. Thus the Weakest Precondition is the conjunction of liberal precondition and termination.
Axiom 1: WP.r.R = WLP.r.R Ç T.r
Weakest Precondition of the Universal Set
The weakest precondition of any result is the weakest precondition of the Universal set. By definition, the weakest precondition of a program statement is the weakest precondition of the Universal set.
Definition 1: WP.r = WP.r.U
On these pages, the Hoare Triple represents a precondition, an activated program statement, and an expected result such that the statement terminates normally guaranteeing the expected result. Therefore the precondition in a Hoare Triple must be a subset of the Weakest Precondition.
Axiom 2: P {r} R º P Í WP.r.R
Axiom 2 asserts that the any subset of the weakest precondition is a proper Hoare-Triple solution to the program statement and expected result. The weakest precondition is the special case that contains all of the solutions to the more general Hoare-Triple form.
Weakest Precondition Theorems
The following theorems describe the properties of the Weakest Preconditions as proposed by Dijkstra. These Weakest Precondition properties apply equally as well to the WP.r.R form of Weakest Precondition.
The first theorem shows that the Weakest Precondition is a solution to a weakest liberal precondition.
Theorem 1: WP.r.R Í WLP.r.R
The second theorem shows that Dijkstra’s second property applies to set-based Weakest Preconditions. It also follows that the weakest precondition of any set is a subset of the weakest precondition of the universal set.
Theorem 2: (P Í Q) Þ (WP.r.P Í WP.r.Q)
The third theorem restates Dijkstra’s third property. The intersection of two preconditions equals the precondition of the intersection.
Theorem 3: WP.r.P Ç WP.r.Q = WP.r.(PÇQ)
The fourth theorem restates Dijkstra’s fourth property. The union of two preconditions is a subset of the precondition of the union.
Theorem 4: WP.r.P È WP.r.Q Í WP.r.(PÈQ)
The fifth theorem provides a sufficient condition that makes the union of preconditions equal to the precondition of the union. The fifth theorem is analogous to property 4’ in which a functional change in program states implies that the precondition of conjuctions is equivalent to the conjunction of preconditions.
Theorem 5: ("X|:(~WLP.r.X = WLP.r.~X)) Þ (WP.r.(RÈQ) = WP.r.R È WP.r.Q)
The sixth theorem describes a set-based desccription of Weakest Precondition by combining the set-based description of Weakest Liberal Precondition and the relation-based expression described in Theory of conditions. The program statement condition uses the relation corresponding to the program statement, and may be defined as:
Definition 1: cond.r.R = dom.r.R – dom.r.~R
The weakest precondition corresponds to the set-relation concept of the condition.
Theorem 6: WP.r.R = cond.r.R
The seventh theorem proves property 1. The null set is a precondition to a null expected result.
Theorem 7: WP.r.Æ = Æ
The weakest precondition intersected with the termination set is still just the weakest precondition.
Theorem 8: WP.r.R Ç T.r = WP.r.R
When the relation associated with a program statement is a function, the weakest precondition is also the domain.
Theorem 9: r is a function Þ WP.r.R = dom.r.R
A Programming example:
In the The programming example, the program randomly selects an integer between 0 and 99. The user then tries to guess the number. The program provides help by directing the user to choose a lower or higher number.
Weakest Precondion Problem Set
Become familiar with the program by running it and by guessing a randomly selected integer.
What set of integers represents the precondition that results in a direction to make a higher choice.
What set of integers represents the precondition that results in a direction to make a lower choice.
What set of integers represents the precondition that results in a report that the choice is correct.
What set of integers represents the precondition that results in a direction to choose higher or lower.
What set of integers represents the precondition that results in a direction to choose higher and lower.
The direction to choose higher or to choose lower causes a response from the program’s user.
Describe the user’s resulting action when the program recommends choosing a higher number.
Describe the user’s resulting action when the program recommends choosing a lower number.
What information does the user need to make an informed choice?
Hoare Triple Problem Set
Indicate which of the following solutions are proper and which are improper. The expression
{s|E[x,y]:s}
represents a set of program states in which the variables in the expression E[x,y] have values that make the expression E[x,y] true.
{s|x > 2:s} {x := x-2} {s|x > 0:s}
{s|x = 0:s} {y := 1/x} {s|y > 1:s}
{s|x = 0:s} {y := x} {s|y = x:s}
References:
Dijkstra, Edsgar, 1976, A Discipline of Programming, Englewood Cliffs, NJ: Prentice-Hall
Fejer, Peter and Simovici, Dan A., 1991, Mathematical Foundations of Computer Science, New York, NY: Springer-Verlag
Gries, David and Schneider, Fred B., 1993, A Logical Approach to Discrete Math, New York, NY: Springer-Verlag
Hu Sze-Tsen, 1963, Elements of Modern Algebra, San Francisco: Holden-Day, Inc.
Jia, Xiaoping, 2003, Student Handout for a course described at http://venus.cs.depaul.edu/se431/
Winskel, Glynn 1993 The Formal Semantics of Programming Languages: An Introduction, Cambridge, MA The MIT Press