Program Verification That Is More Like Informal Reasoning than the Traditional Approach

Wayne D. Heym

Otterbein College
Westerville, OH 43081
Tel: (614) 823-1623
Fax: (614) 823-1315
Email: WHeym@otterbein.edu
WWW: http://www.otterbein.edu/home/fac/WYNDHYM/

Abstract:

The correctness of a reusable software component's implementation with respect to its specification needs to be ascertained if that implementation is to be considered trustworthy. We have formalized, in a direct, natural way, the informal pattern of reasoning generally used with programs written in modular, imperative languages. Formal proof that a program meets a specification can be done with this new approach or with existing approaches (e.g., calculating weakest preconditions using Hoare-style axioms or using symbolic execution). Alternative systems are distinguished, however, by how well they fit programmers' informal reasoning methods. Programmers think of the effect that the execution of a given statement will have on variables' values, and they consider what conditions must hold for those values in each branch of the program. The new method is organized accordingly, unlike previous methods, which are organized for the convenience of mathematicians.

Keywords: component behavior, specifications, program verification, indexed method, preconditions, postconditions, axioms, soundness, completeness

Workshop Goals: Learning; networking; advance state of practice of reasoning about component behavior

Working Groups: Rigorous Behavioral Specification as an Aid to Reuse, Component Certification Tools, Frameworks and Processes

Background

Formal bases for methods of reasoning about the behavior of sequential programs have existed for some time. [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13] However, if you have explored these methods (based on the work of Floyd, Hoare, and Dijkstra), you may have doubts about their applicability to the ways you usually reason about programs. Recently, we developed a new formal basis, called the indexed method, and argued that, unlike the traditional formal bases, the indexed method provides a direct foundation for the reasoning methods naturally used by programmers. [14] We showed the indexed method to be a true formal basis by establishing its soundness and (relative) completeness. The arguments for the naturalness, soundness, and completeness of the indexed method are lengthy. Therefore, in this brief paper, we illustrate an application of the indexed method to a simple example program. We trust this example to convey the indexed method's flavor. If you already have some experience with the traditional methods, you may sense a greater naturalness in the indexed method. So, while the coming example is not robust support for the following position, stronger support exists in a much longer form. [14]

Position

The indexed method provides a direct formal basis for the informal methods of reasoning about software components commonly used by practitioners.

Application to a Simple Example

Our example program/specification pair arises out of a three-part problem statement:

  1. Specify a procedure that has four formal parameters, a, b, c, and max, all of type Integer, such that the maximum among a, b, and c becomes the value of max.
  2. Provide a sequence of statements to compose the body of this procedure.
  3. Show that the procedure body meets its specification.

Figure 1 shows a possible specification of this procedure,

   figure148
Figure 1: A Program/Specification Pair

calling it ``Set_Maximum.'' We specify procedures by prescribing conditions on the parameters' values. The precondition states what may be assumed about the formal parameters at the beginning of the procedure body. Figure 1, by omitting the requires clause, specifies the weakest possible precondition: true. We may assume nothing special about the values of the formal parameters at the beginning of the procedure body, except that all four are integers.

We call the condition in the ensures clause a postcondition; it states what the procedure body must make true of the values of the formal parameters upon completion of the body's execution. Figure 1 specifies that, at the procedure's conclusion, max's value must equal that of at least one of a, b, and c, and that the value of max must be at least as great as the value of a, b, and c.

Part 2 of the problem asks that we provide a sequence of statements that we believe will always behave according to the procedure's specification. Such a sequence appears after the specification in Figure 1. Next we answer the problem's part 3, showing, according to the new indexed method, that this procedure body meets its specification. The first thing we do is mark each between-statement space with a unique integer. For convenience, we use an increasing sequence of integers, as shown in Figure 2.

   figure173
Figure 2: Indexed Method: First Three Steps

We can then refer to the value each program variable had the last time execution reached position 4, say, with the new names tex2html_wrap_inline1083 , tex2html_wrap_inline1085 , tex2html_wrap_inline1087 , and tex2html_wrap_inline1089 . Many new variable names, obtained by using the unique integers as subscripts on the names of the program variables, are now available to the reasoning process. The name ``indexed method'' comes from the fact that the numbers marking between-statement spaces--and appearing as subscripts in names--function as indexes. The assertion `` tex2html_wrap_inline1091 '' says that ``the value of program variable a, whenever execution reaches position 4, is the same as the value variable a had the most recent time execution was at position 0.'' Both `` tex2html_wrap_inline1091 '' and `` tex2html_wrap_inline1095 '' are true statements in our example.

We can use these subscripted variables to reason about the execution of if -then statements. If execution is at position 5 or 6, we know that the last time execution was at position 4, c was greater than max. That is to say, the condition `` tex2html_wrap_inline1097 '' is necessary for execution at positions 5 or 6. When selection and/or looping statements are nested, so are these conditions. A necessary condition for execution inside one of these nested scopes is the conjunction of the nested conditions associated with the containing statements. We call these conjunctions branch conditions. Figure 2 shows the second step in our reasoning process--marking each branch condition.

Our goal in reasoning is to establish the correctness conjecture for this procedure's specification and body. To do this, we must prove something. Here we must prove that the postcondition holds at position 7; that is our obligation. We abbreviate ``obligation'' to the key word oblig. Figure 2 shows that we write this obligation at position 7.

Fortunately, the statement sequence gives us facts to help prove the obligation. We can replace the first statement, the assignment of a to max, with the key word fact followed by everything this statement makes true. This statement changes the value of max ( tex2html_wrap_inline1099 ), leaving the values of all other variables unchanged ( tex2html_wrap_inline1101 ). Figure 3 shows this Fact replacing the assignment statement.

   figure236
Figure 3: Indexed Method: Replacing an Assignment Statement with a Fact, and the Second if - then Statement with Two Facts

We replace an if -then statement with two Facts. The first fact is that, if the branch condition is true, then the values of all variables after the key word then equal their values before the if. With the second if -then statement, this first fact is

equation313

The second fact establishes variables' values after the key words end if. These values are the same as before the end if when the branch condition is true, but they are the same as before the if when the branch condition is false. This fact, for the second if -then statement, is

eqnarray325

Figure 3 shows these facts replacing the second if -then statement.

When a statement is inside a branch condition, we only know that statement's fact when the condition holds. So we replace the statement with a Fact that is an implication; the branch condition is the left-hand side of the implication, and the effect of the statement is the right-hand side. For the assignment ``max tex2html_wrap_inline1123 b'' we have the fact

equation348

For the assignment ``max tex2html_wrap_inline1123 c'' the fact is similar:

equation360

We replace these statements in precisely the same fashion whether or not we have already replaced the containing if -then\ statement.

This example shows that, in the indexed method, the programming statements can be replaced by facts in different orders of succession. We chose for this example an order that jumps around in the sequence of statements. We replaced the first assignment statement, the second if -then statement, the second assignment, the third assignment, and, finally, the first if -then statement (not shown).

This process yields a sequence of facts and obligations (seven facts and one obligation). The branch conditions and position numbers are no longer necessary, so we remove them. At this point we almost have an assertion in classical mathematics. The indexed method specifies a syntactic tranformation from a sequence of facts and obligations to a single mathematical assertion. The idea behind this transformation is that the truth of an obligation in the sequence depends just on the facts appearing earlier in the sequence, i.e., each obligation is to be proved using only the facts that have already appeared. If we have made no mistakes in applying the indexed method, and if the indexed method is sound, then, if we can prove the obligation given the preceding facts (and we can!), we have proved the correctness conjecture true for this implementation of procedure Set_Maximum.

References

1
J. McCarthy, ``Towards a mathematical science of computation,'' in Information Processing 1962: Proc. IFIP Congress 62 (C. M. Popplewell, ed.), (Amsterdam), pp. 21-28, North Holland, 1963.

2
P. Naur, ``Proof of algorithms by general snapshots,'' BIT, vol. 6, pp. 310-316, 1966.

3
R. W. Floyd, ``Assigning meanings to programs,'' in Proceedings of Symposia in Applied Mathematics (J. T. Schwartz, ed.), vol. 19, (Providence, Rhode Island), pp. 19-32, American Mathematical Society, 1967.

4
C. A. R. Hoare, ``An axiomatic basis for computer programming,'' Communications ACM, vol. 12, pp. 576-580, 583, Oct. 1969.

5
C. A. R. Hoare, ``Proof of correctness of data representation,'' Acta Informatica, vol. 1, no. 4, pp. 271-281, 1972.

6
C. A. R. Hoare, ``Proof of correctness of data representation,'' in Programming Methodology: A Collection of Articles by Members of IFIP WG2.3 (D. Gries, ed.), ch. 19, pp. 269-281, Springer-Verlag, 1978.

7
E. W. Dijkstra, A Discipline of Programming. Prentice-Hall Series in Automatic Computation, Englewood Cliffs, NJ: Prentice-Hall, 1976.

8
Z. Manna, ``The correctness of programs,'' Journal of Computer and Systems Sciences, vol. 3, no. 2, pp. 119-127, 1969.

9
Z. Manna and R. Waldinger, The Logical Basis for Computer Programming, vol. 1, Deductive Reasoning. Reading, Mass.: Addison-Wesley, 1985.

10
J. C. King, A Program Verifier. PhD thesis, Department of Computer Science, Carnegie-Mellon University, 1969.

11
L. P. Deutsch, An Interactive Program Verifier. PhD thesis, Department of Computer Science, University of California, Berkeley, May 1973.

12
R. L. Sites, Proving That Computer Programs Terminate Cleanly. PhD thesis, Department of Computer Science, Stanford University, May 1974.

13
D. MacKenzie, ``The automation of proof: A historical and sociological exploration,'' IEEE Annals of the History of Computing, vol. 17, pp. 7-29, Fall 1995.

14
W. D. Heym, Computer Program Verification: Improvements for Human Reasoning. PhD thesis, The Ohio State University, 1995.

Biography

Wayne D. Heym is Assistant Professor of Computer Science at Otterbein College, Westerville, OH. He continues to collaborate with the Reusable Software Research Group (RSRG) of the Computer and Information Science Department of The Ohio State University. He maintains a strong interest in RSRG's development discipline and language, called RESOLVE, REusable Software Language with Verifiability and Efficiency.

He enjoys introducing non-programmers to the wonders in the art and science of computer programming. He likes leading programmers into the rich and satisfying realm of the theoretical foundations of computer science. He also finds joy in helping beginners become more effective computer users.