The Weakest Precondition Calculus

At this stage, with the specification and the code of a function in hand, the problem is to determine if the code is correct with respect to the specification. This decomposes into two problems: partial correctness and termination. Partial correctness means that the code satisfies the pre- and post-conditions, assuming that the code terminates and that it always terminates. Partial correctness will be determined by the WP calculus. Termination is fundamentally nondecidable and must be satisfied separately.

A seminal piece of work about the correctness proof of programs was presented by Robert Floyd at a meeting of the American Mathematical Society in 1967.4 In his talk Floyd discussed attaching assertions to the edges of a flowchart, with the understanding that each assertion would be true during execution of the corresponding program whenever execution reached that edge. For a loop, an invariant was placed on an arbitrary but fixed edge of the cycle that was denoted by a "cut point." It would then prove that if the execution of the cycle beginning at the cut point with P true reached the cut point again, P would still be true at that point. Thus was born the idea of a loop invariant. Floyd also suggested that a specification of proof techniques could provide an adequate definition of a programming language.

Tony Hoare took Floyd's suggestions to heart in his article5 and defined a small programming language (a subpart of Pascal) in terms of a logical system of axioms and inference rules for proving the partial correctness of a program—an extension to predicate calculus. The three main rules are

• For assignment statements (rule 1):

• For conditional statements (rule 2):

In these rules, predicates are enclosed in brackets and statements are written between two such predicates to express the fact that for every state where the left predicate holds, the execution of the statement, if it terminates, always leads to a state where the right predicate holds. Rule 1 gives the semantics of an assignment statement. Rules 2 and 3 are inference rules, meaning that if the premises are satisfied, then it can be inferred that the conclusion also holds. In this way, Hoare attempted to deal with the programming

4. See Robert Floyd's "Assigning Meanings to Programs. Mathematical Aspects of Computer Science," XIX American Mathematical Society, 1967, 19-32.

5. See C. A. R. Hoare's "An Axiomatic Basis for Computer Programming," CACM, vol. 12, no. 7, 1969.

problem at the same time. He restricted himself to "manageable" control structures instead of dealing with flow charts. He attempts to convey the need for such restrictions (programming guidelines), but it is essentially a size problem. It shows how to define a language (or the sublanguage of an existing one such as C) in terms of how to prove programs are correct, instead of how to execute it, which might lead to a simpler design. Tony Hoare founded a whole new school of research on the axiomatic definition of programming languages.

Dijkstra6 was primarily interested in systems that, when started in some initial state, will end up in a final state that, as a rule, depends on the choice of the initial state.

As deterministic systems (C programs) are our targets, the condition that characterizes the set of all initial states such that activation of the system will eventually terminate, leaving the system in a final state satisfying a given post-condition, is called the weakest-precondition (WP) corresponding to that post-condition. Dijkstra called it weakest because the weaker a condition, the more states satisfy it (remember, state predicates are equivalent to state sets), and it is the aim to characterize all possible starting states that are certain to lead to desired final states.

If the system is denoted by S and the desired post-condition by R, then the corresponding weakest precondition is denoted by WP(S, R). If the initial state satisfies it, the mechanism is certain to establish eventually the truth of R. Translated into a function f with pre- and post-conditions, f is partially correct with regards to iff:

This predicate is also called a verification condition (VC), as it has to be discharged for every given pre- and post-condition.

The WP operator has some interesting properties, such as

2. For any code S and post-conditions Q and R such that Q=>R, W(S,Q) => WP(S,R)

3. For any code S and for any post-conditions Q and R,

WP(S,Q) A WP(S,R) = WP(S,QAR) WP(S,Q) V WP(S,R) = WP(S,QVR)

Property 1 expresses that the WP to reach an inaccessible state (i.e., where false holds!) from S is empty. Property 2 shows that the strengthening or the weakening of a post-condition results in a consistent weakened or strengthened WP, respectively.

For programs written in a semantically clean programming language (such as Pascal), Dijkstra derived an operator WP answering the question: How do you derive WP(S,R) for a given S and R?

6. See E. W. Dijkstra's A Discipline of Programming, Prentice-Hall Series in Automatic Computation, 1976.

The programming language chosen was rather simple, consisting of the skip statement, the nondeterministic if statement, the assignment statement, the composition statement, and the nondeterministic loop statement (these sequential statements are the same as in CSP7). These rules are not given here, but instead their counterparts for C. For all these rules, let P, Q, and R be predicates, E be an expression, c1, c2, etc. be constants, and S, S1, S2, etc. be statements.

Assignment Statement Let S = (x=e), then

Conditional Statement Let S = (if b then S1), then

Let S = (if B then S1 else S2), then WP(S,P) = if B then WP(S1,P) else WP(S2,P)

Function Calls Let S = f(a,&b) be a call to function f with associated pre- and postconditions denoted by pre_f and post_f, and whose input and output parameters are a and b, respectively, then

• If post_f is explicit in the form post_f = (y=F(x)) with x and y being, respectively, the formal input and output variables of f, then

WP(S,P) = pre_f[x/a,y/b] A (Vy%, post_f(x,y%) => P(x,y%)) where y% is a new variable of the same domain as y.

While Loops Let S = (while (B) S1). Loops are difficult to compute for the WP as they represent an unknown number of paths, depending on the values of the variables used in B. Partial correctness of the loop, with respect to some pre- and post-conditions, P and Q, is computed by finding an invariant Inv_S such that:

7. See C. A. R. Hoare's Communicating Sequential Processes, Prentice-Hall, 1985.

These express, respectively, that P must imply the invariant; the invariant must always hold as long as the loop condition is true; and Q must hold when the loop terminates. In the absence of P, a precondition for S might simply be Inv_S. The three predicates are also called verification conditions as they have to be discharged for any invariant.

Switch Statements with Breaks Let

thenWP(S,P ) = (E=c1 => WP(S1,P)) A ... A (E=cn => WP(Sn,P)). Sequential Composition Let S = S ;S2, then

The WP of most other statements can be computed using the previously given ones, namely by transforming them syntactically into equivalent instructions whose WP is known.

Symmetric to the WP operator is the strongest-precondition operator (SP) that computes for any statement S and predicate P, the strongest post-condition of S with regard to P.

The SP does a forward computation from the precondition downward, whereas WP computes backward from the post-condition upward. Therefore, some function f is partially correct with regard to its pre- and post-conditions iff:

There are, however, constructs of the C language that pose problems when assigning them proper semantics in the Hoare Logics. This occurs when their informal semantics are unclear or when accessing low-level data or because they are machine-dependent. Dealing with dynamic objects is a tricky problem, especially in relation to aliasing. Aliasing occurs when different variables address or may address the same memory location(s). For instance, writing p=&v creates an alias of v that is *p because they designate the same location. Changing the value of an aliased variable can modify (and falsify) a property on an alias. Solving the aliasing problem requires that you know which variables are aliases of which others and at which program locations. The aliasing problem is complex and might be overcome by computing the dependencies between variables and by approximations on their properties.

Was this article helpful?

0 0
The Ultimate Computer Repair Guide

The Ultimate Computer Repair Guide

Read how to maintain and repair any desktop and laptop computer. This Ebook has articles with photos and videos that show detailed step by step pc repair and maintenance procedures. There are many links to online videos that explain how you can build, maintain, speed up, clean, and repair your computer yourself. Put the money that you were going to pay the PC Tech in your own pocket.

Get My Free Ebook


Post a comment