Method for verifying the total correctness of a program with mutually recursive procedures

A computer-implemented apparatus for verifying the total correctness of a computer program with mutually recursive procedures, comprising:

• (a) a computer;
• (b) means, performed by the computer, for receiving the computer program into the computer as a series of source statements, wherein the source statements include annotations indicating intended behavior of the source statements;
• (c) means, performed by the computer, for translating the source statements into an abstract syntax tree and a call graph of the computer program in the computer, wherein the call graph includes nodes representing procedures in the computer program and directed arcs between the nodes representing procedure calls in the computer program;
• (d) means, performed by the computer, for analyzing the abstract syntax tree and call graph for correctness by invoking a Verification Condition Generator in the computer to generate a set of verification conditions from the abstract syntax tree and call graph;
• and
• (e) means, performed by the computer, for outputting the set of verification conditions as conditions to be proven to complete a proof of total correctness of the computer program.

An article of manufacture comprising a program storage medium readable by a computer and tangibly embodying one or more instructions executable by the computer to perform a method for verifying the total correctness of a computer program with mutually recursive procedures, the method comprising the steps of:

• (a) receiving the computer program into the computer as a series of source statements, wherein the source statements include annotations indicating intended behavior of the source statements;
• (b) translating the source statements into an abstract syntax tree and a call graph of the computer program in the computer, wherein the call graph includes nodes representing procedures in the computer program and directed arcs between the nodes representing procedure calls in the computer program;
• (c) analyzing the abstract syntax tree and call graph for correctness by invoking a Verification Condition Generator in the computer to generate a set of verification conditions from the abstract syntax tree and call graph;
• and
• (d) outputting the set of verification conditions as conditions to be proven to complete a proof of total correctness of the computer program.

A method for verifying the total correctness of a computer program with mutually recursive procedures, comprising the steps of:

• (a) accepting a computer program into a memory of a computer, wherein the program comprises a tree of source code and a formal specification of the intended behavior of the computer program;
• (b) annotating the computer program in the memory of the computer at strategic points within the program, wherein the annotations comprise more detailed specifications of the intended behavior of the computer program consistent with the formal specification;
• (c) creating a procedure call graph program in the memory of the computer from the computer program, formal specification, and annotations;
• (d) creating a procedure call tree program in the memory of the computer for each node in the procedure call graph rooted at the node and annotating each node of the procedure call tree with path expressions;
• and
• (e) deriving a set of verification conditions program in the memory of the computer from the computer program, formal specification, annotations, procedure call graph, and procedure call trees, wherein the derived set of verification conditions is sufficient to prove termination and total correctness of the program.