Loading patent…
AssigneeHewlett-Packard Development Company, L.P.
InventorsJames Benjamin Saxe, Charles Gregory Nelson, David Luke Detlefs
Estimating the term…
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.
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:
A computer readable medium for use in conjunction with a computer system, the computer readable medium comprising a computer readable storage medium and a computer program mechanism embedded therein, the computer program mechanism comprising:
An apparatus for 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 apparatus comprising:
Dependencies are inferred from the claim text.