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/
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
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]
The indexed method provides a direct formal basis for the informal methods of reasoning about software components commonly used by practitioners.
Our example program/specification pair arises out of a three-part problem statement:
Figure 1 shows a possible specification of this procedure,
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.
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 ,
,
, and
. 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 ``
'' 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
``
'' and ``
'' 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 `` '' 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
( ), leaving the values of all other
variables unchanged (
).
Figure 3 shows this Fact replacing the assignment
statement.
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
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
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 b'' we have the fact
For the assignment ``max c'' the fact is similar:
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.
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.