Case-reduced verification condition generation system and method using weakest precondition operator expressed using strongest postcondition operators6553362Abstract The instructions in a computer program are converted into a form of weakest precondition so as to produce a verification condition that is to be evaluated by a theorem prover. In generating the weakest precondition, labels are introduced for values of variables at control join points. In two preferred embodiments, the computer program is converted into a set of guarded commands prior to the application of weakest precondition operators. In one embodiment, as part of the process of generating the verification condition, assignment commands that assign values to variables are removed from the program through use of a "dynamic single assumption" technique. In another embodiment, the weakest precondition is expressed in terms of strongest postconditions. In both embodiments, a simplified verification condition is produced in which duplications of sets of instructions following a choice operator is avoided. Claims What is claimed is: Description FIELD OF THE INVENTION
TABLE 1
Description of Guarded Commands Used In
A Preferred Embodiment of the Invention
Guarded
Command Explanation
x := e Assign expression e to x; ("x gets e").
var x in S.sub.1 end Introduce a new variable (has an arbitrary initial
value).
assume e Assume e is true at this point in the program (direct the
checker to treat e as true).
assert e Require that e is true (direct the checker to warn if e is
not true).
S.sub.1 ; S.sub.2 Sequential execution of S.sub.1 and S.sub.2.
S.sub.1 {character pullout} S.sub.2 Execute either S.sub.1 or S.sub.2
raise Raise an exception.
S.sub.1 ! S.sub.2 Catch an exception.
Accordingly, the term "guarded command" as used herein will be taken to mean those commands set forth in Table 1, though it is understood by one of skill in the art that the methods of the present invention are not limited to those commands but are applicable to Dijkstra's original commands or many other variations thereof. The guarded command, "var x in S.sub.1 end" is similar to the use of a temporary variable in Java as might find application in, for example, swapping the values of two variables. The context in which "assert e" finds application is in the annotation of programs. For the purposes of generating the verification conditions, annotations other than those required by the compiler can be introduced into the program. The purpose of "assert" is to introduce proof obligations into the verification condition. Proof obligations are conditions that permit the theorem prover to test various aspects of the operation of the program. One example is in the checking for null pointer dereferences. The annotation assert x not null represents a condition that the theorem prover checks. If there is a possibility that x is null, that possibility is encoded within the verification condition. Other examples of annotations include: a division operation wherein an "assert" is used to check whether the divisor is ever zero; and an array boundary checker. Implied annotations are annotations that the programmer does not need to explicitly include in a program because the implied annotations are automatically assumed to apply to all instances of certain program constructs. Thus, pointer dereference instructions may be assumed to include an implied annotation asserting that the pointer to be dereferenced is not null, and division instructions may be assumed to include an implied annotation asserting that the divisor is not equal to zero. Details of the commands "raise" and "bang" ("!") are discussed hereinbelow when considering exceptions. The control constructs in Table 1 hereinabove do not include any constructs for introducing loops into the program. This can be explained as follows. All treatments of loops by automatic program verification systems ultimately work by rewriting a program with loops into some other semantically equivalent program without loops. (Several possible ways of doing this are explained in Section 3 of Leino et al., "Checking Java programs via guarded commands," SRC Technical Note 1999-002, Compaq Computer Corporation, May 21, 1999, referred to hereinabove). The methods of the present invention are to be applied to a loop-free program that results from some rewriting of this kind. As an example illustrating the difference between Dijkstra's guarded commands and those presented here, the translation of an "if . . . else" control construct into guarded commands is presented: if(e) {S.sub.1 } else {S.sub.2 } becomes (assume e; S.sub.1){character pullout}(assume {character pullout}e; S.sub.2). The "if . . . else" construct has been translated into two choices: an assumption that e is True and an assumption that e is False. In the guarded command form, S.sub.1 and S.sub.2 are themselves replaced by their respective translations into guarded commands. In contrast, in Dijkstra's original guarded command language, the "if . . . else" control construct becomes if e.fwdarw.S.sub.1 {character pullout}{character pullout}e.fwdarw.S.sub.2 fi wherein .fwdarw. is a "guard arrow". Therefore, in the implementation presented here, "assume e" is like a guard. Weakest Preconditions A verification condition can be produced by applying a weakest precondition operator to a program. According to methods in the prior art, it is possible to compute the weakest precondition, wp, of a program from the weakest preconditions of its various subparts. By definition, the "weakest precondition" of a program is a logical condition that ensures that the program S executes without error and terminates in a state where a postcondition P is True. Formally, wp(S,P) (also written as wp[S.P] or wp.S.P) is a predicate, or condition, that ensures that program S terminates in a state where P is True. Such a precondition operator is referred to herein as a `traditional` precondition operator. As an example, consider the weakest precondition of a "program" that simply increments variable x. wp(x :=x+1,x.ltoreq.10) In this case, the weakest precondition is the condition that must be fulfilled such that x has value .ltoreq.10 after execution. The weakest precondition is then that x is at least 9, i.e., x.ltoreq.9. Computing Weakest Preconditions for Guarded Commands The weakest precondition operators of the prior art, which are examples of traditional precondition operators, may be applied to the set of guarded commands used herein. Table 2 shows how the weakest precondition computations of the prior art are used to produce a VC. The variables that result in the VC refer to, i.e., label the values of the corresponding program variables in the initial state of the program.
TABLE 2
Weakest Preconditions of Guarded Commands
Guarded Weakest
Command Precondition
S wp.S.P Comments
x := e P.sub.x := e P holds with every occurrence of
x replaced by e.
var x in S.sub.1 end .A-inverted.x: wp.S.sub.1.P S.sub.1 should establish P
regardless
of the initial value of x.
assume e e {character pullout} P If e is True, P should hold.
assert e e {character pullout} P Both e is True and P holds.
S.sub.1 ; S.sub.2 wp.S.sub.1.(wp.S.sub.2.P) Weakest precondition on
S.sub.1 is a
precursor to the weakest
precondition on S.sub.2.
S.sub.1 {character pullout} S.sub.2 wp.S.sub.1.P {character pullout}
wp.S.sub.2.P Weakest precondition is valid for
both S.sub.1 and S.sub.2.
As shown in Table 2 hereinabove, for an assignment command, "x gets e," the weakest precondition, wp.S.P, is the postcondition P with every occurrence of x replaced by e. As an example, for the statement S, given by x :=x+1, (i.e., increment x), subject to the postcondition P, given by x>0, the weakest precondition, wp.S.P, is x+1>0, i.e., x>-1. For introduction of a new variable, "var x in S.sub.1 end", i.e., where a new variable x is introduced with scope S.sub.1, the weakest precondition, given by wp.(var x in S.sub.1).P, is simply: .A-inverted.x: wp.S.sub.1.P. I.e., the postcondition, P, holds, no matter what the initial value of x. For the choice expression, S.sub.1 {character pullout} S.sub.2, the weakest precondition involves a duplication of the postcondition, P (which is the precondition for the remainder of the program, if any, after the choice expression). This problem of duplication is magnified for the case of combinations of sequence and choice expressions. For example, consider the expression S=(S.sub.1 {character pullout}S.sub.2); (S.sub.3 {character pullout}S.sub.4) subject to the postcondition, P. In this case, the resulting expression involves four copies of ##EQU1## Similar problems arise for nested choice, meaning that the verification condition is difficult to prove. In such cases, therefore, the resulting verification condition increases exponentially in size with the number of sequentially composed choice operators, and the resulting verification condition will include a corresponding large number of instances of certain postcondition expressions. As a result, the theorem prover will need to repeatedly evaluate the correctness of the repeated postcondition expressions. It is an object of the present invention to simplify the form of the VC so that it contains fewer instances of the postcondition expressions. Dynamic Single Assumption Thus the computation of weakest preconditions by the prior art methods of Table 2 hereinabove introduces labels only for initial values of program variables, which leads to large and difficult VC's. The methods of the present invention, as described hereinbelow, introduces names for the values of program variables at control join points when the variable is modified on at least one of the conditional program execution paths that preceded the control join point, in addition to names for their initial values. In a preferred embodiment of the present invention, shown in FIG. 4, a computer program 118 is first converted to guarded command form, step 402. Then, instead of carrying out a weakest precondition computation according to the formulae of Table 2, the transformation from a set of guarded commands to a VC involves two steps. In the first step 404, the guarded command form is transformed into a semantically equivalent form called the passive guarded command form, which does not include assignments, by application of a technique referred to herein as "dynamic single assumption" (DSA). The DSA is also described in, Cormnac Flanagan and James B. Saxe, "Avoiding Exponential Explosion: Generating Compact Verification Conditions," Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan. 17-19, 2001, London, UK., ACM SIGPLAN Notices 36(3):193-205, (March 2001), ISBN 1-58113-336-7, which is incorporated herein by reference in its entirety. The application of DSA permits the introduction of labels for values of variables at control join points. Implicit in step 404 can be the derivation of "fix-up" and "merge" code, as described hereinbelow. In the second step 406, a precondition operator is applied to the passive form of the guarded commands to give rise to the VC 124. The transformation of commands to DSA form in step 404 is not limited to programs expressed in guarded command form. As an illustration, consider the following code fragment, in guarded command form, comprising three assignments: x:=1; x :=x+1; x :=x+1; While transforming each assignment statement into an assume command, the variable that is assigned a value by the respective assignment statement is mapped into a new variable corresponding to the assignment statement. Thus, for each assignment, a new variable is introduced, and each assignment in the original code is transformed, in the DSA form, into an assumption about one of the new variables. The DSA form of the code fragment is: assume x.sub.1 =1; assume x.sub.2 =x.sub.1 +1; assume x.sub.3 =x.sub.2 +1; Thus the outcome of using the DSA is to replace every assignment by an "assume," accompanied by introduction of a new variable name. Such an "assume" can be referred to as a "guarded assume" command. Although an "assume" appears similar to an assignment, each "assume" introduced by the DSA transformation can only be carried out once for each variable during the execution of a program. It is to be noted that two alternate conditional execution paths of a program can both contain an "assume" for the same variable. The aim of the DSA transformation is to arrive at a program that is free of assignments. For example, if all variable names are different, the "var" statements may be taken to the outside of any control structure and effectively ignored. The resulting program consists entirely of statements comprising the guarded commands "assume", "assert", choice ({character pullout}) and sequential execution (;). The DSA form of a program may also be referred to as a "passive" form of the program, since it contains no assignment statements. In order to transform commands such as guarded commands into DSA form, it is important to keep track of the mappings between variable names in the original program and variable names in the DSA program at each control point. Such a map is referred to as the "context" for a particular control point. The transformation is defined using a function, dsa, that takes two arguments, a command S and a context R for the initial state of S, and produces a pair of results: a new command S' and a context R' for the final state of S. Accordingly, the DSA of a guarded command, such as x :=e, utilizes a mapping to keep track of variable names. As an example, if e is the expression x+y-z wherein x, y, z are variables in the guarded command form of the program, let R be the mapping {x.fwdarw.x.sub.1, y.fwdarw.y.sub.3, z.fwdarw.z.sub.2 }. Then R(e) is the expression x.sub.1 +y.sub.3 -Z.sub.2. In general, R(e) is obtained from e by replacing each free occurrence of any variable v by the renaming prescribed for v by R. Operationally, the dsa function transforms a command-map pair into another such pair. For example, if R is the mapping {y.fwdarw.y.sub.1 } and S is the command x :=y then dsa(S,R) is the pair (assume x.sub.1 =y.sub.1, {y.fwdarw.y.sub.1, x.fwdarw.x.sub.1 }) In general, if S is a guarded command and R is a mapping, then dsa(S,R) is a pair of passive commands (called T) and a new mapping (called U), such that (1) dom(U), the domain of U, includes (at least) every variable in dom(R) and every variable assigned to in any execution of S; and (2) every possible execution of S has at least one "corresponding" possible execution of T, and vice-versa, where "corresponding" executions are related as follows: (a) for every variable v mentioned in dom(R), the initial value of v in any execution of S is equal to the value of R(v) in any corresponding execution of T; (b) corresponding executions of S and T either both go wrong or both complete normally; and (c) if a corresponding pair of executions of S and T both complete normally, then for every variable v in dom(U) the final value of v after the execution of S is equal to the value of U(v) in the execution of T. By definition, a program "goes wrong" when it is caused to execute a sub-command of the form "assert e" from a state where the expression e evaluates to False. (Note that it is unnecessary to distinguish initial and final values for the execution of T, since T includes no assignment commands.) Condition (2)(b) hereinabove means that the verification condition for S will be valid (signifying that S can never go wrong) if and only if the verification condition for T is valid. Because T contains no assignment statements, its VC can be computed by a specialized method (described hereinbelow and summarized in Table 5). The resulting formula will often be smaller, and its validity easier to test, than would be the case for a verification condition for the original command S computed using prior art methods (e.g., as in Table 2). The DSA for each guarded command is shown in Table 3 hereinbelow, in which "where" means that the ensuing code defines how the replacement commands (such as D.sub.1 and D.sub.2) and the new renaming function(s) (such as R.sub.1, and R.sub.2) are generated. Before applying the DSA rules in Table 3, each subcommand of the form "var x in Send" should be replaced by S.sub.x :=x' where the various x' are chosen to be unique. The DSA transformation is applied to any nested set of commands from the inside to the outside. Thus, also, as shown in Table 3, hereinbelow, a pair of conditional program execution paths is converted into a first group of guarded commands coupled by a choice operator to a second group of guarded commands.
TABLE 3
Transforming Guarded Commands to Dynamic Single Assumption Form
Guarded Command, S dsa(S,R)
x := e (assume x.sub.n = R(e), R[x .fwdarw. x.sub.n
])
where x.sub.n is a new name
OR
(assume True, R[x .fwdarw. R(e)])
assume e (assume R(e), R)
assert e (assert R(e), R)
S.sub.1 ; S.sub.2 (D.sub.1 ; D.sub.2, R.sub.2)
where
(D.sub.1,R.sub.1) = dsa(S.sub.1,R)
(D.sub.2,R.sub.2) = dsa(S.sub.2,R.sub.1)
S.sub.1 {character pullout} S.sub.2 ((D.sub.1 ; FX.sub.1) {character
pullout} (D.sub.2 ; FX.sub.2), R.sub.3)
where
(D.sub.1,R.sub.1) = dsa(S.sub.1,R)
(D.sub.2,R.sub.2) = dsa(S.sub.2,R.sub.1)
(FX.sub.1, FX.sub.2, R.sub.3) =
merge(R.sub.1,R.sub.2);
In Table 3, FX is "fix-up" code and merge is a function that generates the "fix-up" code and a merge-map, both of which are defined below. The dsa function is thus an exemplary transformation function having as one of its outputs a modified mapping for application to a subsequent statement of the computer program, such that the modified mapping is based on variable mappings produced by transformation functions on earlier statements of the computer program. In general, the outcome of applying dsa to a guarded command S and an initial renaming function R is both a new command S and a new renaming function R. The DSA additionally introduces new variable names. The transformation of an assignment statement produces an assume command, such that the transformation includes mapping a variable that is assigned a value by the assignment statement into an expression denoting a value of the variable after the assignment statement. In a preferred embodiment, as shown in the first entry in Table 3, for simple assignment expressions it is possible to avoid introducing a new variable. In such cases the mapping just associates the variable x with whatever expression was originally present, i.e., includes a mapping function that maps said variable to the result of applying to the simple expression a mapping corresponding to a program state before the assignment statement, and accompanies it with a no-op, "assume True." Thus the range of possible mappings for an assignment includes variables to expressions as well as variables to variables. In practice, according to the preferred embodiment of the present invention, whether an assignment is represented by mapping that introduces a new variable name or one which produces a simple substitution, is determined by the complexity of the expression on the right hand side of the assignment. The implicit assumption behind the DSA is that, as demonstrated in FIG. 3, although the same variable x starts in R, before a branch point such as 302, it may attain different variable assignments on either of the ensuing conditional program execution paths such as 304 and 306. In FIG. 3, D.sub.1 and D.sub.2 are collections of one or more executed statements. In FIG. 3, variable x before the branch point attains variable names x.sub.10 and x.sub.11, in each respective branch 304 and 306, both of which need to be merged together after the control join point 308. There is always an implicit control join point at the end of a program. As an example, the following program fragment is transformed into DSA, or "passive," command form: dsa((x:=5{character pullout}(x:=6;x:=x+1));assert x>y,(x.fwdarw.x.sub.0,y.fwdarw.y.sub.0)) where the last term in the parentheses is the mapping given, say, by R. This example comprises a choice ({character pullout}) as well as a sequential composition (semi-colon) operator. The DSA's for each command are therefore embedded in the DSA for the program fragment. The form of the DSA translation for each command is presented in Table 3, hereinabove. Inserting the appropriate expressions, the translation is: (((assume x.sub.1 =5; assume x.sub.4 =x.sub.1){character pullout}(assume x.sub.2 =6; assume x.sub.3 =x.sub.2 +1); assume x.sub.4 =x.sub.3)); assert x.sub.4 >y.sub.0. In this example, "assume x.sub.4 =x.sub.1 " in the first parenthesis and "assume x.sub.4 =x.sub.3 " in the second set of parentheses are respectively "fix-up code." The purpose of the fix-up code is to synchronize, i.e., produce a consistent labeling of, the variables at the conclusion of each conditional execution path of the choice operator. This is important to achieve if the program fragment is embedded in a larger piece of code that includes commands following the program fragment. The fix-up code FX.sub.1 and FX.sub.2 for merging the renaming functions of two program paths, merge(R.sub.1, R.sub.2), is generated using the merge procedure of Table 4.
TABLE 4
Merge Procedure for Merging Mapping Functions R.sub.1 and R.sub.2
FX.sub.1 := Assume True;
FX.sub.2 := Assume True;
R := empty map;
for each x in dom(R.sub.1) .orgate. dom(R.sub.2) do
if x is not in dom(R.sub.1) then
R := R[x .fwdarw. R.sub.2 (x)]
elseif x is not in dom(R.sub.2) then
R := R[x .fwdarw. R.sub.1 (x)]
elseif R.sub.1 (x) = R.sub.2 (x) then
R := R[x .fwdarw. R.sub.1 (x)]
else
let x.sub.n be a new name for x
FX.sub.1 := "FX.sub.1 ; assume x.sub.n = R.sub.1 (x)"
FX.sub.2 := "FX.sub.2 ; assume x.sub.n = R.sub.2 (x)"
R := R[x .fwdarw. x.sub.n ]
endif
end for
return (FX.sub.1, FX.sub.2, R)
At the top of the merge procedure of Table 4, the fix-up codes are initially null and the mapping set is empty. The for-loop in the merge code iterates over all the variables that are either in the map R.sub.1 or the map R.sub.2. For each variable x, if R.sub.1 and R.sub.2 map x to the same variable name, there is no conflict, no new fix-up code is needed and the return output variable map, R, just maps x to whatever it was mapped to by R.sub.1 (or R.sub.2). However, the last else branch within the for loop takes care of the general case where x is mapped differently, i.e., to different variable names, by R.sub.1 and R.sub.2. A new name x.sub.n is introduced to represent the value of x at the control join point, and the fix-up code for each path to the join point is extended with an assumption that the value of x at the end of that path is equal to x.sub.n. The extension of the fix-up code is effectively a concatenation operation and could be written in the form: FX.sub.1 :=FX.sub.1 +"; assume x.sub.n =R.sub.1 (x)" Whatever string FX represented before, i.e., whatever set of assume commands, has now tacked on to it another assume command to cope with the variable in question. Ultimately, the two pieces of fix-up code and the mapping are returned; the result of merge is used in the DSA for a choice operator. VC Generation for Passive Commands In a language with assignments, one can think of a program starting in an initial state comprising certain values of its constituent variables and finishing in a final state with certain values of its constituent variables, some of which may be different from the respective initial values. By contrast, in a program comprising guarded commands in which assignments are represented by assumes, the starting states are constrained. As an example, consider the program: assume x=6; This program can only execute with the starting value, x=6. By contrast, the program: assume x=6 {character pullout} assume x=7; has only two possible starting states. Furthermore, in a language composed of assumes and asserts, certain starting states will result in error-free termination of the program, whereas others will not. The goal of the theorem prover is to ascertain those states that result in, say, a bad assertion. For example, a "good" program (i.e., a program that will execute and terminate correctly) is: assume x>1; assert x>0. This is a good program because it can only execute in states where x is >1 and the condition that x>0 must therefore be true. By contrast, the following program is not good: assume x>0; assert x>1. The assertion could be wrong in the case x=1 and the program could go wrong. In summary, there may be some states in which a program executes correctly, some in which the program goes wrong, and even some in which the program does not execute at all. The absence of assignment statements means that the execution of a passive statement cannot change the program state, and the only effect of such an execution is to choose among the two possible outcomes: normal termination and going wrong. Thus the semantics of a passive statement S can be completely captured by two outcome predicates, one which describes the initial states from which the execution of S may terminate normally, and one which describes states from which the execution of S may go wrong. According to the methods of the present invention, two operators are introduced to enable computation of wp for passive commands, namely norm(S) and bad(S): norm(S) represents the set of states from which the program S could execute normally; bad(S) represents the set of states from which the program S could go wrong. For any passive command, S, wp(S,True)={character pullout}bad(S) Both bad and norm are precondition-like predicate transformers that are different from traditional precondition operators such as wp and which may only be applied to passive commands. In generating the case-reduced VC according to the methods of the present invention, bad and norm take the place of the conventional wp of the prior art. The present invention also utilizes a special predicate transformer, exc, for the "exceptional" termination of a program, which is further described hereinbelow. In the foregoing example, represent the program: assume x>0; assert x>1. by S. Then: norm(S).ident.x>1; bad(S).ident.x>0.LAMBDA.x1. The ultimate goal is to generate a good program, S. A program S is free of errors when bad(S)="False", i.e., when no states can go wrong. Accordingly, the expressions for the application of the norm and bad operators to each kind of passive guarded command are shown in Table 5, hereinbelow.
TABLE 5
Precondition Operators Applied to Passive Commands
Guarded
Com-
mand,
S norm(S) bad(S) Comment
assert e e {character pullout}e "assert e" is executed
normally if e is True;
conversely, if e is False,
"assert e" causes the
program to execute
incorrectly.
assume e e False Program can execute
normally if e is True; since
e is assumed to be True, it
cannot at the same time be
False, and therefore the
assume command cannot
go wrong.
S.sub.1 {character pullout} S.sub.2 norm(S.sub.1) {character pullout}
bad(S.sub.1) {character pullout} Program can execute
norm(S.sub.2) bad(S.sub.2) normally if either S.sub.1 or S.sub.2
executes normally.
Program can go wrong if
either S.sub.1 or S.sub.2 goes wrong.
S.sub.1 ; S.sub.2 norm(S.sub.1) {character pullout} bad(S.sub.1)
{character pullout} Program can execute
norm(S.sub.2) (norm(S.sub.1) {character pullout} normally when
both S.sub.1 and
bad(S.sub.2)) S.sub.2 execute normally, in
sequence; program goes
wrong if either S.sub.1 goes
wrong or if S.sub.1 executes
normally but then S.sub.2 goes
wrong.
The bad and norm functions shown in Table 5 can be used to compute the weakest precondition of a specified program that is expressed in passive command form. As an example of the representation of guarded commands in this way, consider the conversion of the following Java code fragment (which is an instance of the "if . . . else" control construct considered previously): {if (b){ x=x+1; }else{ x=0; } S (where S is some Java Statement). This simple Java construct becomes, in guarded command form: ((assume b; x :=x+1){character pullout}(assume {character pullout}b; x:=0)); S where, as before, S would be represented by its translation into guarded command form. Given the initial mapping {x.fwdarw.x.sub.1 }, the transformation to DSA produces the following passive command and another map: ((assume b; assume x.sub.2 =x.sub.1 +1; assume x.sub.4 =x.sub.2){character pullout} (assume {character pullout}b; assume x.sub.3 =0; assume x.sub.4 =X.sub.3) );S' where S' is the passive form of S translated using {x.fwdarw.x.sub.4 } as the initial mapping. The variable x.sub.4 has been introduced to capture the value of x at the control join point. Referring to the preceding expression as D, it may further be written as (D.sub.1 {character pullout}D.sub.2); S'. In order to obtain the verification condition, bad(D) is computed. This, according to the foregoing expression, is calculated as the bad of the two expressions, (D.sub.1 {character pullout}D.sub.2) and S', separated by the semi-colon operator. Using the expressions shown in Table 5, bad(D) is computed as follows: bad(D)=bad(D.sub.1 {character pullout}D.sub.2) V (norm(D.sub.1 {character pullout}D.sub.2).LAMBDA.bad(S')) The first part of this expression is automatically False because in this case there are no asserts in D.sub.1 or D.sub.2. Therefore (D.sub.1 {character pullout}D.sub.2) never goes wrong in this particular case. This type of simplification is representative of the simplifications that are often (but not always) achievable when generating the VC expression for a program that has been transformed into passive form, wherein Dynamic Single Assumption has been used to transform the guarded commands into passive form. After further simplification, bad(D) is evaluated as follows: ##EQU2## The guarded command expression of the "if . . . else" construct and bad(S') are present in the final simplification. In other words, the postcondition expression bad(S') is only present once in the VC expression for the portion of the program comprising the "if . . . else" construct. Thus, in a situation whereby a pair of conditional program execution paths is transformed to a first group of guarded commands coupled by a choice operator to a second group of guarded commands, the resulting verification condition comprises: a logical OR of a first condition corresponding to the first group of guarded commands and a second condition corresponding to the second group of guarded commands; connected by an implication to a single instance of a post-condition, corresponding to the expression following the control join point, that must always be true after execution of either the first or the second groups of guarded commands. As illustrated hereinbelow, this outcome is contrasted with the standard VC expression, obtained according to the methods of the prior art, that contains at least two instances of the postcondition expression. The same code fragment in guarded command form is: ((assume b; x :=x+1){character pullout}(assume {character pullout}b; x:=0)); S Representing this expression by G, the conventional application of weakest preconditions to G is given by: wp(G,True).ident.(b{character pullout}(wp(S,True).sub.x :=+1).LAMBDA.({character pullout}b{character pullout}(wp(S,True) .sub.x :=0) To evaluate this expression for the weakest precondition for G, it is necessary to evaluate the weakest precondition of S twice, once each with x=0 and x=x+1. If S is itself a large or complex expression, this is costly. Also if there are further "if . . . else" constructs in the same program, even further copies of S will be included in the VC and thus even further copies of the weakest precondition of S will be required to be evaluated. Furthermore, if x appears in S, the multiple copies will be slightly different from one another. In this example, one copy would have x replaced by x+1 and the other copy would have x replaced by 0. Consequently, memory resources will be taken up by the similar, but not identical, copies. In summary, one important aspect of the present invention is that when computing the weakest precondition of an expression such as (S.sub.1 {character pullout}S.sub.2); S.sub.3, wherein S.sub.3 is a complex expression (e.g., containing a collection of commands and possibly additional choice expressions), an evaluation of the weakest precondition of S.sub.3 for both branches of the choice is avoided. The weakest precondition of an expression, such as S.sub.3, that follows the choice operator is a postcondition for the expressions on either side of the choice operator. In particular, the application of the operators bad and norm to statements in passive form leads to a direct simplification that does not arise from the application of the conventional wp operators of the prior art. As an example, consider the program, S: (assume e.sub.1 {character pullout}assume e.sub.2); assert P and let S.sub.1 be "assume e.sub.1 ", S.sub.2 be "assume e.sub.1 " and S.sub.3 be "assert P." Using the bad and norm precondition operators of Table 5 hereinabove the weakest precondition is evaluated as follows: ##EQU3## The final form includes the postcondition P only once. By contrast, using the wp operators of Table 2, hereinabove: wp(S, True)=(e.sub.1 {character pullout}P).LAMBDA.(e.sub.2 {character pullout}P) This expression contains two instances of P and must be further simplified by application of a rule of logic, viz: the equivalence of the expression (p{character pullout}r).LAMBDA.(q{character pullout}r) to (p V q){character pullout}r. The simplification that was inherent in the application of bad and norm to the passive command form is not automatically produced by the application of the traditional weakest precondition operator, wp. A further important advantage of the present invention arises when expressions on either branch of program execution following a choice operator contain assignments. In general, the simplification of an expression of the form (p.LAMBDA.r) V (q.LAMBDA.r) to (p V q).LAMBDA.r can only be achieved when r is the same on both branches. Assignments are troublesome because they can change the representation of r. Consequently, an expression appearing on both sides of a branch may not be the same on both sides because of the various variable replacements that occur. As seen, the weakest precondition of any expression, P, involving an assignment, is: wp(x :=e, P)=P.sub.x :=e Consider the program T: ((assume e.sub.1 ; x=f){character pullout}(assume e.sub.2 ; x =g)); assert P. According to the application of traditional weakest precondition operators, as shown in Table 2, hereinabove, wp(T, True)=(e.sub.1 {character pullout}P.sub.x :=f).LAMBDA.(e.sub.2 {character pullout}P.sub.x :=g) Since the oc`currences of P with x replaced by f.sub.1 and f.sub.2 respectively are not identical to one another, the simplification discussed hereinabove cannot be applied. However, simplification becomes possible by eliminating assignments from T using the Dynamic Single Assumption methodology described hereinabove. T is transformed into passive form by translating the assignment commands into "assume" commands according to the expressions in Table 3. The weakest precondition of the passive form of T can then be obtained by application of the bad and norm operators of Table 5, as described in the foregoing example, during which the simplified form in which P appears once is automatically generated. Ultimately, then, the embodiment of the present invention described hereinabove eliminates assignment commands to avoid the need to include multiple instances of choice expression postconditions in the VC, thereby avoiding or reducing the repetitious evaluation of effectively identical expressions (i.e., the multiple instances of the choice expression postconditions) by the theorem prover. While the application of DSA does not vitiate all possible occurrences of duplication or near duplication of subexpressions, it relieves the situation in many cases. Exceptions Heretofore, the possibility that a program may terminate exceptionally has been ignored. The guarded commands, introduced in Table 1 hereinabove, are able to model exceptions, but the discussion of DSA and weakest preconditions ignored exceptions. The additional guarded commands, "raise" and "bang" (`!`) permit exceptions to be modelled, and the VC-generation techniques described hereinabove can be extended to apply to situations where a program terminates exceptionally. Accordingly a modified version of DSA is described, hereinbelow. An exceptional outcome leaves the variables in some state but is not the same as an outcome in which the program goes wrong or terminates normally. Exceptions are used to model premature exit conditions from portions of the code. They are used to control the behavior of the program when such a condition arises. A program written in a language such as Java can be written to explicitly handle specified exceptions and therefore the translation of such a program into guarded commands should be able to handle exceptions. Other programming constructs such as an intermediate "return" statement from a procedure (in Java, a "method"), or a "break" statement within a loop are also modeled as exceptions. Table 6 describes how the guarded commands of Table 1 behave when an exception arises
TABLE 6
Effect on Guarded Commands when an Exception Arises
Guarded
Command, S Behavior of S.
x := e Assign e to x and terminate normally. (An exception is
never raised)
assume e if e = True, S terminates normally. No execution
is possible otherwise.
assert e if e = True; S terminates normally. If e is False,
S goes wrong.
S.sub.1 ; S.sub.2 Sequential composition. Execute S.sub.1. If S.sub.1
terminates normally, execute S.sub.2. If S.sub.1 goes
wrong or terminates exceptionally, S.sub.2 is ignored.
S.sub.1 {character pullout} S.sub.2 Execute either S.sub.1 or S.sub.2
choosing nondeterministically.
raise Terminate exceptionally.
S.sub.1 ! S.sub.2 Exception handling. Execute S.sub.1. If S.sub.1 goes
wrong
or terminates normally, S.sub.2 is ignored. If S.sub.1
terminates exceptionally, execute S.sub.2.
In order to transform guarded commands into a VC that behaves properly when an exception arises, an alternate, expanded definition of the weakest precondition, wp, is utilized and written as wp (S, N, X), wherein S is a guarded command, N is a normal postcondition and X is an exceptional postcondition. In an equivalent notation, the expanded definition of the weakest precondition is expressed as wp.S.(N, X). The weakest precondition is then the weakest predicate, P, such that: every normally terminating execution of S that starts in a state satisfying P terminates in a state satisfying N; every exceptionally terminating execution of S that starts in a state satisfying P, terminates in a state satisfying X, and no execution of S starting in a state satisfying P goes wrong. This is an extension of the teachings of Dijkstra to accommodate the possibility of exceptions. Dijkstra's only terminating condition was the normal postcondition, N. (See E. W. Dijkstra, A Discipline of programming, Prentice-Hall (1976).) The two guarded commands, "raise," and "bang" (`!`) which is the "dual" of the sequential operator; find special application to the modelling of exceptions. When using the "raise" operator to model a language with multiple exceptions, an appropriate convention is to record the particular exception raised in a reserved global variable, for example xvar. Thus the raising of a particular exception E is modeled with xvar :=E; raise. The "bang" operator (as in S.sub.1 !S.sub.2) shows how to handle an exception when it is raised, say, by S.sub.1 : the bang operator catches it. Here, if S.sub.1 terminates exceptionally, then S.sub.2 is executed. For example, in a string of sequentially executed statements: ( . . . ; raise ; . . . )!S.sub.2 The statements in parenthesis jump straight to S.sub.2 when an exception is raised. If the statements in parenthesis all execute normally, then the program finishes normally, unless S.sub.2 itself terminates exceptionally in which case the program can finish exceptionally. Recalling the norm and bad operators, in Table 5 hereinabove, which represent, respectively, the set of states where a specified passive command could execute or terminate normally or badly, the exc operator is now introduced to enable computation of wp for passive commands that could terminate exceptionally. Accordingly, exc (S) represents the set of states from which the program, S, could terminate exceptionally. The exc operator is used when generating verification conditions. Table 7 extends the VC generation technique of Table 5 hereinabove to passive commands that may include exceptions.
TABLE 7
Precondition Commands for Passive Commands when Exceptions Occur
Guarded
Command, S norm (S) exc (S) bad (S)
assume e e False False
assert e e False {character pullout}e
S.sub.1 ; S.sub.2 norm (S.sub.1) {character pullout} exc (S.sub.1)
{character pullout} bad (S.sub.1) {character pullout}
norm (S.sub.2) (norm (S.sub.1) {character pullout} (norm
(S.sub.1) {character pullout} bad (S.sub.2))
exc (S.sub.2))
S.sub.1 {character pullout} S.sub.2 norm (S.sub.1) {character pullout} exc
(S.sub.1) {character pullout} exc (S.sub.2) bad (S.sub.1) {character
pullout} bad (S.sub.2)
norm (S.sub.2)
raise False True False
S.sub.1 ! S.sub.2 norm (S.sub.1) {character pullout} exc (S.sub.1)
{character pullout} exc (S.sub.2) bad (S.sub.1) {character pullout}
exc (S.sub.1) {character pullout} (exc
(S.sub.1) {character pullout} bad (S.sub.2))
norm (S.sub.2)
As with bad, the exceptional termination of "assume e" never happens and is therefore False. Furthermore, norm (raise) is False because raise never terminates normally--it automatically raises an exception. Correspondingly, because "raise" always terminates exceptionally, exc (raise) is True. The expressions for exc and bad of the sequential composition operator S.sub.1 ; S.sub.2 mirror one another. They have similar forms in which bad and exc occupy corresponding positions. On the other hand, S.sub.1 !S.sub.2, which is the dual of S.sub.1 ; S.sub.2, is such that norm and exc have changed places as well as column positions in Table 7, compared with Table 5. It is also possible to derive forms for exceptional termination using "weakest precondition" language. As before, the job of the theorem prover when evaluating the VC of a program is to determine if there are any states for which bad of the program is True, or alternatively to determine whether bad of the program is False for all possible states of the program. As shown hereinafter, the technique (given in Table 3 hereinabove) for transforming guarded commands to passive form can be extended to deal with commands that may include exceptions. Before listing the version of the DSA transformation that handles exceptional as well as normal commands, the following three points should be noted. First, the DSA transformation presented hereinabove had, as one of its results, a mapping describing the state of the program variables at termination. The result of the modified DSA transformation includes two maps, one describing the state of the program variables upon normal termination and the other describing their state upon exceptional termination. Second, in the original guarded command language the only source of control join points was the non-deterministic choice operator {character pullout}.It is also important to handle additional join points, for example, in (S.sub.1 ; S.sub.2)!S.sub.3 where the exceptional outcomes of S.sub.1 and S.sub.2 join at the start of S.sub.3. The implication for the DSA is additional calls to the merge function. Third, since raise has no normal outcome and several commands have no exceptional outcome, it is worthwhile as an optimization to introduce the special map "bottom", which represents the condition that control cannot reach the relevant control point. Thus "bottom" is used to indicate infeasible code paths. A version of DSA embodying these changes is presented in Table 8. In the Table, FN and FX are fix-up codes for, respectively, normal and exceptional termination.
TABLE 8
Guarded
Command, S dsa (S,R) Comment
x := e (assume x.sub.n = R(e), R[with x .fwdarw. x.sub.n ],
bottom)
assume e (assume R(e), R, bottom)
assert e (assert R(e), R, bottom)
S.sub.1 ; S.sub.2 let (D.sub.1, R.sub.1, X.sub.1) = dsa (S.sub.1, R) X is
the renaming
let (D.sub.2, R.sub.2, X.sub.2) = dsa (S.sub.2, R.sub.1)
function resulting
let (FX.sub.1, FX.sub.2, X) = merge (X.sub.1, X.sub.2) from
merging of
(((D.sub.1 ! (FX.sub.1 ; raise)); (D.sub.2 ! (FX.sub.2 ;
X.sub.1, X.sub.2.
raise))), R.sub.2, X)
S.sub.1 {character pullout} S.sub.2 let (D.sub.1, R.sub.1, X.sub.1) = dsa
(S.sub.1, R)
let (D.sub.2, R.sub.2, X.sub.2) = dsa (S.sub.2, R)
let (FN.sub.1, FN.sub.2, R.sub.3) = merge (R.sub.1, R.sub.2)
let (FX.sub.1, FX.sub.2, X) = merge (X.sub.1, X.sub.2)
((((D.sub.1 ; FN.sub.1) ! (FX.sub.1 ; raise)) {character
pullout}
((D.sub.2 ; FN.sub.2) ! (FX.sub.2 ; raise))), R.sub.3, X)
raise (raise, bottom, R) raise never
terminates
normally
S.sub.1 ! S.sub.2 let (D.sub.1, R.sub.1, X.sub.1) = dsa (S.sub.1, R)
let (D.sub.2, R.sub.2, X.sub.2) = dsa (S.sub.2, X.sub.1)
let (FN.sub.1, FN.sub.2, R.sub.3) = merge (R.sub.1, R.sub.2)
((D.sub.1 ; FN.sub.1) ! (D.sub.2 ; FN.sub.2), R.sub.3,
X.sub.2)
In Table 8, the last argument of the dsa for the guarded command, x :=e, is "bottom", meaning that this command never terminates exceptionally so no mapping is required for that outcome. Having introduced the special map "bottom" as an optimization, merge(R.sub.1, R.sub.2) can be redefined to take advantage of it, as follows: if R.sub.1 =bottom then return (assume True, assume True, R.sub.2) else if R.sub.2 =bottom then return (assume True, assume True, R.sub.1) else proceed as in the merge procedure described in Table 4 hereinabove. In the above, "assume True" is a no-operation (a "no-op"). Since the fix-up code is only used as the right argument to ";", and since "S; assume True" is equivalent to "S" for any command S, these cases require no insertion of fix-up code. Such a situation arises frequently, in, for example a long sequence of statements wherein many of the statements do not raise an exception. Therefore, many of the paths through the code have a "bottom" on them and it is not necessary to generate fix-up code. Application of Strongest Postcondition to the Weakest Precondition Computation In the embodiment described hereinabove, the command to be checked is translated into passive form via the DSA equations of Tables 3 and 8 and then the passive form is translated into a VC via a special version of the weakest precondition computation, using norm, bad, and, if applicable, exc, as described in Tables 5 and 7. Thereby, assignments are removed, and labels are introduced for variables at control join points as well as for their initial values. In a second embodiment, a VC is computed directly from the original command using another special version of the weakest precondition computation, in which weakest preconditions of some subcommands are computed in terms of strongest postconditions. Although the equations involved are quite different from one another, both approaches end up labelling the values of targets at control join points, and thereby eliminate or reduce duplication or near duplication of subexpressions that follow the control join point in the eventual VC. In the second embodiment it is not necessary to remove assignments. By definition, the strongest normal postcondition, snp, of an expression, S, is such that: snp(S, P).ident. the strongest predicate, N, such that every normally terminating execution of S starting from a state that satisfies P, terminates in a state satisfying N. That is, if S starts in a state satisfying P, and terminates normally, snp is the most that can be said about the final state. Analogously, the strongest exceptional postcondition, sxp(S, P) is given by: sxp(S, P).ident. the strongest predicate X such that every exceptionally terminating execution of S starting in a state satisfying P terminates in a state satisfying X. The strongest postcondition, then, of an expression is computed according to the following equations, wherein Q and P are predicates, S.sub.1 and S.sub.2 are commands, x is a variable and e is an expression. Strongest normal postconditions: snp(assume Q, P).ident.Q.LAMBDA.P snp(assert Q, P).ident.Q.LAMBDA.P snp(raise, P).ident.False snp(x:=e, P).ident.(.E-backward.x':P.sub.x :=x'.LAMBDA.x=e.sub.x :=x') snp(S.sub.1 ; S.sub.2, P).ident.snp(S.sub.2, snp(S.sub.1, P)) snp(S.sub.1 !S.sub.2, P).ident.snp(S.sub.1, P).LAMBDA.snp(S.sub.2, sxp(S.sub.1, P)) snp(S.sub.1 {character pullout}S.sub.2, P).ident.snp(S.sub.1, P) V snp(S.sub.2, P) Strongest exceptional postconditions: sxp(assume Q, P).ident.False sxp(assert Q, P).ident.False sxp(raise, P).ident.P sxp(x:=e, P).ident.False sxp(S.sub.1 ; S.sub.2, P).ident.sxp(S.sub.1, P) V sxp(S.sub.2, snp(S.sub.1, P)) sxp(S.sub.1 !S.sub.2, P) sxp(S.sub.2, sxp(S.sub.1, P)) sxp(S.sub.1 {character pullout}S.sub.2, P) sxp(S.sub.1, P) V sxp(S.sub.2, P) An example of strongest postconditions is as follows. The strongest normal postcondition of an expression, given by: snp(v:=v.sup.2, v.gtoreq.3) becomes .E-backward.v' such that v'.gtoreq.3.LAMBDA.v=(v').sup.2 That is, it is desired to ascertain what values integer v could end up with when it is squared, subject to the precondition that v is at least 3. The answer is that there is some initial value of v, denoted v', such that v' satisfies the precondition and such that the final value of v is the value of the expression with v' substituted for v. (v' is rather like a dummy variable, but it is important to ensure that its name does not conflict with other variable names already used.) For the simplification of expressions obtained by applying snp to expressions that include assignments, a general rule, the "one point rule" may be used. The one-point rule says that an expression of the form: .A-inverted.y:y=x{character pullout}P or .E-backward.y:y=x .LAMBDA.P is equivalent to P.sub.y:=x' The approach adopted to case-reduced VC generation in this embodiment, is to compute the weakest precondition of subexpressions in terms of the strongest exceptional and strongest normal postconditions, according to the following relationship, denoted by Equation 1: wp(S, N,X)=wp(S, True, True).LAMBDA.(.A-inverted.TT, T': (snp(S.sub.T:=TT ; T':=TT, TT=T){character pullout}N.sub.T:=T').LAMBDA.(sxp(S.sub.T:=TT !(T':=TT; raise), TT=T){character pullout}X.sub.T:=T')) (Eq. 1) Equation 1 caters for the possibility of exceptional termination of the program. A simpler form of Equation 1 for use with a guarded command language without exceptions is presented as Equation 2: wp(S, N)=wp(S, True).LAMBDA.(.A-inverted.TT,T':(sp(S.sub.T:=TT ;T':=TT, TT=T){character pullout}N.sub.T:=T')) (Eq. 2) wherein sp is an ordinary "strongest postcondition" operator. In the discussion hereinbelow, Equation 1 is discussed. Selective application of Equation 1 to expressions containing the choice operator can lead to the desired simplified forms of verification conditions. In Equation 1, not disclosed in any previous publication, S is a command and N and X are normal and exceptional postconditions. The variables T, TT and T' are tuples of variables. In particular, T represents the "target variables" of command S, that is a list of all program variables that may be modified by S. (Such variables are those that occur on the left hand sides of assignment commands that are subcommands of S.) An expression such as N.sub.T:=T' means N with each variable in T replaced by the corresponding adorned variable in T'. T' and TT represent "adornments" of T, i.e., systematic renamings of the variables in T to new names that do not occur in S, N, or X. An adornment of a variable is also referred to herein as an adorned variable or an inflection of the variable. For example if S contains assignments to variables u and v (and to no other variables), then Equation 1 becomes: wp(S, N, X).LAMBDA.(.A-inverted.uu, vv, u', v': (snp(S.sub.u:=uu, v:=vv ; u':=uu ;v':=vv, (uu, vv)=(u, v)){character pullout}N.sub.u:=u', v:=v').LAMBDA.(sxp(S.sub.u:=uu, v:=vv !(u':=uu ; v':=v; raise), (uu, vv)=(u, v)){character pullout}X.sub.u:=u', v:=v')) wherein uu, vv, u', and v' are variable names not already occurring in S, N, or X. In both the present embodiment and in the embodiment described hereinabove in which the DSA is employed, a given program variable may have several adornments, corresponding to the labels introduced for the values taken on by the given program variable at various points in the program. The approach according to the present embodiment is outlined in FIG. 5. The computer program 118 is optionally converted to guarded command form, step 502, and the strongest postcondition representation of the weakest precondition is computed from the guarded command form, step 504, thereby generating a VC 124. According to this approach, it is not necessary to transform the guarded commands to passive form and there is no need to remove assignments. According to this embodiment, labels are introduced for variables by selectively applying Eq. 1 to compute weakest preconditions instead of using the formulae of Table 2 for a traditional weakest precondition operator. Specifically, if Eq. 1 is used for subexpressions of the form (S.sub.1 {character pullout}S.sub.2) and if the prior art method is used for all other subexpressions, then this embodiment of the present invention effectively introduces the label T' for the value at the control join point after (S.sub.1 {character pullout}S.sub.2) for each target T. The reason that equation 1 is promising for case-reduced VC generation is that it separates the occurrences of S from the occurrences of N and X, placing them on opposite sides of implications ({character pullout}symbols). If S contains choices, then antecedents of the implications (those expressions on the left hand side of the {character pullout}symbol) will end up containing disjunctions, but the postconditions will not be duplicated for each arm of those disjunctions. One convenient approach to simplifying an equation such as Equation 1 is to use the following relationship: (.A-inverted.x:x=e{character pullout}P).ident.P.sub.x:=e Thus, in equation 1, application of this relationship permits the factoring out of TT. An acceptable strategy, therefore, for generating a verification condition is to use equation 1 to expand the wp of choices and to use the ordinary wp equations (Table 2) for all other operators (and also for the expression wp( . . . , True, True) on the right hand side of equation 1). Thus, the method described herein, by which weakest preconditions are written as expressions that comprise strongest postconditions, has succeeded in avoiding the duplication (or approximate duplication) of postconditions that would result in the methods of the prior art that utilize only weakest preconditions. A program whose weakest precondition has been computed in a manner utilizing strongest postconditions, as described hereinabove, is passed to a theorem prover to test its validity as shown in FIG. 1. Savings of resources are consequently gained by avoiding the duplication of expressions following control join points. As would be understood by one of skill in the art, the method of transforming a computer program in guarded command form to a weakest precondition in which subexpressions separated by choice operators are expressed as strongest postconditions, is applicable to computer programs written in other guarded command forms as well as other programming languages that are not first converted to guarded command form. EXAMPLES Example 1 Embodiment Employing Strongest Postconditions As an example of this strategy, suppose it is desired to compute the following weakest precondition expression of a choice expression. wp((x:=5{character pullout}x:=x+1); K, N, X) wherein K is a potentially large command. By applying the ordinary weakest precondition calculation, using the rule for semi-colon, as shown hereinabove in Table 2, the value is: wp((x:=5{character pullout}x:=x+1), wp(K, N, X), X) Applying the strongest postcondition expression, given above in Eq. 1, wherein S is represented by the choice expression in parenthesis, N is represented by the expression wp(K,N,X) and X is simply X, the only target of the command S is x. To apply Eq. 1, the adorned variables xx and x' are introduced. Eq. 1 then gives: wp(x:=5{character pullout}x:=x+1, True, True).LAMBDA.(.A-inverted.xx, x': (snp((x:5{character pullout}xx:=xx+1); x':=xx, xx=x){character pullout}wp(K,N,X).sub.x:=x').LAMBDA.(sxp((x:=5{character pullout}xx:=xx+1); x':=xx, xx=x){character pullout}X.sub.x:=x')) Applying the ordinary weakest precondition formula (Table 2) and simple predicate calculus, the expression wp(x:=5{character pullout}x:=x+1, True, True) simplifies to True. Also, since there are no occurrences of "raise" in the command (xx: 5{character pullout}xx:=xx+1); x':=xx, the application of sxp in the antecedent of the second implication reduces to False, and the implication itself reduces to True. Thus, the entire formula reduces to (.A-inverted.xx, x': snp((xx:=5{character pullout}xx:=xx+1); x':=xx, xx=x)=>wp(K,N,X).sub.x:=x') Applying the rules for snp for assignment, the subexpression snp((xx:=5{character pullout}xx:=xx+1); x':=xx, xx=x) is simplified to x'=xx.LAMBDA.(xx=5V xx=x+1) and therefore the entire formula becomes, on application of the "one-point" rule, (.A-inverted.x':(x'=5V x'=x+1)=>wp(K,N,X).sub.x:=x') which has effectively given the label x' to the value of the program variable x at the control join point following the command (x:=5{character pullout}x:=x+1). Although wp(K,N,X).sub.x:=x' may be large, it is not duplicated for each arm of the nondeterministic choice. There is only one copy of this expression. Instead of substituting both 5 and x+1 separately into wp(K, N, X), it is x' that is substituted. This result is equivalent to the result of merging variables from the DSA used in the first preferred embodiment described above. Note that if wp(K,N,X).sub.x:=x' is valid for all values of x', then a theorem prover might prove the preceding verification condition without separately analyzing the case x'=5 and the case x'=x+1. By contrast if the ordinary wp equations are used to compute the weakest precondition of S, i.e., wp((x:=5{character pullout}x:=x+1);K,N,X) the expression wp(K,N,X).sub.x:=5.LAMBDA.wp(K,N,X).sub.x:=x+1 is obtained, in which wp(K,N,X) is duplicated in two nearly, but not exactly, identical copies. Example 2 Embodiment Employing Conversion to DSA and Comparison with Traditional Weakest Precondition Computation A method according to the present invention has been implemented, as part of the Extended Static Checker for Java ("ESC/Java") project. ESC/Java is a tool for finding, by static analysis, common defects in Java programs that are not normally detected until run-time, if ever (see, K. R. M. Leino, J. B. Saxe and R. Stata, "Checking Java programs via guarded commands.", in Formal Techniques for Java Programs, Technical Report 251, Ed. B. Jacobs, et al., Fernuniversitat Hagen, 1999; and K. R. M. Leino, J. B. Saxe and R. Stata, "ESC/Java user's manual," Compaq Systems Research Center Technical Note 2000-002, October 2000, available from http://research.compag.com/SRC/publications. incorporated herein by reference). The executable object code of ESC/Java is publicly available for research and educational purposes (see Extended Static Checking web-page, Compaq Systems Research Center, http://research.compag.com/SRC/esc). It takes as input a Java program, possibly including user annotations, and produces as output a list of possible defects in the program. The annotations in the input program describe program properties such as method preconditions, method postconditions, and object invariants. These annotations allow ESC/Java to catch software defects using a modular, or method-local, analysis. During this analysis, ESC/Java verifies that the annotations are consistent with the program, and it also uses the annotations to verify that each primitive operation (such as a dereference operation, an array access, or a type cast) will not raise a run-time exception (as might happen, for example, if a dereferenced pointer is null or if an array index is out-of-bounds). To perform this analysis, ESC/Java first translates each method and its correctness property into an intermediate representation, the guarded command form, then translates the intermediate representation into a verification condition, and then uses an automatic decision procedure to determine the validity of the verification condition. In the implementation of the present invention used in this Example, the program to be checked is converted into a passive guarded command form before the VC is generated. Thus duplicated subexpressions in the VC are exact copies (and not substitution instances) of one another. This implementation uses a cutoff K, and only names a duplicated subexpression if the subexpression is larger than K (where the size of a subexpression is the number of nodes in its representation). For any finite value of this cutoff, the size of the resulting VC is linear in the size of the passive statement, and hence at most quadratic in the size of the source program. The validity of the VC is checked with an automatic decision procedure, Simplify (see for example, Nelson, G., "Techniques for program verification," Technical Report CSL-81-10, Xerox Palo Alto Research Center, 1981). This Example presents experimental results comparing five VC-generation options: the standard wp-based translation, and the two-stage translation based on the embodiment described hereinabove with four different values (0, 10, 30, .infin.) for the cutoff size K above which to introduce names for duplicated outcome predicates. These experiments were performed on a 667 MHz ES40 Alpha workstation containing 4 Gb of memory running Tru64 UNIX. ESC/Java is written in Java, and was run on the Compaq Fast VM. The Simplify theorem prover is written in Modula-3, and runs as a separate process. The two processes communicate via Unix pipes. The benchmark used for these experiments is ESC/Java's front-end, which has been annotated with appropriate specifications. This front-end consists of 2292 routines (methods and constructors) totaling over 20,000 lines of code. The routines in the benchmark have been divided into three categories according to their worst performance under any of the five options. The first category contains the ten "hardest" routines. The verification of each of these routines either exhausted a 1 Gb heap or required more than five minutes under at least one of the options. The second category of routines contains the 17 routines that required at least 100 seconds under some option, but no more than 300 seconds under any option. The third category contains the 2184 routines in the benchmark that were successfully verified in under 100 seconds regardless of the VC generation option chosen. The remaining 81 routines in the front end are routines for which ESC/Java performs no VC generation (for example, methods declared in interfaces); these routines are not included in the benchmark. The performance of the five VC generation options on the routines in the benchmark are shown in Table 9 hereinbelow, with results for the ten "hardest" routines given individually, and summed results for the other two categories.
TABLE 9
wp translation Present
invention using DSA
Routine name AST GC VC time PGC % K
VC % time %
BinaryExpr. 420 1805 too big 1545 86 0
5758 1.4
postCheck 10
4840 0.6
30
4700 0.6
.infin.
5513 1.0
LiteralExpr. 423 1417 too big 1608 113 0
5735 1.5
PostCheck 10
5023 1.3
30
5141 1.3
.infin.
5765 1.3
finishFloating 653 3464 too big 7927 229 0
13134 69.5
PointLiteral 10
10616 8.9
30
10583 10.7
.infin.
20416 73.9
ScanCharOr 812 3896 too big 23904 614 0
33502 49.8
String 10
29851 18.1
30
29924 17.1
.infin.
51357 16.3
scanNumber 1030 4170 too big 12383 297 0
19080 34.6
10
15334 23.0
30
15204 14.6
.infin.
25093 10.7
scanPunctuation 509 3326 4751446 350.0 10457 314 0
15525 0 26.0 7
10
13748 0 12.9 4
30
13816 0 12.0 3
.infin.
17972 0 6.8 2
parseNew 794 7052 102780 77.0 27170 385 0
38186 37 530.1 688
Expression 10
36116 35 432.0 561
30
35749 35 419.0 544
.infin.
83659 81 339.2 440
checkExpr 3945 17448 2798672 >2000.0 35491 203 0
61813 2 750.4 <30
10
53779 2 401.5 <16
30
51874 2 347.8 <14
.infin.
90646 3 169.4 <7
checkStmt 2883 15746 1041210 309.0 43417 276 0
67915 7 457.5 148
10
61352 6 251.1 81
30
57726 6 145.4 47
.infin.
105297 10 151.9 49
visitMethodDecl 479 4331 2022351 381.5 5270 122 0
12423 1 10.2 3
10
11430 1 8.7 2
30
11581 1 8.7 2
.infin.
12544 1 8.8 2
sum of 17 other 14735 124511 11782617 1574.5 312822 251 0
489529 4 1777.8 113
routine needing 10
461027 4 1048.0 67
>100 seconds in 30
450090 4 900.7 57
some rum .infin.
955276 8 676.8 43
sum of remaining 148168 1851166 11668371 1613.4 2379973 129 0
7471786 64 2473.1 153
2184 routines 10
7095724 61 1662.8 103
30
6998342 60 1508.5 93
.infin.
7530778 65 1564.1 97
The columns of Table 9 identify: the routine name (or summed category); the size of the abstract syntax tree for the routine (number of nodes); the size of the guarded command (number of nodes); the size of the VC under the wp translation (number of nodes); the time required to check this routine under the wp translation (seconds); the size of the passive version of the guarded command (number of nodes and percentage of original guarded command); the cutoff K for naming duplicated outcome predicates (number of nodes); the size of the VC under the two-stage translation (number of nodes and percentage of the wp VC); and the time required to verify this routine under the two-stage translation (seconds and percentage of time using wp). The times in Table 9 include the time required to translate the Java abstract syntax tree representation into a guarded command, the time required to translate the guarded command into a VC (including translation into the intermediate passive representation, if necessary), and time required to check the VC. For the summed categories, the entries in the percentage columns tell how big one summed quantity is as a percentage of another. The results indicate that all the VC generation algorithms work well on the simpler routines in the third category. The two-stage translation produces smaller VC's that are slightly easier to prove for K=30 or K=.infin.. Choosing K=0 results in the theorem prover performing significant extra work to process the resulting indirections. The wp translation has difficulty scaling to the larger or more complex routines; for five of the routines in this benchmark the wp translation exhausted a 1 Gb heap limit. The two-stage translation involving passive guarded commands performs much better on these complex routines; the resulting VC's are significantly smaller, and can easily fit in the heap. Again, choosing K=0 results in larger proof times. For K>0, the two-stage translation yields VC's that require significantly less time to prove (sometimes by an order of magnitude) than the VC's produced by the wp translation. The routine "parseNewExpression" requires significantly more time to verify under the two-stage translation than under wp. In general, the time required by Simplify to verify a formula is highly dependent on the order in which Simplify chooses to perform various case-splits, and the case-split order is determined by a variety of heuristics. For this routine, we suspect that these heuristics are misled in some manner by the VC generated by the two-stage translation. Overall, the two-stage translation via passive guarded commands performs significantly better than the direct wp translation. It enables ESC/Java to check all of the routines in this benchmark due to the smaller space requirements, and is significantly faster. Excluding the six routines that could not be checked using the wp translation, checking the entire benchmark using wp required 4305 seconds, whereas using the two-stage translation requires only 2994 seconds (for K=30), or 2748 seconds (for K=.infin.). All references cited herein are incorporated herein by reference in their entirety and for all purposes to the same extent as if each individual publication or patent or patent application was specifically and individually indicated to be incorporated by reference in its entirety for all purposes. The present invention can be implemented as a computer program product, or a computer readable medium, that includes a computer program mechanism embedded in a computer readable storage medium. For instance, the computer program product could contain the program modules shown in FIG. 1. These program modules may be stored on a CD-ROM, magnetic disk storage product, or any other computer readable data or program storage product. The software modules in the computer program product may also be distributed electronically, via the Internet or otherwise, by transmission of a computer data signal (in which the software modules are embedded) on a carrier wave. While the present invention has been described with reference to a few specific embodiments, the description is illustrative of the invention and is not to be construed as limiting the invention. Various modifications may occur to those skilled in the art without departing from the true spirit and scope of the invention as defined by the appended claims.
|
Same subclass Same class Consider this |
||||||||||