Method for verifying the total correctness of a program with mutually recursive procedures5963739Abstract A computer-implemented method, apparatus, and article of manufacture for verifying the total correctness of a computer program with mutually recursive procedures. A computer program is received into the computer as a series of source statements, wherein the source statements include annotations indicating the intended behavior of the source statements. The source statements are translated into an abstract syntax tree and a call graph of the program in the computer, wherein the call graph includes nodes representing procedures and directed arcs between the nodes representing procedure calls. The abstract syntax tree and call graph are analyzed 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. The set of verification conditions are outputted as conditions to be proven to complete a proof of total correctness of the program. The set of verification conditions are verified in the computer and a theorem is outputted showing that the program is totally proven to be totally correct with respect to its specification based on the set of verification conditions. Claims What is claimed is: Description BACKGROUND OF THE APPLICATION
______________________________________
E e s = n
Numeric expression e:exp evaluated in state s yields numeric
value n:num.
B b s = t
Boolean expression b:bexp evaluated in state s yields truth
value t:bool.
______________________________________
The notationf›e/x! indicates the function f updated so that ##EQU1## The operational semantics of the programming language is expressed by the following relation: C c s.sub.1 s.sub.2 Command c executed in state s.sub.1 yields resulting state s.sub.2. Table 2.2 gives the structural operational semantics of the programming language, specified by rules inductively defining the relation C. The semantics of the assertion language is given by recursive functions V and A defined on the structure of vexp and aexp, in a directly denotational fashion. Since the expressions may contain variables, their evaluation must refer to the current state.
______________________________________
V v s = n
Numeric expression v:vexp evaluated in state s yields numeric
value n:num.
A a s = t
Boolean expression a:aexp evaluated in state s yields truth
value t:bool.
______________________________________
This syntax and structural operational semantics is the foundational definition for this programming language and its meaning. It is complete, in that the details of any prospective computation are known, given the initial state and the program to be executed. However, it is not the easiest form with which to reason about the correctness of programs. For that, we need to turn to a more abstract representation of the semantics such as Hoare-style program logics. 2.3 Partial and Total Correctness When talking about the correctness of a program, exactly what is meant? In general, this describes the consistency of a program with its specification. There have developed two versions of the specific meaning of correctness, known as partial correctness and total correctness. Partial correctness signifies that every time the program is run, every answer that it gives is consistent with what is specified. However, partial correctness admits the possibility of not giving any answer at all, by permitting the possibility of the program not terminating. A program that does not terminate is still said to be partially correct. In contrast, total correctness signifies that every time the program starts, it will in fact terminate, and the answer it gives will be consistent with what is specified. The partial and total correctness of commands may be expressed by logical formulae called Hoare triples, each containing a precondition, a command, and a postcondition. The precondition and postcondition are boolean expressions in the assertion language. Traditionally, the precondition and postcondition are written with curly braces ({ }) around them to signify partial correctness, and with square braces (›!) to signify total correctness. For the example programming language and its assertion language, notations for partial and total correctness are defined in Table 2.3. As described in the table, {a} is used to denote a boolean assertion expression which is true in all states. This is the same as having all of the free variables of a universally quantified, and so this is also known as the universal closure of a. close a denotes the same universal closure, but by means of a unary operator. With these partial and total correctness notations, it now becomes possible to express an axiomatic semantics for a programming language, as a Hoare-style logic, which is described in the next section. In this application, a larger programming language is studied that will include procedures with parameters. Verifying these procedures will introduce several new issues. It is an obvious but nevertheless significant feature that a procedure call has a semantics which depends on more than the syntactic components of the call itself-it must refer to the declaration of the procedure, which is external and part of the global context. This is unlike all of the constructs in the small example programming language given above. The parameters to a procedure will include both value parameters, which are passed by value, and variable parameters, which are passed by name to simulate call-by-reference. The passing of these parameters, and their interaction with global variables, has historically been a delicate issue in properly defining Hoare-style rules for the semantics of procedure call. The inclusion of parameters also raises the need to verify that no aliasing has occurred between the actual variables presented in each call and the global variables which may be accessed from the body of the procedure, as aliasing greatly complicates the semantics in an intractable fashion. To verify total correctness, it is necessary to prove that every command terminates, including procedure calls. If the termination of all other commands is established, a procedure call will terminate unless it initiates an infinitely descending sequence of procedure calls, which continue issuing new calls deeper and deeper and never finishing them. To prove termination, this infinite recursive descent must be proven to not occur. This will constitute a substantial portion of this application, as a new method for proving the termination of procedure calls is described, which we believe to be simpler, more general, and easier to use than previous proposals. 2.4 Hoare Logics In ›Hoa69!, Hoare presented a way to represent the calculations of a program by a series of manipulations of logical formulae, which were symbolic representations of sets of states. The logical formulae, known as "axioms" and "rules of inference," gave a simple and beautiful way to express and relate the sets of possible program states at different points within a program. In fact, under certain conditions it was possible to completely replace a denotational or operational definition of the semantics of a language with this "axiomatic" semantics. Instead of involving states, these "rules" now dealt with symbolic formulae representing sets of possible states. This had the benefit of more closely paralleling the reasoning needed to actually prove a program correct, without being as concerned with the details of actual operational semantics. To some, reasoning about states seemed "lower level" and more representation-dependent than reasoning about expressions denoting relationships among variables. To illustrate these ideas, consider the Hoare logic in Table 2.4 for the simple programming language developed so far. In the rule for Assignment, the precondition is q›e/x!. denotes the operation of proper substitution; hence, this denotes the proper substitution of the expression e for the variable x throughout the assertion q. There is one small problem with this which is that the expressions e and q are really from two different, though related, languages. We will intentionally gloss over this issue now, simply using e as a member of both languages. This also applies to b where it appears in the Conditional and Iteration rules. Given these rules, we may now compose them to prove theorems about structured commands. For example, from the Rule of Assignment, we have ##EQU2## From these and the Rule of Sequence, we have ##EQU3## For completeness, a Hoare logic will usually contain additional rules not based on particular commands, such as precondition strengthening or postcondition weakening. The Precondition Strengthening Rule in Table 2.4 is an example. 2.5 Soundness and Completeness An axiomatic semantics for a programming language has the benefit of better supporting proofs of program correctness, without involving the detailed and seemingly mechanical apparatus of operational semantics. However, with this benefit of abstraction comes a corresponding weakness. The very fact that the new Hoare rules are more distant from the operational details means a greater possibility that in fact they might not be logically consistent. This question of consistency has two aspects, which are called soundness and completeness. Soundness is the quality that every rule in the axiomatic semantics is true for every possible computation described by the foundational operational semantics. A rule is sound if every computation that satisfies the antecedents of the rule also satisfies its consequent. Completeness is the quality of the axiomatic semantics of being expressive and powerful enough to be able to prove within the Hoare logic theorems that represent every computation allowed by the operational semantics. One could easily come up with a sound axiomatic semantics by having only a few trivial rules; but then one would never be able to derive useful results about interesting programs. Likewise, one could come up with powerful axiomatic semantics with which many theorems about programs could be proven; but if any one rule is not sound, the entire system is useless. Of these two qualities, this application concentrates on soundness. By this choice, we do not intend to minimize the role or importance of completeness; it is simply a question of not being able to solve every problem at once. Nevertheless, we do feel that of the two qualities, soundness is in some sense the more vital one. A system that is sound but not complete may still be useful for proving many programs correct. A system that is complete but not sound will give you the ability to prove many seemingly powerful theorems about programs which are in fact not true with respect to the operational semantics. Also, researchers have occasionally proposed rules for axiomatic semantics which were later found to be unsound. This problem has arisen, for example, in describing the passing of parameters in procedure calls. This history shows a need for some mechanism to more carefully establish the soundness of the rules of an axiomatic semantics, thereby establishing the rules as trustworthy, since all further proof efforts in that language depend on them. 2.6 Verification Condition Generators Given a Hoare logic for a particular programming language, it may be possible to partially automate the process of applying the rules of the logic to prove the correctness of a program. Generally this process is guided by the structure of the program, applying in each case the Hoare logic rule for the command which is the major structure of the phrase under consideration. A Verification Condition Generator 112 takes a suitably annotated program and its specification, and traces a proof of its correctness, according to the rules of the language's axiomatic semantics. Each command has its own appropriate rule which is applied when that command is the major structure of the current proof goal. This replaces the current goal by the antecedents of the Hoare rule. These antecedents then become the subgoals to be resolved by further applications of the rules of the logic. At certain points, the rules require that additional conditions be met; for example, in the Iteration Rule in Table 2.4, there is the antecedent a.LAMBDA..about.bq. This is not a partial correctness formula, and so cannot be reduced further by rules of the Hoare logic. The Verification Condition Generator 112 emits this as a verification condition to be proven by the user. As an example, Table 2.5 presents a Verification Condition Generator 112 for the simple programming language discussed so far. It consists of two functions, the main function vcg and a helper function vcgl. The square brackets ›and ! enclose a list, for which semicolons (`;`) separate list elements; the phrase ›! denotes an empty list. Comma (`,`) creates a pair, and ampersand (`&`) appends two lists together. vcg1 has type cmd.fwdarw.aexp.fwdarw.(aexp.times.(aexp) list). This function takes a command and a postcondition, and returns a precondition and a list of verification conditions that must be proved in order to verify that command with respect to the precondition and postcondition. This function does most of the work of calculating verification conditions. vcg1 is called by the main verification condition generator function, vcg, with type aexp.fwdarw.cmd.fwdarw.aexp.fwdarw.(aexp)list. vcg takes a precondition, a command, and a postcondition, and returns a list of the verification conditions for that command. Given such a Verification Condition Generator 112, there are two interesting things to be asked about it. First, does the truth of the verification conditions it generates in fact imply the correctness of the program? If so, then the Verification Condition Generator 112 is sound. Second, if the program is in fact correct, does the Verification Condition Generator 112 generate verification conditions sufficient to prove the program correct from the axiomatic semantics? Such a Verification Condition Generator 112 is called complete. In this application, we will only focus on the first question, that of soundness. 2.7 Higher Order Logic Higher Order Logic (HOL) is a mechanical proof assistant that mechanizes higher order logic, and provides an environment for defining systems and proving statements about them. It is secure in that only true theorems may be proven, and this security is ensured at each point that a theorem is constructed. HOL has been applied in many areas. The first and still most prevalent use is in the area of hardware verification, where it has been used to verify the correctness of several microprocessors. In the area of software, HOL has been applied to Lamport's Temporal Logic of Actions (TLA), Chandy and Misra's UNITY language, Hoare's CSP, and Milner's CCS and .pi.calculus. HOL is one of the oldest and most mature mechanical proof assistants available, roughly comparable in maturity and degree of use with the Boyer-Moore Theorem Prover ›BM88!. Many other proof assistants have been introduced more recently that in some ways surpass HOL, but HOL has one of the largest user communities and history of experience. It therefore is considered ideal for this work. HOL differs from the Boyer-Moore Theorem Prover in that HOL does not attempt to automatically prove theorems, but rather provides an environment and supporting tools to the user to enable him to prove the theorems. Thus, HOL is better described as a mechanical proof assistant, recording the proof efforts and its products along the way, and maintaining the security of the system at each point, but remaining essentially passive and directed by the user. It is, however, powerfully programmable, and thus the user is free to construct programs which automate whatever theorem-proving strategy he desires. 2.7.1 Higher Order Logic as a Logic Higher Order Logic is a version of predicate calculus which allows quantification over predicate and function symbols of any order. It is therefore an .omega.-order logic, or finite type theory, according to Andrews ›And86!. In such a type theory, all variables are given types, and quantification is over the values of a type. Type theory differs from set theory in that functions, not sets, are taken as the most elementary objects. Some researchers have commented that type theory seems to more closely and naturally parallel the computations of a program than set theory. A formulation of type theory was presented by Church in ›Chu40!. Andrews presents a modern version in ›And86! which he names Q.sub.0. The logic implemented in the Higher Order Logic system is very close to Andrews' Q.sub.0. This logic has the power of classical logic, with an intuitionistic style. The logic has the ability to be extended by several means, including the definition of new types and type constructors, the definition of new constants (including new functions and predicates), and even the assertion of new axioms. The HOL logic is based on eight rules of inference and five axioms. These are the core of the logical system. Each rule is sound, so one can only derive true results from applying them to true theorems. As the HOL system is built up, each new inference rule consists of calls to previously defined inference rules, ultimately devolving to sequences of these eight primitive inference rules. Therefore the HOL proof system is fundamentally sound, in that only true results can be proven. HOL provides the ability to assert new axioms; this is done at the user's discretion, and he then bears any responsibility for possible inconsistencies which may be introduced. Since such inconsistencies may be hard to predict intuitively, we have chosen in our use of the HOL system to restrict ourselves to never using the ability to assert new axioms. This style of using HOL is called a "definitional" or "conservative extension," because it is assured of never introducing any inconsistencies. In a conservative extension, the security of HOL is not compromised, and hence the basic soundness of HOL is maintained. The theoretical foundation of the HOL logic is not described in detail herein, referring the interested reader to ›GM93!, because the purpose of this application is not the study of HOL itself, but rather its application as a tool to support the verification of Verification Condition Generators 112. Hence this application concentrates on describing the useful aspects of HOL that apply to the present invention. 2.7.2 Higher Order Logic as a Mechanical Proof Assistant The HOL system provides the user a logic that can easily be extended, by the definition of new functions, relations and types. These extensions are organized into units called theories. Each theory is similar to a traditional theory of logic, in that it contains definitions of new types and constants, and theorems which follow from the definitions. It differs from a traditional theory in that a traditional theory is considered to contain the infinite set of all possible theorems which could be proven from the definitions, whereas a theory in HOL contains only the subset which have been actually proven using the given rules of inference and other tools of the HOL system. When the HOL system it started, it presents to the user an interactive programming environment using the programming language ML, or Meta Language of HOL. The user types expressions in ML, which are then executed by the system, performing any side effects and printing the value yielded. The language ML contains the data types term and thm, which represent terms and theorems in the HOL logic. These terms represent a second language, called the Object Language (OL) of HOL, embedded within ML. ML functions are provided to construct and deconstruct terms of the OL language. Theorems, however, may not be so freely manipulated. Of central importance is the fact that theorems, objects of type thm, can only be constructed by means of the eight standard rules of inference. Each rule is represented as a ML function. Thus the security of HOL is maintained by implementing thm as an abstract data type. Additional rules, called derived rules of inference, can be written as new ML functions. A derived rule of inference could involve thousands of individual calls to the eight standard rules of inference. Each rule typically takes a number of theorems as arguments and produces a theorem as a result. This methodology of producing new theorems by calling functions is called forward proof. One of the strengths of HOL is that in addition to supporting forward proof, it also supports backwards proof, where one establishes a goal to be proved, and then breaks that goal into a number of subgoals, each of which is refined further, until every subgoal is resolved, at which point the original goal is established as a theorem. At each refinement step, the operation that is applied is called in HOL a tactic, which is a function of a particular type. The effect of applying a tactic is to replace a current goal with a set of subgoals which if proven are sufficient to prove the original goal. The effect of a tactic is essentially the inversion of an inference rule. Tactics may be composed by functions called tacticals, allowing a complex tactic to be built to prove a particular theorem. Functions in ML are provided to create new types, make new definitions, prove new theorems, and store the results into theories on disk. These may then be used to support further extensions. In this incremental way a large system may be constructed. 2.8 Embeddings Previous researchers have constructed representations of programming languages within HOL, of which the work of Gordon ›Gor89! was seminal. He introduced new constants in the HOL logic to represent each program construct, defining them as functions directly denoting the construct's semantic meaning. This is known as a "shallow" embedding of the programming language in the HOL logic, using the terminology described in ›BGG+92!. This approach yielded tools which could be used to soundly verify individual programs. However, there were certain fundamental limitations to the expressiveness of this approach, and to the theorems which could be proven about all programs. This was recognized by Gordon himself ›Gor89!: P›E/V! (substitution) is a meta notation and consequently the assignment axiom can only be stated as a meta theorem. This elementary point is nevertheless quite subtle. In order to prove the assignment axiom as a theorem within higher order logic it would be necessary to have types in the logic corresponding to formulae, variables and terms. One could then prove something like: .vertline.-.A-inverted.P,E,V. Spec(Truth(Subst(P,E,V)), Assign(V, Value E), Truth P) It is clear that working out the details of this would be a lot of work. This application explores the alternative approach described but not investigated by Gordon. It yields great expressiveness and control in stating and proving as theorems within HOL concepts which previously were only describable as meta-theorems outside HOL. To achieve this expressiveness, it is necessary to create a deeper foundation than that used previously. Instead of using an extension of the HOL Object Language as the programming language, an entirely new set of datatypes are created within the Object Language to represent constructs of the programming language and the associated assertion language. This is known as a "deep" embedding, as opposed to the shallow embedding developed by Gordon. This allows a significant difference in the way that the semantics of the programming language is defined. Instead of defining a construct as its semantics meaning, the construct is defined as simply a syntactic constructor of phrases in the programming language, and then the semantics of each construct is separately defined in a structural operational semantics. This separation means that the syntactic program phrases can now be decomposed and analyzed at the HOL Object Language level. Now the semantics of purely syntactic manipulations may be reasoned about within HOL, such as substitution or verification condition generation, since they exist within the HOL logic. This has definite advantages because syntactic manipulations, when semantically correct, are simpler and easier to calculate. They encapsulate a level of detailed semantic reasoning that then only needs to be proven once, instead of having to be repeatedly proven for every occurrence of that manipulation. This will be a recurring pattern in this application, where repeatedly a syntactic manipulation is defined, and then its semantics is described, and proved correct within HOL. 2.9 Additional Information Additional information concerning previous research can be found in Chapter 3 (and other parts) of the co-pending U.S. provisional application Ser. No. 60/016,357, filed Apr. 26, 1996, by inventor Peter Vincent Homeier, entitled "METHOD FOR VERIFYING THE TOTAL CORRECTNESS OF A PROGRAM WITH MUTUALLY RECURSIVE PROCEDURES", which application is incorporated by reference herein. Such additional information is also available in Chapter 3 (and other parts) of the Ph.D. dissertation entitled "TRUSTWORTHY TOOLS FOR TRUSTWORTHY PROGRAMS: A MECHANICALLY VERIFIED VERIFICATION CONDITION GENERATOR FOR THE TOTAL CORRECTNESS OF PROCEDURES", by inventor Peter Vincent Homeier, published by the University of California, Los Angeles, in June, 1995, which dissertation is incorporated by reference herein. 3. Sunrise Programming Language In this section are described the Sunrise programming language and its associated assertion language, which is the language studied in this work. This is a representative member of the family of imperative programming languages, and its constructs will be generally familiar to programmers. The Sunrise language is presented in this application merely as an example of the kinds of langugaes to which this new invention may be applied, and is not intended to limit the invention in any way. Those skilled in the art will recognize that this invention can be applied to any language that includes procedures. The constructs included in the Sunrise language have been carefully chosen to have natural, straightforward, and simple semantics, which will support proofs of correctness. To this end, the normal notation for some constructs has been extended, notably while loops and procedure declarations, to include annotations used in constructing the proof of a Sunrise program's correctness. These annotations are required, but have no effect on the actual operational semantics of the constructs involved. They could therefore be considered comments, except that they are used by the verification condition generator in order to produce an appropriate set of verification conditions to complete the proof. In the past, there has been considerable debate over the need for the programmer to provide, say, a loop invariant. Some have claimed that this is an unreasonable burden on the programmer, who should have to provide only a program and an input/output specification. Others have replied that the requirement to provide a loop invariant forces clear thinking and documentation that should have been done in any case. We would like to take the pragmatic position that the provision of loop invariants is necessary for the simple definition of verification condition generators, which are not complex functions. The same principle holds for the more complex annotations we require for procedures, that the provision of these annotations is necessary for simple and clean definitions of the program logic rules which serve as an axiomatic semantics for procedures. If one wishes to transfer the burden of coming up with the loop invariant from the human to the automatic computer, one incurs a great increase in the degree of difficulty of constructing the verification condition generator, including the need for automatic theorem provers, multiple decision procedures, and search strategies which have exponential time complexity. We wish to attempt something rather more tractable, and to perform only part of the task, in particular that part which seems most amenable to automatic analysis. This desire has guided the construction of the language here defined. 3.1 Programming Language Syntax Table 3.1 contains the concrete syntax of the Sunrise programming language, defined using Backus-Naur Form as a context-free grammar. Six types of phrases are defined in this programming language (Table 3.2): The lexical elements of the syntax expressed in Table 3.1 are numbers and variables. Numbers (denoted by n) are simple unsigned decimal integers, including zero, with no a priori limit on size, to match the HOL type num. They cannot be negative, either as written or as the result of calculations. Variables (denoted with x or y, etc.) are a new concrete datatype var consisting of two components, a string and a number. In HOL a character string may be of any length from zero or more. The name of a variable is typically printed as the string, followed immediately by the variant number, unless it is zero, when no number is printed; the possibility exists for ambiguity of the result. The parser expects the name of the variable to consist of letters, digits, and underscore (`.sub.-- `) except that the first character may also be a caret (` `). However, the operations of the Verification Condition Generator 112 allow the string to contain any characters. The meaning of the string is to be the base of the name of the variable, and the meaning of the number is to be the variant number of the variable. Hence there might be several variables with the same string but differing in their number attribute, and these are considered distinct variables. This structure is used for variables to ease the construction of variants of variables, by simply changing (increasing) the variant number of the variable. Variables are divided into two classes, depending on the initial character (if any) of the string. If the initial character is a caret (` `), then the variable is a logical variable, otherwise it is a program variable. Program and logical variables are completely disjoint; "y" and "y" are separate and distinct variables. Both kinds are permitted in assertion language expressions, but only program variables are permitted in programming language expressions. Since logical variables cannot appear in programming language expressions, they may never be altered by program control, and thus retain their values unchanged throughout a computation. " y" is also sometimes written "y". The syntax given in Table 3.1 uses standard notations for readability. The actual data types (except for lists) are created in HOL as new concrete recursive datatypes, using Melham's type definition package ›GM93!. The results of this definition includes the creation of the constructor functions for the various programming language syntactic phrases in Table 3.3. This forms the abstract syntax of the Sunrise programming language. All the internal computation of the verification condition generator is based on manipulating expressions which are trees of these constructor functions and the corresponding ones for assertion language expressions. These trees are not highly legible. However, we have provided parsers and pretty-printing functions to provide an interface that is more human-readable, so that the constructor trees are not seen for most of the time. 3.2 Informal Semantics of Programming Language The constructs in the Sunrise programming language, shown in Table 3.1, are mostly standard. The full semantics of the Sunrise language will be given as a structural operational semantics later in this section. But to familiarize the reader with these constructs in a more natural and understandable way, informal descriptions of the semantics of the Sunrise language are given here. This is intended to give the reader the gist of the meaning of each operator and clause in Table 3.1. The significance of the system of annotations for both partial and total correctness is also described. 3.2.1 Numeric Expressions n is an unsigned integer. x is a program variable. It may not here be a logical variable. ++x denotes the increment operation, where x is a program variable as above. The increment operation adds one to the variable, stores that new value into the variable, and yields the new value as the result of the expression. The addition, subtraction, and multiplication operators have their normal meanings, except that subtraction is restricted to nonnegative values, so x-y=0 for x.ltoreq.y. The two operands of a binary operator are evaluated in order from left to right, and then their values are combined and the numeric result yielded. 3.2.2 Lists of Numeric Expressions HOL provides a polymorphic list type, and a set of list operators that function on lists of any type. This list type has two constructors, NIL and CONS, with the standard meanings. In both its meta language and object language, HOL typically displays lists using a more compact notation, using square brackets (›!) to delimit lists and semicolons (;) to separate list elements. Thus NIL=›!, and ›2; 3; 5; 7! is the list of the first four primes. In this Sunrise programming language square brackets are reserved to denote total correctness specifications, and so angle brackets (< >) are used instead to denote lists within the Sunrise language, for example <2; 3; 5; 7> or < >. When dealing with HOL lists, however, the square brackets will still be used. The numeric expressions in a list are evaluated in order from left to right and their values are combined into a list of numbers which is the result yielded. 3.2.3 Boolean Expressions The operators provided here have their standard meaning, except for es.sub.1 <<es.sub.2, which evaluates two lists of expressions and compares their values according to their lexicographic ordering. Here the left-most elements of each list are compared first, and if the element from es.sub.1 is less, then the test is true; if the element from es.sub.1 is greater, then the test is false; and if the element from es.sub.1 is the same as (equal to) the element from es.sub.2, then these elements are discarded and the tails of es.sub.1 and es.sub.2 are compared in the same way, recursively. For every operator here, the operands are evaluated in order from left to right, and their values combined and the boolean result yielded. 3.2.4 Commands The skip command has no effect on the state. The abort command causes an immediate abnormal termination of the program. x:=e evaluates the numeric expression e and assigns the value to the variable x, which must be a program variable. c.sub.1 ; c.sub.2 executes command c.sub.1 first, and if it terminates, then executes c.sub.2. The conditional command if b then c.sub.1 else c.sub.2 fi first evaluates the boolean expression b; if it is true, then c.sub.1 is executed, otherwise c.sub.2 is executed. The iteration command assert a with apr while b do c od evaluates b; if it is true, then the body c is executed, followed by executing the whole iteration command again, until b evaluates to false, when the loop ends. The "assert a" and "with a.sub.pr " phrases of the iteration command do not affect its execution; these are here as annotations to aid the verification condition generator. a denotes an invariant, a condition that is true every time control passes through the head of the loop. This is used in proving the partial correctness of the loop. In contrast, a.sub.pr denotes a progress expression, which here must be of the form v<x, where v is a assertion language numeric expression and x is a logical variable. v may only contain program variables. Assertion language expressions will be defined presently; here, v serves as a variant, an expression whose value strictly decreases every time control passes through the head of the loop. This is used in proving the termination of the loop. In future versions of the Sunrise programming language, a.sub.pr will be broadened to other expressions, such as vs<<xs, whose variants describe values of well-founded sets. Finally, p(x.sub.1, . . . , x.sub.n, ; e.sub.1, . . . , e.sub.m) denotes a procedure call. This first evaluates the actual value parameters e.sub.1, . . . , e.sub.m in order from left to right, and then calls procedure p with the resulting values and the actual variable parameters x.sub.1, . . . , x.sub.n. The value parameters are passed by value; the variable parameters are passed by name, to simulate call-by-reference. The call must match the declaration of p in the number of both variable and value parameters. Aliasing is forbidden, that is, the actual variable par ameters x.sub.1, . . . , x.sub.n, may not contain any duplicates, and may not duplicate any global variables accessible from p. The body of p has the actual variable parameters substituted for the formal variable parameters. This substituted body is then executed on the state where the values from the actual value parameters have been bound to the formal value parameters. If the body terminates, then at the end the values of the formal value parameters are restored to their values before the procedure was entered. The effect of the procedure call is felt in the actual variable parameters and in the globals affected. 3.2.5 Declarations The main kind of declaration is the procedure declaration: the other forms simply serve to create lists of procedure declarations or empty declarations. The procedure declaration has the concrete syntax procedure p (var x.sub.1, . . . , x.sub.n ; val y.sub.1, . . . y.sub.m); global z.sub.1, . . . z.sub.k ; pre a.sub.pre ; post a.sub.post ; calls p.sub.1 with a.sub.1 ; calls p.sub.j with a.sub.j ; recurses with a.sub.rec ; end procedure This syntax is somewhat large and cumbersome to repeat; usually the following lithe abstract syntax version is used instead: proc p vars vals gibs pre post calls rec c where it is understood to mean p=p vars=x.sub.1, . . . , x.sub.n vals=y.sub.1, . . . , y.sub.m vars=z.sub.1, . . . , z.sub.k pre=a.sub.pre post=a.sub.post calls=(.lambda.p. false)›a.sub.j /p.sub.j ! . . . ›a.sub.1 /p.sub.1 ! rec=a.sub.rec c=c Note that the calls parameter is now a progress environment of type prog.sub.-- env, where prog.sub.-- env=string.fwdarw.aexp, a function from procedure names to progress expressions, to serve as the collection of all the calls . . . with phrases given. The meaning of each one of these parameters is as follows: p is the name of the procedure, a simple string. vars is the list of the formal variable parameters, a list of variables. If there are no formal variable parameters, the entire "var x.sub.1, . . . , x.sub.n " phrase may be omitted. vals is the list of the formal value parameters, a list of variables. If there are no formal value parameters, the entire "val y.sub.1, . . . , y.sub.m " phrase may be omitted. gibs is the list of the global variables accessible from this procedure. This includes not only those variables read or written within the body of this procedure, but also those read or written by any procedure called immediately or eventually by the body of this procedure. Thus it is a list of all globals which can possibly be read or written during the course of execution of the body once entered. If there are no globals accessible, the entire "global z.sub.1, . . . z.sub.k ;" phrase may be omitted. pre is the precondition of this procedure. This is a boolean expression in the assertion language, which denotes a requirement that must be true whenever the procedure is entered. Only program variables may be used. post is the postcondition of this procedure. This is a boolean expression in the assertion language, which denotes the relationship between the states at the entrance and exit of this procedure. Two kinds of variables may be used in post, program variables and logical variables. The logical variables will denote the values of variables at the time of entrance, and the program variables will denote the values of the variables at the time of exit. The postcondition expresses the logical relationship between these two sets of values, and thus describes the effect of calling the procedure. calls is the progress environment, the collection of all the calls . . . with phrases given. Each "calls p.sub.i with a.sub.i " phrase expresses a relationship between two states, similar to the post expression but for different states. The first state is that at the time of entrance of this procedure p. The second state is that at any time that procedure p.sub.i is called directly from the body of p. That is, if while executing the body of p there is a direct call to p.sub.i, then the second state is that just after entering p.sub.i. Expression a.sub.i is a progress expression. Similar to the post expression, there are two kinds of variables that may be used in a.sub.1, program variables and logical variables. The logical variables will denote the values of variables at the time of entrance of p, and the program variables will denote the values of the variables at the time of entrance of p.sub.i. The progress expression gives the logical relationship between these two sets of values, and thus describes the degree of progress achieved between these calls. rec is the recursion expression for this procedure. It is a progress expression, similar to the progress expression of an iteration command, describing a relationship between two states. For rec, the first state is that at the time of entrance of p, and the second state is any time of entrance of p recursively (at any depth) as part of executing the body of p for the first call. Similar to the post expression, there are two kinds of variables that may be used in rec, program variables and logical variables. The logical variables will denote the values of variables at the time of original entrance of p, and the program variables will denote the values of the variables at the times of recursive entrance of p. The rec expression gives the logical relationship between these two sets of values, and thus describes the degree of progress achieved between recursive calls. There are two permitted forms for rec. rec may be of the form v<x, where v is an assertion language numeric expression and x is a logical variable, or rec may be false. false is appropriate when the procedure p is not recursive and cannot call itself. Otherwise, v<x should be used. v may only contain program variables: it serves as a variant, an expression whose value strictly decreases for each recursive call. Thus if v was equal to x at the time rec was originally called, then at any recursive call to p nested within that first call to p, we should have v<x. In the future, this will be broadened to include other expressions, such as vs<<xs, whose variants describe values in well-founded sets, and the strict decrease described will be in terms of the relation used, e.g., <<. If this procedure is not expected to ever call itself recursively, then the phrase "recurses with a.sub.rec ;" may be omitted, in which case rec is taken by default to be false. Command c is the body of this procedure. It may only use variables appearing in vars, vals, or glbs. The actual significance of the various annotations, especially calls and rec, will be explained in greater depth and illustrated with examples in later sections. 3.2.6 Programs A program consists of a declaration of a set of procedures and a command as the main body. The declarations are processed to create a procedure environment .rho. of type env, collecting all of the information declared for each procedure into a function from procedure names to tuples of the following form: .pi.p=(vars, vals, gibs, pre, post, calls, rec, c). The definition of env is env=string.fwdarw.((var)list.times.(var)list.times.(var)list.times.aexp.tim es.aexp.times.prog.sub.-- env.times.aexp.times.cmd). This environment is the context used for executing the bodies of the procedures themselves, and also for executing the main body of the program. The program is considered to begin execution in a state where the value of all variables is zero; however, this initial state is not included in the proof of a program's correctness. A future version of the Sunrise program may have an arbitrary initial state, and the same programs will prove correct. 3.3 Assertion Language Syntax Table 3.4 contains the syntax of the Sunrise assertion language, defined using Backus-Naur Form as a context-free grammar. Three types of phrases are defined in this assertion language, in Table 3.5. The above syntax uses standard notations for readability. The actual data types are created in HOL as new concrete recursive datatypes, using Melham's type definition package ›GM93!. The results of this definition includes the creation of the constructor functions for the various assertion language syntactic phrases in Table 3.6. This forms the abstract syntax of the Sunrise assertion language. 3.4 Informal Semantics of Assertion Language The constructs in the Sunrise assertion language, shown in Table 3.4, are mostly standard. The full semantics of the Sunrise assertion language will be given as a denotational semantics later in this section. But to familiarize the reader with these constructs in a more natural and understandable way, informal descriptions of the semantics of the Sunrise assertion language are provided here. This is intended to give the reader the gist of the meaning of each operator and clause. The evaluation of any expression in the assertion language cannot change the state; hence it is immaterial in what order subexpressions are evaluated. 3.4.1 Numeric Expressions n is an unsigned integer, as before for the programming language. x is a variable, which may be either a program variable or a logical variable. The addition, subtraction, and multiplication operators have their normal meanings, except that subtraction is restricted to nonnegative values, so x-y=0 for x.ltoreq.y. 3.4.2 Lists of Numeric Expressions These are similar to the lists of numeric expressions described previously for the programming language, except that the constituent expressions are assertion language numeric expressions. This list type has two constructors, NIL and CONS, with the standard meanings. 3.4.3 Boolean Expressions Most of the operators provided here have their standard meaning, and are similar to their counterparts in the programming language, if one exists. true and false are the logical constants. = and < have the normal interpretation, and so do the various boolean operators, such as conjunction and disjunction vs.sub.1 <<vs.sub.2 evaluates two lists of expressions and compares their values according to their lexicographic ordering. (a.sub.1 =>a.sub.2 .vertline.a.sub.3) is a conditional expression, first evaluating a.sub.1, and then yielding the value of a.sub.2 or a.sub.3 respectively, depending on whether a.sub.1, evaluated to T or F, which are the HOL truth constants. close a forms the universal closure of a, which is true when a is true for all possible assignments to its free variables. We have specifically included the universal and existential quantifiers; all quantification is over the nonnegative integers. 3.5 Formal Semantics This section presents the structural operational semantics of the Sunrise programming language, according to the style of Plotkin ›Plo81! and Hennessey ›Hen90!. Also, the semantics of the Sunrise assertion language are presented in denotational style. The definitions in this section are the primary foundation for all succeeding proof activity. In particular, it is from these definitions from which the Verification Condition Generator 112 presented hereinafter is proven sound. These extensions to the HOL system are purely definitional. No new axioms are asserted. This is therefore classified as a "conservative extension" of HOL, and there is no possibility of unsoundness entering the system. This security was essential to this invention. These proofs culminated in the Verification Condition Generator 112 soundness theorems, and once proven, the theorems are applied to example programs without needing to retrace the same proofs for each example. This significant expenditure of effort was necessary because of the history of unsoundness in proposed axiomatic semantics, particularly in relation to procedures. After constructing the necessary proofs, we are grateful for the unrelenting vigilance of the HOL system, which kept us from proving any incorrect theorems. Apparently it is easier to formulate a correct structural operational semantics than it is to formulate a sound axiomatic semantics. This agrees with our intuition, that an axiomatic semantics is inherently higher-level than operational semantics, and omits details covered at the lower level. We exhibit this structural operational semantics as the critical foundation for our work, and present it for the research community's appraisal. As previously described, the programming language has six kinds of phrases, and the assertion language has three. For each programming language phrase, a relation is defined to denote the semantics of that phrase. The structural operational semantics consists of a series of rules which together constitute an inductive definition of the relation. This is implemented in HOL using Melham's excellent library ›Mel91! for inductive rule definitions. The semantics of the assertion language is defined in a denotational style. For each assertion language phrase, a function is defined which yields the interpretation of that phrase into the HOL Object Language. This is implemented in HOL using Melham's tool for defining recursive functions on concrete recursive types ›Mel89!. The types used here are the types of the assertion language phrases. 3.5.1 Programming Language Structural Operational Semantics The structural operation semantics of the six kinds of Sunrise programming language phrases is expressed by the six relations in Table 3.7. In Table 3.8, the rules that inductively define the numeric expression semantic relation E are presented. This is a structural operational semantics for numeric expressions. In Table 3.9, the rules that inductively define the numeric expression list semantic relation ES are presented. This is a structural operational semantics for lists of numeric expressions. The ES relation was actually defined in HOL as a list recursive function, with two cases for the definition based on NIL or CONS. In Table 3.10, the rules that inductively define the boolean expression semantic relation B are presented. This is a structural operational semantics for boolean expressions. In Table 3.11, the rules that inductively define the command semantic relation C are presented. This is a structural operational semantics for commands. In Table 3.12, the rules that inductively define the declaration semantic relation D are presented. This is a structural operational semantics for declarations. In Table 3.13, the rules that inductively define the program semantic relation P are presented. This is a structural operational semantics for programs. As used in this definition, .rho..sub.0 is defined as the empty environment: .rho..sub.1 =.lambda.p. ›!, ›!, ›!, false, true, (.lambda.p. false), false, abort), and s.sub.0 as the initial state s.sub.0 =.lambda.x. 0. 3.5.2 Assertion Language Denotational Semantics The denotational semantics of the three kinds of Sunrise assertion language phrases is expressed by the three functions in Table 3.14. In Table 3.15, a denotational definition of the assertion language semantic function V for numeric expressions is presented. In Table 3.16, a denotational definition of the assertion language semantic function VS for lists of numeric expressions is presented. In Table 3.17, a denotational definition of the assertion language semantic function A for boolean expressions is presented. The lexicographic ordering << is defined as ##EQU4## This concludes the definition of the semantics of the assertion language. The Sunrise language is properly thought of as consisting of both the programming language and the assertion language, even though the assertion language is never executed, and only exists to express specifications and annotations, to facilitate proofs of correctness. The two languages are different in character. The semantics of the programming language is very dependent on time; it both responds to and causes the constantly changing state of the memory. In contrast, the assertion language has a timeless quality, where, for a given state, an expression will always evaluate to the same value irrespective of how many times it is evaluated. The variables involved also reflect this, where program variables often change their values during execution, but logical variables never do. The programming language is an active, involved participant in the execution as it progresses; the assertion language takes the role of a passive, detached observer of the process. This difference carries over to how the languages are used. States and their changes in time are the central focus of the operational semantics, whereas assertions and their permanent logical interrelationships are the focus of the axiomatic semantics. Programs in the programming language are executed, causing changes to the state. Assertions in the assertion language are never executed or even evaluated. Instead they are stepping stones supporting the proofs of correctness, which also have a timeless quality. Done once for all possible executions of the program, a proof replaces and exceeds any finite number of tests. 3.6 Procedure Entrance Semantic Relations In addition to the traditional structural operational semantics of the Sunrise programming language, semantic relations that connect to states reached at the entrances of procedures called from within a command are also defined. These semantic relations are used to define the correctness specifications for the Entrance Logic. The entrance structural operational semantics of commands and procedures is expressed by the two relations described in Table 3.18. In Table 3.19, rules that inductively define the command semantic relation C.sub.-- calls are presented. In Table 3.20, rules that inductively define the procedure path semantic relation M.sub.-- calls are presented. 3.7 Termination Semantic Relations In addition to the other structural operational semantics of the Sunrise programming language, two semantic relations that describe the termination of executions begun in states reached at the entrances of procedures called from within a command are also defined. These semantic relations are used to define the correctness specifications for the Termination Logic. The termination semantics of commands and procedures is expressed by the two relations in Table 3.21. These termination semantic relations are true when all direct calls from c or from the body of p.sub.1 are known to terminate. In Tables 3.22 and 3.23, the definitions of the command termination semantic relation C.sub.-- calls.sub.-- terminate and the procedure path termination semantic relation M.sub.-- calls.sub.-- terminate are presented. The definitions of the relations presented in this section define the semantics of the Sunrise programming language, as a foundation for all later work. From this point on, all descriptions of the meanings of program phrases will be proven as theorems from this foundation, with the proofs mechanically checked. This will ensure the soundness of the later axiomatic semantics, a necessary precondition to a verified Verification Condition Generator 112. 4. Verification Condition Generator In this section, a vcg for the Sunrise programming language is described. This is a function that analyzes programs with specifications to produce an implicit proof of the program's correctness with respect to its specification, modulo a set of verification conditions which need to be proven by the programmer. This reduces the problem of proving the program correct to the problem of proving the verification conditions. This is a partial automation of the program proving process, and significantly eases the task. The previous discussions of many different correctness specifications and Hoare-style rules all culminate here, and contribute to the correctness of the Verification Condition Generator 112 presented. All the rules condense into a remarkably small definition of the verification condition generator. The operations of the Verification Condition Generator are simple syntactic manipulations, which may be easily and quickly executed. The correctness that is proven by the Verification Condition Generator 112 is total correctness, including the termination of programs with mutually recursive procedures. Much of the work involved is aimed at establishing the termination of programs. This is the part of the verification condition generator which is most novel. The partial correctness of programs is verified by the Verification Condition Generator producing a fairly standard set of verification conditions, based on the structure of the syntax of bodies of procedures and the main body of the program. Termination is verified by the Verification Condition Generator producing new kinds of verification conditions arising from the structure of the procedure call graph. 4.1 Definitions In this section, the primary functions that make up the verification condition generator are defined. 4.1.1 Partial Correctness Additional information concerning various aspects of the Verification Condition Generator 112, including variants, Substitution, Translation, Well-Formedness, and Semantic Stages can be found in Chapter 10 (and other parts) of the co-pending U.S. provisional application Ser. No. 60/016,357, filed Apr. 26, 1996, by Peter Vincent Homeier, entitled "METHOD FOR VERIFYING THE TOTAL CORRECTNESS OF A PROGRAM WITH MUTUALLY RECURSIVE PROCEDURES", which application is incorporated by reference herein. Such additional information is also available in Chapter 10 (and other parts) of the Ph.D. dissertation entitled "TRUSTWORTHY TOOLS FOR TRUSTWORTHY PROGRAMS: A MECHANICALLY VERIFIED VERIFICATION CONDITION GENERATOR FOR THE TOTAL CORRECTNESS OF PROCEDURES", by inventor Peter Vincent Homeier, published by the University of California, Los Angeles, in June, 1995, which dissertation is incorporated by reference herein. 4.1.2 Program Logics The following describes some of the program logics used in the present invention. Additional information concerning various aspects of the program logics can be found in Chapter 6 (and other parts) of the co-pending U.S. provisional application Ser. No. 60/016,357, filed Apr. 26, 1996, by Peter Vincent Homeier, entitled "METHOD FOR VERIFYING THE TOTAL CORRECTNESS OF A PROGRAM WITH MUTUALLY RECURSIVE PROCEDURES", which application is incorporated by reference herein. Such additional information is also available in Chapter 6 (and other parts) of the Ph.D. dissertation entitled "TRUSTWORTHY TOOLS FOR TRUSTWORTHY PROGRAMS: A MECHANICALLY VERIFIED VERIFICATION CONDITION GENERATOR FOR THE TOTAL CORRECTNESS OF PROCEDURES", by inventor Peter Vincent Homeier, published by the University of California, Los Angeles, in June, 1995, which dissertation is incorporated by reference herein. 4.1.2.1 Call Progress Function The call-rogress function can compute the appropriate precondition when starting execution from the entrance of one procedure to establish a given entrance condition for another procedure as true. It is defined in Table 4.1. This is a specific example of such a function, made in particular to fit the exact semantics of the Sunrise language. Those skilled in the art will understand that the present invention also covers adaptations of this to match the semantics of other languages. Once the environment .rho. is proven to be well-formed for calls progress, the following rule, proven as a theorem, applies for proving the effect of the call.sub.-- progress function across a single procedure call. Call Progress Rule: ##EQU5## 4.1.2.1.1 Example of Call Progress Specification As an example, consider the progress of calls from procedure odd to procedure even in the odd/even program presented in Table 4.2. It has been proved that the correctness of the claim in the heading for procedure odd that calls even with n<n, that the value of the n argument to even must be strictly less than the value of n at the head of the of the body of odd. Then, by the Call Progress Rule given above, we have: ##EQU6## The invocation of call.sub.-- progress evaluates as: ##EQU7## Thus, we have proven: ##EQU8## A similar pattern of reasoning could be followed to proved the following: ##EQU9## 4.1.2.2 Call Path Progress Function Just as the call.sub.-- progress function can compute the appropriate precondition across a single procedure call, the call.sub.-- path.sub.-- progress function can compute the appropriate precondition when starting execution from the entrance of one procedure to establish a given entrance condition at the end of a path of procedure calls. It is defined in Table 4.3. Once the environment .rho. is proven to be well-formed for preconditions and for calls progress, the following rule, proven as a theorem, applies for proving the effect of the call.sub.-- path.sub.-- progress function across a path of procedure calls. ##EQU10## 4.1.2.2.1 Example of Call Path Progress Specification As an example, consider the progress of paths of procedure calls that involve the procedure even in the odd/even program presented in Table 4.2. Examining the procedure call graph in FIG. 2, we can observe several cycles that include the even node. Let us assume the correctness of the call progress parts of the headers of the procedures as declared, that is, that every calls . . . with clause has been verified to be true. Then, consider the path odd.fwdarw.odd.fwdarw.even. By the Call Path Progress Rule given above, we have: ##EQU11## We previously evaluated call-progress odd even (n<n) .rho. as: ##EQU12## Using this, we can evaluate the invocation of call.sub.-- path.sub.-- progress as call.sub.-- path.sub.-- progress odd (odd) even (n<n) ##EQU13## Thus, we have proven: ##EQU14## Similar patterns of reasoning could be followed to prove the following: ##EQU15## 4.1.2.3 Hoare Logic for Total Correctness 4.1.2.3.1 Total Correctness Specification
______________________________________
›a.sub.1 ! c ›a.sub.2 !/.rho.
a.sub.1 precondition
c command
a.sub.2 postcondition
.rho. procedure environment
______________________________________
4.1.2.3.2 Semantics of Total Correctness Specification ##EQU16## If the command c is executed, beginning in a state satisfying a.sub.1, then the execution terminates in a state satisfying a.sub.2. Consider the Hoare logic in Tables 4.4 and 4.5 for total correctness. This is a traditional Hoare logic for total correctness, except that we have added /.rho. at the end of each specification to indicate the ubiquitous procedure environment. This must be used to resolve the semantics of procedure call. However, the environment .rho. never changes during the execution of the program, and hence could be deleted from every specification, being understood in context. Of particular interest are the Rule of Adaptation and the Procedure Call Rule. Each rule has been proved completely sound from the corresponding rules in Tables 4.6 and 4.7, using the following rule: ##EQU17## The procedure environment .rho. is defined to be well-fonned for correctness if for every procedure p, its body is totally correct with respect to the given precondition and postcondition: ##EQU18## An environment .rho. is well-formed for correctness if and only if it is well-formed for partial correctness and for termination. ##EQU19## 4.1.3 Verification of Commands There are two Verification Condition Generator functions that analyze commands. The main function is the vcgc function. Most of the work of vcgc is done by a helper function, vcg1. In the definitions of these functions, comma (,) makes a pair of two items, square brackets (›!) delimit lists, semicolon (;) within a list separates elements, and ampersand (&) appends two lists. In addition, the function dest< is a destructor function, breaking an assertion language expression of the form v.sub.0 <v.sub.1 into a pair of its constituent subexpressions, v.sub.0 and v.sub.1. The vcg1 function is presented in Table 4.8. This function has type cmd.fwdarw.prog.sub.-- env.fwdarw.aexp.fwdarw.env.fwdarw.(aexp.times.(aexp)list). vcg1 takes a command, a calls progress environment, a postcondition, and a procedure environment, and returns a precondition and a list of verification conditions that must be proved in order to verify that command with respect to the precondition, postcondition, and environments. vcg1 is defined recursively, based on the structure of the command argument. Note that the procedure call clause includes calls p; this inclusion causes the verification conditions generated to verify not only the partial correctness of the command, but also the calls progress claims present in calls. The vcgc function is presented in Table 4.9. This function has type aexp.fwdarw.cmd.fwdarw.prog.sub.-- env.fwdarw.aexp.fwdarw.env.fwdarw.(aexp)list. vcgc takes a precondition, a command, a calls progress environment, a postcondition, and a procedure environment, and returns a list of verification conditions that must be proved in order to verify that command with respect to the precondition, postcondition, and environments. 4.1.4 Verification of Declarations The verification condition generator function to analyze declarations is vcgd. The vcgd function is presented in Table 4.0. This function has type dec1.fwdarw.env.fwdarw.(aexp)list. vcgd takes a declaration and a procedure environment, and returns a list of verification conditions that must be proved in order to verify the declaration's body with respect to the precondition, postcondition, and environments. 4.1.5 Verification of Call Graph The next several functions deal with the analysis of the structure of the procedure call graph. The description begins with the lowest level functions, and build up to the main Verification Condition Generator function for the procedure call graph, vcgg. There are two mutually recursive functions at the core of the algorithm to analyze the procedure call graph, extend.sub.-- graph vcs and fan.sub.-- out.sub.-- graph.sub.-- vcs. They are presented together in Table 4.11. Each yields a list of verification conditions to verify progress across parts of the graph. In the definitions, SL converts a list to a set, and CONS adds an element to a list. MAP applies a function to each element of a list, and gathers the results of all the applications into a new list which is the value yielded. FLAT takes a list of lists and appends them together, to "flatten" the structure into a single level, a list of elements from all the lists. The purpose of the graph analysis is to verify that the progress specified in the recurses with clause for each procedure is achieved for every possible recursive call of the procedure. The general process is to begin at a particular node of the call graph, and explore backwards through the directed arcs of the graph. The recursion expression for that procedure is associated with that starting node, and this is the starting path expression. For each arc traversed backwards, the current path expression is transformed using the call.sub.-- progress function defined in Table 4.12, and the result yielded by call.sub.-- progress is associated with the new node reached along the arc. At each point the Verification Condition Generator 112 keeps track of the path of nodes from the current node to the starting node. This backwards exploration continues recursively, until the Verification Condition Generator 112 reaches a "leaf" node. A leaf node is one which is a duplicate of one already in the path of nodes to the starting node. This duplicate may match the starting node itself, or it may match one of the other nodes encountered in the path of the exploration. When a leaf node is reached, a verification condition is generated by the Verification Condition Generator 112. These will be explained in more detail later; for now it suffices to note that there are two kinds of verification conditions generated, depending on which node the leaf node duplicated. If the leaf node matched the starting node, then we generate an undiverted recursion verification condition. If the leaf node matched any other node, then the Verification Condition Generator 112 generates a diversion verification condition. extend.sub.-- graph.sub.-- vcs performs the task of tracing backwards across a particular arc of the procedure call graph.fan.sub.-- out.sub.-- graph.sub.-- vcs traces backwards across all incoming arcs of a particular node in the graph. The arguments to these functions have the following types and meanings:
______________________________________
p string current node (procedure name)
ps (string)list
path (list of procedure names)
p.sub.0
string starting node (procedure name)
q aexp current path condition
pcs string.fwdarw.aexp
prior path conditions
p env procedure environment
all.sub.-- ps
(string)list
all declared procedures (list of names)
n num depth counter
p' string source node of arc being
explored
______________________________________
The depth counter n was a necessary artifact to be able to define these functions in HOL; first fan.sub.-- out.sub.-- graph.sub.-- vcs was defined as a single primitive recursive function on n combining the functions of Table 4.11. Then extend.sub.-- graph.sub.-- vcs was defined as a mutually recursive part of fan.sub.-- out.sub.-- graph.sub.-- vcs, and fan.sub.-- out.sub.-- graph.sub.-- vcs resolved to the remainder. For calls of fan.sub.-- out.sub.-- graph.sub.-- vcs, n should be equal to the difference between the lengths of all.sub.-- ps and ps. For calls of extend.sub.-- graph.sub.-- vcs, n should be equal to the difference between the lengths of all.sub.-- ps and ps, minus one. The definition of fan.sub.-- out.sub.-- graph.sub.-- vcs maps extend.sub.-- graph.sub.-- vcs across all defined procedures, as listed in all.sub.-- ps. It is expected that practically speaking, most programs will have relatively sparse call graphs, in that there will be many procedures in the program, but each individual procedure will only be called by a small fraction of all defined. Therefore it is important for the application of extend.sub.-- graph.sub.-- vcs described above to terminate quickly for applications across an arc which does not actually exist in the procedure call graph. The lack of an arc is represented by the lack of a corresponding calls . . . with clause in the header of the procedure which would be the source of the arc. When assembling the calls progress environment calls from the calls . . . with clauses of a procedure, each clause produces a binding onto an initial default calls progress environment. This default calls progress environment is .lambda.p. false. Then all references to target procedures not specified in the calls . . . with clauses yield the default value of this default calls progress environment, false. This indicates that there is no relationship at all possible between the values in the states before and after such a call, and therefore signifies that such calls cannot occur. As a side benefit, this ensures that any omission of a calls . . . with clause from the header of a procedure whose body does indeed contain a call to the target procedure will generate verification conditions that require proving false, and these will be quickly identified as untrue. An invocation of extend.sub.-- graph.sub.-- vcs will at its beginning call the call.sub.-- progress function. call.sub.-- progress will evaluate calls p.sub.2 to extract the progress expression. For a nonexistent arc, this will be false, as described above. The definition of call.sub.-- progress then tests whether the progress expression is equal to false. For such a nonexistent arc in the procedure call graph, it is, and call-progress then immediately terminates with value true. The invocation of extend.sub.-- graph.sub.-- vcs then receives true as the current path condition. The next step of extend.sub.-- graph.sub.-- vcs is to test whether the path condition is equal to true. Since it is, the definition of extend.sub.-- graph.sub.-- vcs then immediately terminates, yielding an empty list with no verification conditions as its result. In theory these functions could have been designed more simply and homogeneously to yield equivalent results just using the parts of each definition which handle the general case. However, this would not have been a practical solution. All these functions are designed with particular attention to as quickly as possible dismiss all nonexistent arcs of the procedure call graph. This is critical in practice, because of the potentially exponential growth of the time involved in exploring a large graph. This rapid dismissal limits the exponential growth to a factor depending more on the average number of incoming arcs for nodes in the graph, than on the total number of declared procedures. The fan.sub.-- out.sub.-- graph.sub.-- vcs function is called initially by the function graph.sub.-- vcs. graph.sub.-- vcs is presented in Table 4.13. It analyzes the procedure call graph, beginning at a particular node, and generates verification conditions for paths in the graph to that node to verify its recursive progress, as designated in its recursion expression declared in the procedure's header. The graph.sub.-- vcs function is called by the function vcgg. vcgg is presented in Table 4.14. It analyzes the entire procedure call graph, beginning at each node in turn, and generates verification conditions for paths in the graph, to verify the recursive progress declared for each procedure in all.sub.-- ps. 4.1.5.1 Example of Verification of Call Graph As an example of this graph traversal algorithm, consider the odd/even program in Table 4.2. Its procedure call graph is illustrated in FIG. 2. The following examples explore this call graph, beginning at the node corresponding to procedure even. In this process, part of the structure of the procedure call tree rooted at even is traced, which is given in FIG. 3. The Verification Condition Generator 112 takes the recursion expression of even, n<n, and attaches that to the even node. This becomes the current path expression. Examining the call graph, it can be seen that there are two arcs coming into the even node, one from odd and one from even itself, as a self-loop. These will form two paths, which we will explore as two cases. Case 1: Path odd.fwdarw.even. The call graph arc goes from odd to even. The Verification Condition Generator 112 pushes the current path expression backwards across the arc from even to odd, using the function call.sub.-- progress. As previously described: ##EQU20## The Verification Condition Generator 112 attaches this path expression to the odd node. According to the definition of extend.sub.-- graph.sub.-- vcs, the Verification Condition Generator 112 then goes through a series of tests. The Verification Condition Generator 112 first tests to see if this path expression is true, which it clearly is not. If, however, there had been no arc in the procedure call graph from odd to even, then the call.sub.-- progress function would have returned true, and extend.sub.-- graph.sub.-- vcs would terminate, yielding an empty list of verification conditions for this path. The second test the Verification Condition Generator 112 encounters in the definition of extend.sub.-- graph.sub.-- vcs is whether the node just reached backwards across the arc is the same as the starting node. In this case, the node just reached is odd and the starting node is even, so this test is not satisfied. The third test the Verification Condition Generator 112 encounters is whether the node just reached, odd, is a duplicate of one of the nodes in the path to the starting node. In this case, the path only consists of the starting node even itself, and odd is not a duplicate of any member. The choice finally arrived at in the definition of extend.sub.-- graph.sub.-- vcs is to continue the graph exploration recursively, by calling fan.sub.-- out.sub.-- graph vcs. Considering the node odd in the procedure call graph in FIG. 2, it can be seen there are two arcs of the procedure call graph which enter the node odd, one from odd itself and one from even. These will form two paths, which we will explore as two cases. Case 1.1: Path odd.fwdarw.odd.fwdarw.even. The Verification Condition Generator 112 pushes the current path expression backwards across the arc from odd to odd, using the function call.sub.-- progress. As previously described: ##EQU21## This becomes the current path expression. The Verification Condition Generator 112 then goes through the series of tests in the definition of extend.sub.-- graph.sub.-- vcs. The Verification Condition Generator 112 first tests to see if this path expression is true, which it clearly is not. The second test is whether the node just reached backwards across the arc is the same as the starting node. In this case, the node just reached is odd and the starting node is even, so this test is not satisfied. The third test is whether the node just reached, odd, is a duplicate of one of the nodes in the path to the starting node. In this case, this path is odd.fwdarw.even, so odd is a duplicate, and this test succeeds. According to the definition of extend.sub.-- graph.sub.-- vcs, for satisfying this test, the Verification Condition Generator 112 generates a verification condition of the form pcs pq.sub.1, which in this case is: ##EQU22## This kind of verification condition is called a diversion verification condition, which is described in more detail later. This terminates this exploration of this path (Case 1.1) through the procedure call graph. Case 1.2: Path even.fwdarw.odd.fwdarw.even. The Verification Condition Generator 112 pushes the current path expression backwards across the arc from odd to even, using the function call.sub.-- progress. As previously described: ##EQU23## This becomes the current path expression. The Verification Condition Generator 112 then goes through the series of tests in the definition of extend.sub.-- graph.sub.-- vcs. The Verification Condition Generator 1 12 first tests to see if this path expression is true, which it clearly is not. The second test is whether the node just reached backwards across the arc is the same as the starting node. In this case, the node just reached is even and the starting node is even, so this test succeeds. According to the definition of extend.sub.-- graph.sub.-- vcs, for satisfying this test, the Verification Condition Generator 112 generates a verification condition of the form: ##EQU24## which in this case is: ##EQU25## This kind of verification condition is called an undiverted recursion verification condition, which is described in more detail later. This terminates this exploration of this path (Case 1.2) through the procedure call graph. Since this is also the last case for expanding the path of Case 1, this also terminates the exploration of that path. Case 2: Path even.fwdarw.even. The call graph arc goes from even to even. The Verification Condition Generator 112 pushes the current path expression backwards across the arc from even to even, using the function call.sub.-- progress. As previously described: ##EQU26## This becomes the current path expression. The Verification Condition Generator 112 then goes through the series of tests in the definition of extend.sub.-- graph.sub.-- vcs. The Verification Condition Generator 112 first tests to see if this path expression is true, which it clearly is not. The second test is whether the node just reached backwards across the arc is the same as the starting node. In this case, the node just reached is even and the starting node is even, so this test succeeds. According to the definition of extend.sub.-- graph.sub.-- vcs, for satisfying this test, the Verification Condition Generator 112 generates a verification condition of the form: ##EQU27## which in this case is: ##EQU28## This is another undiverted recursion verification condition. This terminates this exploration of this path (Case 2) through the procedure call graph. Since this is also the last case, this also terminates the exploration of the procedure call graph for paths rooted at even. This ends the example. 4.1.6 Verification of Programs The mkenv function is presented in Table 4.15. This function has type decl.fwdarw.env.fwdarw.env. mkenv takes a declaration and an environment, and returns a new environment containing all of the declarations of procedures present in the declaration argument, overriding the declarations of those procedures already present in the environment. The proc.sub.-- names function is presented in Table 4.16. This function has type decl.fwdarw.(string)list. proc.sub.-- names takes a declaration, and returns the list of procedure names that are declared in the declaration. vcg is the main Verification Condition Generator function presented in Table 4.17. vcg calls vcgd to analyze the declarations, vcgg to analyze the call graph, and vcgc to analyze the main body of the program. vcg takes a program and a postcondition as arguments, analyzes the entire program, and generates verification conditions whose proofs are sufficient to prove the program totally correct with respect to the given postcondition. mkenv creates the procedure environment that corresponds to a declaration using the empty procedure environment po (with all procedures undeclared), and g.sub.0 is the "empty" calls progress environment .lambda.p. true. 4.2 Verification Conditions In the functions presented above, the essential task is constructing a proof of the program, but this proof is implicit and not actually produced as a result. Rather, the primary results are verification conditions, whose proof verifies the construct analyzed. In ›Gri81!, Gries gives an excellent presentation of a methodology for developing programs and proving them correct. He lists many principles to guide and strengthen this process. The first and primary principle he lists is: Principle: A program and its proof should be developed hand-in-hand, with the proof usually leading the way. In ›AA78!, Alagic and Arbib establish the following method of top-down design of an algorithm to solve a given problem: Principle: Decompose the overall problem into precisely specified subproblems, and prove that if each subproblem is solved correctly and these solutions are fitted together in a specified way then the original problem will be solved correctly. Repeat the process of "decompose and prove correctness of the decomposition" for the subproblems; and keep repeating this process until reaching subproblems so simple that their solution can be expressed in a few lines of a programming language. We would like to summarize these in our own principle: Principle: The structure of the proof should match the structure of the program. In the past, verification condition generators have concentrated exclusively on the structure of the syntax of the program, decomposing commands into their subcommands, and constructing the proof with the same structure based on the syntax, so that the proof and the program mirror each other. That tradition is continued in this work, but we also recognize that an additional kind of structure exists in programs with procedures, the structure of the procedure call graph. This is a perfectly valid kind of structure, and it provides an opportunity to structure part of the proof of a program's correctness. In particular, it is the essential structure used to prove the recursive progress claims of procedures. In our opinion, wherever a natural and inherent kind of structure is recognized in a class of programs, it is worth examining to see if it may be useful in structuring proofs of properties about those programs. Such structuring regularizes proofs and reduces their ad hoc quality. In addition, it may provide opportunities to prove general results about all programs with that kind of structure, moving a part of the proof effort to the meta-level, so that it need not be repeated for each individual program being proven. 4.2.1 Program Structure Verification Conditions The functions vcg1, vcgc, and vcgd are defined recursively, based on the recursive syntactic structure of the program constructs involved. An examination of the definitions of vcg1, vcgc, and vcgd (Tables 4.8, 4.9, 4.10) reveals several instances where verification conditions are generated in this analysis of the syntactic structure. The thrust of the work done by vcg1 is to transform the postcondition argument into an appropriate precondition, but it also generates two verification conditions for the iteration command. vcgc takes the verification conditions generated by vcg1, and adds one new one, making sure the giv | ||||||