Data processing: artificial intelligence – Knowledge processing system – Knowledge representation and reasoning technique
Reexamination Certificate
2001-07-16
2003-04-22
Starks, Jr., Wilbert L. (Department: 2121)
Data processing: artificial intelligence
Knowledge processing system
Knowledge representation and reasoning technique
C717S152000, C717S152000, C717S158000
Reexamination Certificate
active
06553362
ABSTRACT:
FIELD OF THE INVENTION
The present invention relates generally to tools that automatically verify, using static checking techniques, the correctness of a computer program with respect to predefined criteria, and particularly to a tool that derives verification conditions from a computer program source code. In particular, the present invention relates to the simplification of the verification condition to avoid repeated evaluation by a theorem prover of a subexpression in the verification condition that corresponds to a portion of the computer program that is common to two or more alternative paths through the program.
BACKGROUND
The purpose of a computer program verification system is to analyze a given computer program to determine whether or not it has certain desirable properties. Verification systems can also be used to analyze hardware components. A typical verification system works by generating a verification condition from a given behavioral design, and then evaluating the verification condition with a theorem prover. The verification condition is a mathematical formula. Ideally this formula is valid if and only if the original source program is free of certain kinds of errors.
The verification condition (VC) is analyzed by a theorem prover that attempts to prove the “theorem” that the VC is true. When the theorem prover is unable to prove that the VC is true, it preferably provides a counter-example, which specifies at least one condition for which the VC is false. For example, if the VC is x+y>x, then a counter-example is y≦0.
In general, theorem proving is difficult and may consume exorbitant computer resources. Many verification conditions are not solvable in general. Also, the size of the VC may grow exponentially with the size of the computer program from which it is derived. Another circumstance is that two mathematical formulae may be logically equivalent but one may be harder to prove than the other. Overall, significant computer resources may be expended in theorem proving, even when the computer program corresponding to the VC is not unusually complex or long.
The theory behind VC generation and theorem proving derives from that branch of mathematics known as Logic. Principles underlying VC generation also underlie the general theory of the construction of computer programs and the operation and implementation of programming languages. A theoretical treatment of VC generation in the prior-art can be found in E. W. Dijkstra,
A Discipline of Programming,
Prentice-Hall, (1976); and in C. A. R. Hoare, “An Axiomatic Basis for Computer Programming,”
Communications of the Association for Computing Machinery,
12(10):576-83 (October 1969), both of which are hereby incorporated by reference as background information.
Several program verification systems exist in the prior art. Examples include:
A Program Verifier,
J. King, Ph.D. thesis, Carnegie-Mellon University (1969) in which a system, called Effigy, used Symbolic execution to generate verification conditions; L. P. Deutsch,
An Interactive Program Verifier,
Ph.D. thesis, Univ. Calif., Berkeley, (1973), the first program verifier to use an interactive theorem prover; D. Luckham and N. Suzuki,
Automatic Program Verification V: verification
-
oriented rules for arrays, records and pointers,
Stanford Artificial Intelligence Laboratory Memo AIM-278, (March 1976). The last of these, the Stanford Pascal Verifier, used “Hoare Logic” to generate VC's.
A major contribution to the intensivity of effort in applying the theorem prover is in case-splitting situations, i.e., where choices arise in the program. For example, an “if . . . then . . . else” construct in a computer program provides two alternative, i.e., a pair of, conditional program execution paths, more generally called a choice. Other examples of program constructs that result in a choice are a loop with a loop termination condition, and a conditional branch. All of the aforementioned systems produced VC's with enormous numbers of cases for programs containing a sequential composition of a significant number of alternative choice constructs.
When a computer program has the structure (S
1
S
2
) S
3
(wherein the
operator represents choice), the corresponding VC generated by methods in the prior art will normally include two instances of an expression corresponding to S
3
, wherein one instance is combined with an expression corresponding to S
1
and another instance is combined with an expression for S
2
. More generally, each choice in a computer program will approximately double the size of the resulting VC because of the duplication of S
3
, and will thereby double the amount of work to be performed by the theorem prover to evaluate the VC. Thus, the presence of multiple choices within a computer program will typically cause the complexity of the corresponding VC to increase exponentially when using the methods of the prior art.
Therefore it is a goal of the present invention to generate a VC that is easier for the theorem prover to evaluate and which is smaller in size than the normal VC for the computer program for which the VC is being generated. None of the aforementioned program verification systems featured a solution to the problem, as addressed by the present invention.
SUMMARY OF THE INVENTION
The present invention relates to the generation of a verification condition (VC) from a computer program source code that comprises a collection of program statements.
Accordingly, the present invention involves a method of generating a verification condition for a computer program that comprises a collection of program statements and that contains a pair of conditional program execution paths preceding a control join point and an expression following the control join point, the method comprising: applying at least one precondition operator to the computer program to produce a verification condition which includes a single instance of a subexpression derived from the expression following the control join point, wherein, while applying the at least one precondition operator to the computer program, a label is given to a value, at the control join point, of a variable that is modified on at least one of the conditional program execution paths.
Although a computer program can be transformed directly into a VC and take advantage of the benefits of the present invention, the overall process is facilitated by introducing an intermediate step, whereby the computer program is first converted into an intermediate form comprising “guarded commands.” The preferred input to the VC generator is then a set of guarded commands. In principle, a program written in any computer language can be converted this way.
In a preferred embodiment, the VC generation algorithm is the computation of a weakest precondition. In one embodiment, the weakest precondition of the set of guarded commands is computed and assignment commands (which assign values to variables) are removed from the program through use of the “dynamic single assumption” technique that transforms assignment commands into program assumptions. In another embodiment, the weakest precondition is expressed in terms of strongest postconditions. The commonality between the embodiments is that labels are introduced for the values of variables at control join points and that duplication or near duplication in the VC of subexpressions derived from the expression following the control join point is avoided.
The present invention includes a method of generating a verification condition for a computer program that comprises a collection of program statements and that contains a pair of conditional program execution paths preceding a control join point and an expression following the control join point, the method comprising: when the program statements in the computer program include at least one assignment statement, transforming the at least one assignment statement into an assume command, wherein the transforming includes mapping a variable that is assigned a value by the at least one assignment s
Detlefs David Luke
Nelson Charles Gregory
Saxe James Benjamin
Hewlett--Packard Development Company, L.P.
Pennie & Edmonds LLP
Starks, Jr. Wilbert L.
Williams Gary S.
LandOfFree
Case-reduced verification condition generation system and... does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Case-reduced verification condition generation system and..., we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Case-reduced verification condition generation system and... will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-3001120