Programming Notes – Weakest Liberal Precondition
The weakest precondition model described in Program States Part 1 provides the basis for many valuable programming algorithms, and is a very successful theory. A slightly different approach starts with primitive notions regarding the Weakest Liberal Precondition. The basic properties outlined in part 2 are derived here from axioms that describe the Weakest Liberal Precondition using a set-based metaphor.
Set-Based Program Statement Axioms
The set-based axioms apply the concept of a set of program states and the subset model of implication described in relations part 3. These axioms use the instance of the Hoare Triple as described in the Introduction to the Hoare Triple.
The set-based model describes the implication between the precondition P, the program statement r, and the expected result R. The event T(r) describes the event ‘activation of program statement r leads to normal termination’.
The expression T(r) has properties distinct from set-based predicates, T(r) is an event, so the rules of proof in theorems must be restricted.
The set model provides a way of describing the meaning of T(r). Program statements behave in more or less predictable ways, so there is a relation r corresponding to the program statement r. Suppose that the symbol ‘a’ represents a program state. Suppose that activation of the program statement leads to program state b. Thus, there exists an ordered pair
a r b
describing the event T(r).
Thus, T(r) may be defined as
Definition 1: T(r) º x r y
If no result state exists for the beginning state x and activating program statement r, then the program statement terminates abnormally. The set of program states T.r contains all points that terminate normally with proper result states. If x and y are two points in a program state space, then the expression
x r y
describes the condition that program statement r terminates normally.
The expression
Ø(x r y)
describes the condition that, given program state x, program statement r cannot terminate with program state y. If no result state exists for a beginning state and program statement, then the program statement must terminate abnormally in the beginning state.
The first Axiom describes the condition of membership to the set T.r and also the condition of normal termination.
Axiom 1: x Î T.rºØ("y|:Ø(x r y))
Axiom 2: ("x,y|xÎP:x r y Þ yÎR) º PÍWLP.r.R
Weakest Liberal Precondition Theorems
The last of the three equivalences follows directly from Axiom 3.
Theorem 1: P Í WLP.r.R º ran.r.P Í R
The set corresponding to normal termination is the domain.
Theorem 2: T(r) = dom.r
The third theorem restates Dijkstra’s second property in equivalent set terminology. If the first result is a subset of the second result, then the first precondition is a subset of the second precondition.
Theorem 3: (P Í Q) Þ WLP.r.P Í WLP.r.Q
Dijkstra’s third property is verified in the set model. The intersection of two preconditions equals the precondition of the intersection.
Theorem 4: WLP.r.P Ç WLP.r.Q = WLP.r.(PÇQ)
Dijkstra’s fourth property is also true in the set model. The union of two preconditions is a sub-set of the precondition of the union.
Theorem 5: WLP.r.P È WLP.r.Q Í WLP.r.(PÈQ)
The next theorem provides a sufficient condition that makes the union of preconditions equal to the precondition of the union. This 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 6: ("X|:(~WLP.r.X = WLP.r.~X)) Þ (WLP.r.(RÈQ) = WLP.r.R È WLP.r.Q)
The Weakest Liberal Precondition may be described using a set-based metaphor as the complement of the domain of the complement. That is, if one eliminates all preconditions that could lead to an undesirable result, then what is left must be an acceptable initial condition.
Theorem 7: WLP.r.R = ~dom.r.(~R)
The relationship between the elements of the relation associated with the program statement r may be expressed as a predicate containing the Weakest Liberal Precondition.
Theorem 8: ("x,y|: x Î WLP.r.R Ù x r y Þ y Î R)
As one would expect, the Weakest Liberal Precondition of a null-set result is wholly contained in the set of conditions leading to non-termination.
Theorem 9: WLP.r.Æ Í ~T.r
If the program statement forms a function so each expected result state is unique for each initial state, then the domain of the result is a liberal precondition.
Theorem 10: r is a function Þ dom.r.R Í WLP.r.R
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