Proof Movie II: A Proof with PVS

Incomplete D R A F T

John Rushby Computer Science Laboratory SRI International Menlo Park CA 94025 USA

February 7, 1994

Abstract

Debora Weber-Wulff [5] describes the development of a formal specification and verification for a simple add-assign compiler using the Boyer-Moore prover. Her purpose was to record and describe (as a “Proof Movie”) an example of the iterative process by which an expert user (in this case, Bill Young of CLInc) develops a formal specification and proof—including the discovery and correction of unproductive paths, missing lemmas, overlooked cases and so on. In this report, I describe the formal specification and verification of the same problem using the PVS system [2]. However, my purpose in describing this exercise is slightly different to that of Weber-Wulff: I use it as a vehicle to highlight some of the differences in approach that follow from using a strongly-typed logic and an interactive theorem prover (such as PVS), compared with an untyped logic and an automatic prover (such as Boyer-Moore). By rendering rather abstract issues in a concrete form, this direct comparison is intended to expose the underlying design choices in a readily understandable form. In addition, this exercise is also intended as a tutorial for those who wish to learn about some of the more advanced features of PVS, including recursive definitions and inductive proofs, datatypes and their inductions, disjoint union types, record-extensionality, and user-customized proof-strategies.

Contents

1 The Problem 3

2 Specification in PVS 4 2.1 Terms and the Environment . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Programs, Semantics, and the Compiler . . . . . . . . . . . . . . . . . . . . 14 2.3 Typechecking the Specification and Proving the TCCs . . . . . . . . . . . . 19

3 Verification 31 3.1 Theorem correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.2 Lemma target append . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.3 Lemma correct step . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.4 Lemma correct expr . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 3.5 Lemma correct expression aux . . . . . . . . . . . . . . . . . . . . . . . . 47 3.6 Lemma good compile . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 3.7 Lemma independence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 3.8 Lemma prior value irrelevant . . . . . . . . . . . . . . . . . . . . . . . . 55 3.9 Lemma prior value irrelevant aux . . . . . . . . . . . . . . . . . . . . . 56

4 Summary 56 4.1 Proof Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 4.2 Proofchain Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 4.3 Proof Scripts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58 4.4 Typeset Specification Text . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 4.5 Cross-Reference to Specification Identifiers . . . . . . . . . . . . . . . . . . . 65

5 Conclusions 66

1 The Problem

The problem is described in detail by Weber-Wulff [5, pp. 122–125], so I merely sketch it here. The definitive specification is given by Weber-Wulff using “Meta IV style notation” []. The challenge is to verify the correctness of a “compiler” for a simple source language whose programs consist of sequences of statements of the form

V:=A_{1} + A_{2} + ⋯ + A_{n}

where n ≥ 1, V is a “variable,” and each of the A_{i}’s is either a variable different from V, or an integer constant.^{1}

The target code should consist of a sequence of instructions of one of the two forms:

  LOAD X, Y
  ADD  X, Y

where X is a variable, and Y is either a variable or a constant, with the intended interpretation that the first kind of instruction loads the value of Y into X, and the second adds the value of Y into that stored in X. In particular, the code compiled for the expression

V:=A_{1} + A_{2} + ⋯ + A_{n}

should have the form

  LOAD V, 0
  ADD  V, A 1
  ADD  V, A 2
      ...
  ADD  V, A n

Notice that the left hand side variable V is used as an accumulator, so the restriction that this variable not appear on the right hand side of a source language statement is crucial.

The semantics of the source and target languages are specified in terms of the effects that the elements of each have on their “environment,” which is a state recording the (integer) value associated with each variable. The goal of the formal specification and verification exercise is to formalize the semantics of the source and target languages, then to specify the operation of a compiler, and to prove that the target code compiled from a source program has the same effect on its environment as that given by the semantics for the original source program. For example, the source program

1The problem as originally specified for an evaluation exercise by the European ProCos project allows only variables on the right hand side; also allowing literal integers to appear here is an extension introduced in the Boyer-Moore specification. I have retained this extension because it makes the exercise much more interesting—indeed it is really the only nontrivial part. (Actually, the Boyer-Moore version provided for only natural numbers; the extension to integers is a trivial variation introduced here.)

  X := 3
  Y := 2
  Z := X + 4 + X + Y

has the effect of modifying its environment so that the value recorded for variable X becomes 3, that for Y becomes 2, and that for Z becomes 12. The compiled code for this example (which contains obvious inefficiencies) is:

  LOAD X, 0
  ADD  X, 3
  LOAD Y, 0
  ADD  Y, 2
  LOAD Z, 0
  ADD  Z, X
  ADD  Z, 4
  ADD  Z, X
  ADD  Z, Y

and this must be shown to have the same effect as that given for the source program.

2 Specification in PVS

As in the Boyer-Moore version, I will represent the elements of source and target programs abstractly: for the general correctness issue, we do not need to be concerned with the exact lexical representation of source program text, nor the machine code representation of the target code. My basic approach, therefore, will be to represent source programs as lists of statements, and statements as records consisting of a left hand side, and a right hand side: the former being a variable and the latter a list whose elements are either variables or integer constants. Similarly, target code will consist of a list of instructions, which are themselves records comprising an op-code, a destination, and a source. The op-code is one of LOAD or ADD, the destination is a variable, and the source is either a variable, or an integer constant.

2.1 Terms and the Environment

In order to formalize this informal outline in PVS, we must start by identifying the type (i.e., domain of values) of the individual terms that can appear on the right hand side of a source statement, or in the second argument position of a target instruction. These terms can take one of two forms:

• A variable, whose value is determined by the current environment, or

• A constant, which is literal integer whose value is intrinsic in the constant itself.

In the untyped Boyer-Moore logic, all values are members of a single domain and predicates are used to recognize those that have particular attributes: thus, numberp recognizes whether its argument is a number, and listp recognizes lists. In this framework, there is no difficulty recognizing a class of values that are either numbers, or members of an environment (described later). In a strongly typed logic, however, constructions such as this pose quite a challenge if the type system lacks certain mechanisms. What is wanted here is a disjoint-union type: a type whose values are drawn from two distinguishable, disjoint domains. PVS provides a construction for defining such types using its datatype mechanism, but before I describe that construction I want to motivate and explain it by building it up “by hand” from more primitive mechanisms.

The technique I use is based on predicate subtypes: in PVS, types may have subtypes and those subtypes may be associated with predicates. If necessary, PVS generates proof obligations (called type correctness conditions, or tccs) to ensure that expressions satisfy the predicate associated with their type. For example, the signature for the division operation (on the reals) is specified by

   / : [real, nonzero_real -> real]

where

   nonzero_real: TYPE = { x : real | x /= 0 }^{2}

is a predicate subtype specifying the nonzero real numbers. This construction constrains division to nonzero divisors, so that a formula such as

   x /= y  =>  (y-x)/(x-y) < 0

requires the typechecker to discharge the tcc

   x /= y  =>  (x-y) /= 0

in order to ensure that the occurrence of division is well-typed. Notice that the “context” (x /= y) of the division appears as an antecedent in the proof obligation (thereby rendering it provable). tccs establish that the value of an expression does not depend on the value of a type-incorrect term. A PVS specification is not considered type-correct, and any theorems proved are considered incomplete, until all tccs have been discharged.

Returning to our compiler specification, we wish to specify that variables and constants are mutually disjoint and exhaustive subtypes of the type of the terms that may appear on the right hand side of a source language statement. We can do this by associating the type constant with an uninterpreted predicate is const? on the type term (itself uninterpreted) of all terms, and then associating the type variable with the predicate is var?, defined as the negation of is const?

2In PVS, the symbol /= expresses “not equal.”

   term: TYPE
   is_const?: pred[term]^{3}
   is_var?(t: term): bool = NOT is_const?(t)
   constant: TYPE = (is_const?)^{4}
   variable: TYPE = (is_var?)

Now let us consider how to define the function term value which will take a term and return its value. If the term is a variable, then its value is obtained by looking it up in the current environment—so first we need to consider the specification of an environment. In the Boyer-Moore specification described by Weber-Wulff, an environment is represented as an association list: a list of dotted pairs (i.e., in Lisp terminology, cons cells whose cdr is a simple value, not a list) relating variables to their values. Thus the dotted pair (V .

3) indicates that the variable V has the value 3. The Lisp function assoc for searching association lists is built-in to the Boyer-Moore prover. The association list provides a representation in which an environment is essentially a partial function from variables to integer values: it is partial because not all variables need have an entry in the association list. The Boyer-Moore specification therefore defines a predicate definedp that checks whether a variable is defined in a given environment and the specification of source and target semantics requires that source programs and target instructions are only evaluated in environments that do define values for the variables referenced.

We could follow this construction in PVS, but I prefer to model the environment as a total function from the variables to integers.

   env: TYPE = [variable -> int]^{5}

which means that each variable has a value in every environment. This seems to be the interpretation intended in the statement of the problem: there is no requirement to model the declaration of variables nor the visibility rules of, say, a block structured language. Rather, the intent of this problem seems to be to examine the correctness of an add-assign compilation algorithm.

Formal specification and verification is generally undertaken in order to examine some element of a larger problem that is considered particularly challenging. This purpose is best achieved, in terms of both clarity and economy, if attention is focussed on the main element, and all peripheral issues are treated as abstractly and as simply as possible (provided, of course, that they are truly peripheral—a judgment that requires skill and experience). Here, I judge the definedness of variables in an environment to be irrelevant to the main problem and therefore prefer the total function representation of environments (though it would be straightforward to model partial environments, if desired^{6}). The pragmatic advantage of this choice is that assigning a newly computed value to the left hand side of a source language statement, or to the destination of a target language instruction, will be accomplished by function overriding (also called function modification or updating), for which the PVS theorem prover provides complete mechanization. In contrast, the association list approach will require the definition of a new function (put-assoc in the Boyer-Moore specification) to specify assignment, and then necessitate several lemmas to be stated and proved in order to establish properties of the construction.

3The expression pred[term] denotes the type of predicates over the type term. It is a shorthand (defined in the “prelude” of preloaded PVS theories) for the function type [term -> bool].

4A predicate enclosed in parentheses denotes its corresponding predicate subtype. This particular declaration is therefore a shorthand for the declaration constant: TYPE = { x: term | is const?(x)}.

5The type int is a shorthand for the built-in type integer. Note also that all functions are total in PVS.

6The Boyer-Moore specification does not provide a way to add new variables to the environment, so the set of defined variables is defined by the initial environment. This partial function approach is therefore no different to the total function approach when the intended interpretation of the type variable as just the defined variables.

Given the decisions described above on the representation of terms and environments, we can specify the value of the function term val(t, e), where t is a term, and e is an env, to be e(t) in the case that is var?(t) is satisfied (i.e., when t is a variable).

   temporary: AXIOM FORALL (t:term): is_var?(t) => term_val(t, e) = e(t)

But what of the case is const?(t) (i.e., where t is a constant)? We really want t to be its own value in this case (i.e., we want t to be an integer), but this is not possible directly: values of the subtype constant are uninterpreted—they have no properties other than being distinguishable from values of the subtype variable—and so we cannot make them be the integers. However, we can specify that they be in correspondence with the integers, so that it is possible to transfer from an integer to a constant and back again to the original integer. We do this by means of functions mk const, and const val and an axiom which asserts that the latter is a left inverse for the former (so that the former is a surjection).

   mk_const: [int -> constant]
   const_val: [constant -> int]
   inv: AXIOM FORALL (x:int): const_val(mk_const(x)) = x

With this construction, we can delete the temporary axiom above and write the specification for the function term val as follows.

   term_value(t: term, e: env): int =
     IF is_var?(t) THEN e(t) ELSE const_val(t) ENDIF

The construction just described is perfectly legitimate, but PVS provides a built-in mechanism that allows us to achieve the same effect with less invention and greater economy. The mechanism concerned is the PVS datatype construction (which resembles, and was inspired by, the Boyer-Moore “shell” construction [1]).^{7} Before describing how to use the datatype mechanism to construct a disjoint union, however, I will first describe its more usual application—which is the specification of recursively structured data types such as lists and trees.

7The “free types” of Z [4] are similar.

2.1.1 Lists and the PVS Datatype Mechanism

Since we are going to need lists in order to specify source language programs as lists of statements and so on, I will use the list datatype as my example. The idea of a PVS datatype is that it is a collection of mutually disjoint subtypes, each of which is associated with a predicate called its recognizer, and a function called a constructor that builds values of that subtype. A constructor will generally take arguments, some of which may be of the datatype being defined (hence the recursion); in all cases, the types of the arguments must be specified, along with the name of its accessor, which is the function that will be used to extract that component from a value of the subtype concerned. To see how this works, here is the specification of the list datatype exactly as it appears in the PVS prelude (which means it is automatically pre-loaded into PVS and need not be defined by the user).

   list[t:TYPE] : DATATYPE
    BEGIN
     null: null?
     cons (car: t, cdr: list): cons?
    END list

This specification introduces the datatype list, parameterized by some arbitrary type t (this means we can instantiate the datatype to obtain lists of integers, or lists of “statements,” each of which is a distinct type). The line

   cons (car: t, cdr: list): cons?

says that one subtype of the lists is recognized by the predicate cons? and constructed by the function cons, which takes two arguments: one of type t and the other which is a list. If l is of type (cons?)^{8}, then its first component can be retrieved by car(l), and its second by cdr(l).

The other line in the body of the datatype specification

   null: null?

says that the other subtype of list is recognized by null?, and constructed by the function of no arguments (i.e., a constant) null.

When the PVS typechecker processes a datatype specification, it “expands” it into a collection of ordinary PVS definitions and axioms that specify the semantics of the abstract data type concerned. For the datatype specification foo, PVS generates the expanded theories foo adt and foo rec mod and places them in the file foo adt.pvs.^{9}

8Recall, a predicate name in parentheses denotes the corresponding subtype.

9Datatype specifications can appear either at the “top level” of a PVS specification (i.e., not within a theory), or nested within a theory. The “adt” file is generated only in the former case. The same structures are generated internally in the latter case and can be viewed using the PVS Emacs command M-x ppe (prettyprint-expanded).

The expanded set of definitions and axioms generated in the “adt” file contains nothing that the user could not have entered directly. One advantage of letting PVS generate them is that we guarantee that the set of axioms generated is consistent—so that datatypes provide only conservative extension and are therefore considered a definitional form in PVS. The second advantage in using datatype specifications, rather than providing an equivalent axiomatization, is that the PVS theorem prover provides very powerful automation for constructions known to have been generated from a datatype specification. Let us look at the specification file list adt.pvs generated from list datatype given earlier. The file begins as follows.

   list_adt[t: TYPE]: THEORY
     BEGIN
     list: TYPE
     null?, cons?: [list -> boolean]
     null: (null?)
     cons: [t, list -> (cons?)]
     car: [(cons?) -> t]
     cdr: [(cons?) -> list]

These declarations establish the types of the recognizers, constructors, and accessors in the manner informally described earlier. Skipping over some declarations that we will return to shortly, the adt file continues with the axioms that specify the relationship between the constructor cons and its accessors car and cdr.

   car_cons:
     AXIOM
       (FORALL (cons1_var: t), (cons2_var: list):
          car(cons(cons1_var, cons2_var)) = cons1_var)
   cdr_cons:
     AXIOM
       (FORALL (cons1_var: t), (cons2_var: list):
          cdr(cons(cons1_var, cons2_var)) = cons2_var)

The axioms I skipped over are the extensionality axioms for null and cons and the eta axiom for cons.

   null_extensionality:
     AXIOM
       (FORALL (null?_var: (null?)), (null?_var2: (null?)):
          null?_var = null?_var2)
   cons_extensionality:
     AXIOM
       (FORALL (cons?_var: (cons?)), (cons?_var2: (cons?)):
          car(cons?_var) = car(cons?_var2) AND cdr(cons?_var) = cdr(cons?_var2)
            IMPLIES cons?_var = cons?_var2)
   cons_eta:
     AXIOM
       (FORALL (cons?_var: (cons?)):
          cons(car(cons?_var), cdr(cons?_var)) = cons?_var)

The first of these says that null is the unique constant of type (null?); the second says two (cons?)’s are the same if their car and cdr are; the third says that a (cons?) is the same as the cons of its car and cdr (although this is listed as an axiom, it can actually be proved from extensionality).

The next axiom says that all lists are either null? or cons?.

   list_inclusive:
     AXIOM (FORALL (list_var: list): null?(list_var) OR cons?(list_var))

There should also be an axiom that asserts that the recognizers are pairwise disjoint. However, this axiom has n×(n−1) clauses (where the datatype has n different recognizers), which rapidly becomes excessive,^{10} so instead the effect of this axiom is built-in to the PVS prover and the axiom is not constructed explicitly. (Pairwise disjointness is implicit in the semantics of the CASES construct introduced below; it can be proved explicitly from

cons eta using CASES.)

The next axiom supplies a principle of structural induction for lists.

   list_induction:
     AXIOM
       (FORALL (p: [list -> boolean]):
          p(null)
            AND
            (FORALL (cons1_var: t), (cons2_var: list):
               p(cons2_var) IMPLIES p(cons(cons1_var, cons2_var)))
            IMPLIES (FORALL (list_var: list): p(list_var)))

10Datatypes are the mechanism that implements the enumeration types of PVS. It is quite common to encounter enumerations with 30 or more constants—which would lead to disjointness axioms having over 900 clauses.

It says that to prove something for all lists, it is enough to prove it for null and, assuming it is true for an arbitrary list l, prove that it is also true for cons(x, l), where x is of type t. (Incidentally, list inclusive, although stated as an axiom, can be proved from list induction.) The PVS prover provides strategies for performing proofs by induction. These strategies automatically select an induction scheme based on the type of the induction variable (the user can override this if a nonstandard induction scheme—such as induction over a finite segment of the natural numbers—is required). Thus, induction on a variable if type list will automatically use the list induction axiom.

The next axiom is rather tricky. First, let me explain why it is needed. We are obviously going to want to write some functions that operate on lists, and it is likely that most of those functions will be recursive. Now recursive definitions in PVS must be shown to terminate^{11}, and the way this is done is by specifying a measure function with each recursive function definition. A measure function is one that takes the same arguments as the function being defined recursively, but whose range type is the natural numbers (or the sub-ϵ_{0} ordinals in the transfinite case). PVS generates proof obligations that require demonstration that the “size” of the arguments (as given by the measure function) decreases across recursive calls. For most operations that operate on lists, the obvious measure function to use is the function that gives the length of the list argument. The length function can itself be specified recursively as follows (note, we will see a better way to specify this shortly).

   length(l:list[t]): RECURSIVE nat =
      IF null?(l) THEN 0 ELSE 1 + length(cdr(l)) ENDIF

but what can we use as the measure function to show that this definition terminates? It is to solve this dilemma that the following definition is provided in the adt file.

   list_nat_rec((null?_fun: nat), (cons?_fun: [t, nat -> nat])): [list -> nat]
       = LAMBDA (list_var: list):
           CASES list_var OF
             null: null?_fun,
             cons(cons1_var, cons2_var):
                 cons?_fun(cons1_var,
                           list_nat_rec(null?_fun, cons?_fun)(cons2_var))
           ENDCASES

This definition introduces a higher-order recursive function called list nat rec that is known to terminate (by metatheoretic arguments) without a measure function being required.^{12} Of course, we could have made the length function serve as this base measure, but list nat rec is used instead because it is more general.

11Definitions provide conservative extension in PVS (i.e., they are guaranteed not to introduce (new)

inconsistencies). No guarantees are given concerning axioms.

12Because it lacks a measure function, this definition could not be provided by the user—contradicting my earlier statement that there is nothing in the adt file that the user could not have created directly.

However, it is only as a definition (with its guarantee of conservative extension) that this is unacceptable; a recursion without a measure function can be specified axiomatically with the user taking responsibility for the termination argument.

The specification of list nat rec uses the CASES construct, whose availability is another of the advantages of the datatype facility in PVS. The CASES construct provides a way to specify by cases over the constructors of a datatype, with variables in place of the arguments (thereby eliminating the need to use the accessors to reference components). Thus, our definition of the length function can be rewritten as

   length(l:list[t]): RECURSIVE nat =
      CASES l OF
        null: 0;
        cons(x, y): 1 + length(y)
      ENDCASES

Notice how in the second clause, the (implicitly defined) local variables x and y stand for car(l) and cdr(l), respectively. The CASES construct makes for clearer and more concise specifications, and its treatment by the theorem prover is highly automated.

We can now read the specification of list nat rec. This function takes two functions as its arguments (that is why I called it “higher-order” earlier: a higher-order function is one that takes other functions as arguments and/or returns them as values); the first takes null and returns a natural number, the second takes a t and a natural number and returns a natural number. The idea is that these functions tell us the “size” of (null?) and (cons?) lists respectively (intuitively, the second argument to the second function will be the “size” of the cdr of the corresponding list). The function list nat rec is then defined recursively to yield a function that gives the size of its argument. Thus, another way to specify the length function on lists is

   length(l:list[t]): nat = list_nat_rec(0, (LAMBDA (x:t),(n:nat): n+1))(l)

This definition is a little hard to read, however, so the length function is actually defined (in the PVS prelude theory list props ) in the “natural” recursive manner, with the right hand side of the definition above providing its measure:

   list_props[t:TYPE] : THEORY
    BEGIN
     length(l:list[t]): RECURSIVE nat =
       CASES l OF
         null: 0,
         cons(x,y): length(y) + 1
       ENDCASES
       MEASURE list_nat_rec(0, (LAMBDA (x: t), (n: nat): n + 1))

While we are looking at the theory list props from the PVS prelude, we should also take note of the definition of the function every, which returns true if and only if every element of the list supplied as its second argument satisfies the predicate supplied as its first argument.

   every(p: pred[t], l: list[t]): RECURSIVE bool =
     CASES l OF
       null: true,
       cons(x, y): p(x) & every(p, y)
     ENDCASES
     MEASURE (LAMBDA (p: pred[t]), (l: list[t]): length(l))

Notice that now we have the length function available, we can use it to provide the heart of the measure function.

To finish up our examination of the expanded datatype theory list adt, I will simply observe that its final axiom, list ordinal rec is similar to list nat rec, but uses the ordinals instead of the naturals. Following the theory list adt, the file list adt.pvs provides the theory list rec mod, which contains the definition of a function list rec that is similar to list nat rec and list ordinal rec, except that it allows an arbitrary type to be used in place of the natural numbers and ordinals.

2.1.2 Disjoint Unions as PVS Datatypes

Returning at last to our original problem of specifying the type term as the disjoint union of the types variable and integer, we see that this can be accomplished with the datatype declaration

   variable: TYPE
   env: TYPE = [variable -> int]
   term: DATATYPE
   BEGIN
    mk_var(var_val: variable): is_var?
    mk_const(const_val: int): is_const?
   END term

This gives us exactly the same construction as that which we previously defined “by hand,” except that terms of type variable are constructed and accessed by the functions mk var and var val, whereas previously we were able (implicitly) to use the identity function for these purposes. Thus, our definition for the function term val now needs to be adjusted slightly (we need e(var val(t)) instead of just e(t) in the THEN clause).

   term_value(t: term, e: env): int =
     IF is_var?(t) THEN e(var_val(t)) ELSE const_val(t) ENDIF

However, since term is now defined as a datatype, the definition of term val is more conveniently written using the CASES construct.

   term_value(t: term, e: env): int =
     CASES t OF
       mk_var(v): e(v),
       mk_const(i): i
     ENDCASES

The techniques I have used to specify the type term and the function term val seem— and indeed are—much more complicated than those needed in the Boyer-Moore specification (though, of course, much of the complexity of the description was due to my wish to explain the PVS datatype facility in its general form). However, the complexity is in the concepts provided by PVS, not in the specification text itself. The PVS specification is 12 lines long; the Boyer-Moore specification requires 5 lines to specify term-value, but needs and additional 13 lines to define the auxiliary functions put-assoc and definedp.

The benefits gained by using a typed logic are that strong error detection can be performed early in the analysis—during typechecking—so that time is not wasted in trying to prove type-incorrect “theorems” later on. For example, Weber-Wulff describes [5, page 135] a failed proof attempt using the Boyer-Moore prover that was traced to a failure to prove the “seemingly obvious relationship” (equal (plus n 0) n), which turns out to be false if n is a list, rather than a number. Cases such as this cannot even be formulated in a typed logic: the error is detected in typechecking, rather than through failed proof attempts.

2.2 Programs, Semantics, and the Compiler

2.2.1 The Source Language

Having specified the type term that is basic to both the source and target languages, we next need to specify source and target programs, and their semantics. The first step is to specify an individual source language statement. Recall that these are assignment statements, with a variable on the left hand side, and a sum of terms on the right hand side. This structure is easily specified in PVS as a record.

   crude_source_stmt: TYPE = [# lhs: variable, rhs: list[term] #]

The [# … #] construction introduces a record type in PVS; here lhs and rhs are the field identifiers, and the values of the corresponding fields in a constant or variable s of type are accessed by lhs(s) and rhs(t), respectively.^{13} The construction list[term] identifies the type list from the generic lists datatype, instantiated with list elements of type term.^{14}

In the introduction, I mentioned that it is important that the variable on the left hand side of a source language statement should not appear in the right hand side. It is also necessary that the right hand side should not be the empty list, since it is not clear what a statement of the form “A := ” could be intended to mean.

We can specify both of these restrictions by means of a predicate good source stmt?

on the type crude source stmt.

13This is in distinction to the more common field selection syntax s.lhs and s.rhs.

14The full syntax for this type is lists[term].list; a shorthand permits the theory name to be dropped and the entity name to be moved to the front when no ambiguity results.

   good source stmt?(s: crude_source_stmt): bool =
     NOT null?(rhs(s))
       AND every((LAMBDA t: is_var?(t) => var_val(t) /= lhs(s)), rhs(s))

This specification uses the predicate every introduced in the list props theory described earlier (on page 12).

In PVS, subtypes can be associated with predicates. It is convenient to do this here, defining source stmt to be the subtype of crude source stmts satisfying the

good source stmt? predicate.^{15}
   source_stmt: TYPE = (good_source_stmt?)

Given statements, we can specify source language programs as lists of statements.

   source_prog: type = list[source_stmt]

It is worth comparing this specification with the Boyer-Moore version. Because the Boyer-Moore logic is untyped, it is not possible to directly specify a source program, say, as a list of source statements: there is no way to say “a list of x.” Instead, it is necessary to program recognizers (i.e., predicates) for each kind of object. Thus a source program is recognized by the recognizer legal-source-program, which is a recursive function that takes an arbitrary argument x and an environment: if x is not a cons cell it is legal only if it is nil, otherwise we require that (cdr x) is a legal-source-program and that (car x) is legal-source-statement. This last is a regognizer for source statements and is defined in terms of more primitive recognizers for variables and exclusive-var-lists and so on.

It is worth noting, too, that the specification that served as the starting point for the Boyer-Moore treatment [5, page 122] uses similar recursively-defined recognizers for legal source programs and statements—despite being couched in a realatively rich specification language. This “Meta IV style notation” [], which was the precursor to VDM [?], is typed but lacks constructions for parameterized abstract data types such as lists, and also lacks predicate subtypes. The simplicity of the PVS specification illustrates some of the power and convenience of adding these constructions to a strongly-typed specification notation.

The next step is to specify a semantics for source programs and statements. The intent is that the meaning of a source language statement should be defined by its effect on the environment; the sum denoted by the right hand side of the statement is evaluated in the current environment (which supplies values for any variables in the right hand side), and the environment is then updated so that the sum just evaluated is recorded as the value of the variable appearing on the left hand side of the statement. Now it seems clear that the sum denoted by a right hand side will need to be specified by a recursion on the structure of the right hand side. Thus, before we can specify the semantics of a statement, we need to specify this recursion. We do this by the function source rhs val, which takes an arbitrary list of terms (not constrained to be non-null), and an environment, and returns the integer value corresponding to the sum of the terms in the list, evaluated in the given environment.

15Another way to specify source statement would be as a dependent tuple-type, in which the type of the rhs would be non-empty lists over terms excluding the lhs variable.

   source_rhs_val(l: list[term], e: env): RECURSIVE int =
     CASES l OF
       null: 0,
       cons(t, expr): source_rhs_val(expr, e) + term_value(t, e)
     ENDCASES
     MEASURE (LAMBDA (l: list[term]), (e: env): length(l))

Now it is easy to specify the interpretations of source language statements and programs:

   source_stmt_interp(s: source_stmt, e: env): env =
     e WITH [(lhs(s)) := source_rhs_val(rhs(s), e)]
   source_interpreter(p: source_prog, e: env): RECURSIVE env =
     CASES p OF
       null: e,
       cons(stmt, rest): source_interpreter(rest, source_stmt_interp(stmt, e))
     ENDCASES
     MEASURE (LAMBDA (p:source_prog), (e:env) : length(p))

The WITH clause appearing in this specification is the PVS notation for function, tuple, and record overriding. In the case of functions, a construction such as f WITH [(x) := y] is a function that has the same values as f, except that for argument x it has value y:

  f WITH [(x) := y] (z) = IF x=z THEN y ELSE f(z) ENDIF

The Meta IV, Boyer-Moore, and PVS specifications for the source-language semantics are very similar to each other: all use two recursive functions. The Meta IV and PVS specifications are able to use built-in pattern-matching on list constructors and function overriding on the environment, whereas the Boyer-Moore descriptions use explicit cars, cdrs, and a user-defined put-assoc function. The Boyer-Moore version allows the right hand side of a source statement to be empty (the interpretation is a “no-op”) because “it makes for simpler proofs with NQTHM [the Boyer-Moore prover] when properties are defined for empty lists as well” [5, page 129]. The Boyer-Moore specification lacks a definition corresponding to source stmt interp: the expression corresponding to the definition of its body appears directly in the function corresponding to source interpreter. Overall, the lengths of the specifications for the source language and its semantics are 24, 37, and 20 lines for the Meta IV, Boyer-Moore, and PVS versions, respectively.

2.2.2 The Target Language

The next step is to perform the corresponding constructions for target language instructions and programs. We need two “op-codes” to distinguish the two kinds of target language instructions (load and add). We specify these using a PVS enumerated type

   opcode: TYPE = {LOAD, ADD}

Then we can say that a target instruction is a record consisting of an op-code, a destination (which is a variable), and a source value, which is a term:

   target_instr: TYPE = [# op: opcode, dest: variable, src: term #]

The semantics of target instructions will be specified by cases: for a LOAD instruction, the effect is to update the environment so that the value recorded for the destination is the value of the source term; for an add instruction, the environment is to be updated so that the value recorded for the destination is the sum of its value in the original environment plus value of the value of the source term.

   target_instr_interp(i:target_instr, e: env):env =
     e WITH [(dest(i)) := CASES op(i) OF
                            LOAD: term_value(val(i), e),
                            ADD:  e(dest(i)) + term_value(val(i), e)
                          ENDCASES]

Now we can specify a target program as a list of target instructions, and can specify the interpretation of a target program by recursively composing the interpretation of the individual steps from left to right.

   target_prog: type = list[target_instr]
   target_interpreter(t:target_prog, e: env): RECURSIVE env =
     CASES t OF
       null: e,
       cons(instr, rest): target_interpreter(rest, target_instr_interp(instr, e))
     ENDCASES
     MEASURE (LAMBDA (t:target_prog), (e:env): length(t))

Comparisons between the Meta IV, Boyer-Moore, and PVS specifications for the target language and its semantics are similar to those for the corresponding source language specifications. The lengths of the specifications for the target language and its semantics are 30, 38, and 14 lines, for Meta IV, Boyer-Moore, and PVS, respectively.

2.2.3 The Compiler

Our task now is to specify a compiler from source to target language programs. The basic idea is that for each source language statement the compiler will generate a load instruction to initialize the left hand side variable to 0, followed by a series of add instructions that add each of the terms on the right hand side into the left hand side variable. The series of additions will be constructed by recursing on the structure of the right hand side, so we need to specify this first. The function generate adds takes a variable and a list of terms and generates a target program consisting of a series of add instructions.

   generate_adds(target: variable, l: list[term]): RECURSIVE target_prog =
     CASES l OF
       null: null,
       cons(t, rest): cons( (# op := ADD, dest := target, src := t #),
                            generate_adds(target, rest))
     ENDCASES
     MEASURE (LAMBDA (target: variable), (l: list[term]): length(l))

The (# … #) construction is the PVS syntax for a literal constant of record type.

To compile a source language statement, we simply need to generate a load instruction to initialize the left hand side variable to 0, then follow it with the code compiled by

generate adds:
   compile_stmt(s: source_stmt): target_prog =
     cons( (# op := load, dest := lhs(s), src := mk_const(0) #),
           generate_adds(lhs(s), rhs(s)))

Finally, to compile a source language program, we simply need to join together the target programs generated for each of its individual statements. Since target programs are lists, we need the append function on lists in order to join them together. This function ought to be defined in the list props theory from the PVS prelude, but is missing at present. Consequently, I give a definition for it here in a separate theory list aux.

   list_aux[t: TYPE]: THEORY
     append(l1,l2: list[t]): RECURSIVE list[t] =
       CASES l1 OF
         null: l2,
         cons(hd, tl): cons(hd, append(tl, l2))
       ENDCASES
       MEASURE (LAMBDA (l1,l2: list[t]): length(l1))
   END list_aux

Now we can specify the compiler in the obvious way:

   compiler(sp:source_prog): RECURSIVE target_prog =
     CASES sp OF
       null: null,
       cons(hd, tl): append(compile_stmt(hd), compiler(tl))
     ENDCASES
     MEASURE length

We have now assembled all the pieces necessary to specify the goal of the exercise: that is, correctness of the code generated by the compiler. Since both source and target language have the same terms and the same environment, the correctness goal is simply stated as the requirement that the environment resulting from interpretation of a source program in a given initial environment is the same as that resulting from interpretation in the same initial environment of the target program generated by the compiler from the given source program.

   correctness: THEOREM FORALL (sp: source_prog), (e: env):
     source_interpreter(sp, e) = target_interpreter(compiler(sp), e)

The specifications for the compiler and its correctness are very similar in Meta IV, Boyer-Moore, and PVS, requiring 24, 19, and 18 lines, respectively. (PVS requires an additional 8 lines to specify append; the Meta IV version does not specify the correctness criterion.)

2.3 Typechecking the Specification and Proving the TCCs

At this point, it seems prudent to collect together all the fragments of PVS we have written so far and to allow PVS to check them for syntactic and semantic errors. The specification fragments are shown in the Figures 1 to 3. For processing by PVS, they are concatenated together into a single file compiler.pvs.

The first step is to check the file for syntax errors. This is done by giving the Emacs command M-x parse.^{16} Assuming we have made no mistakes typing the specification into the file, The Emacs interface to PVS will simply report that it has parsed the two theories list aux and compiler. If there are errors, a pop-up error buffer will appear and the cursor will move to the location of the error. If this happens, we must fix the problem and parse again.

Once parsing is completed successfully, the next step is to typecheck the file using the command M-X tc (typecheck). Again, assuming there are no errors, PVS should report that it has typechecked the two theories, generating in the process 1 tcc for list aux, and 6 for compiler (tcc is short for “Typecheck Correctness Condition”). The language of PVS is sufficiently rich that type correctness is not algorithmically decidable; in certain circumstances, PVS generates a proof-obligation that must be discharged before the specification is considered type-correct. We can display the tccs for a theory by giving the command M-x show-tccs; those for the theory compiler are shown in Figure 4.

It can be seen that 5 of the 6 tccs are termination arguments for recursively-defined functions (as is the tcc—not shown—generated from the theory list aux), and that the other is concerned with demonstrating that the type source stmt is nonempty.

PVS provides a useful proof strategy called tcc that is able to discharge many tccs without assistance. It is applied automatically to all tccs that do not have a user-developed proof by the command M-X tcp (typecheck-prove). Unfortunately, the tcc strategy is unable to prove any of the tccs in this file. This deficiency will be fixed shortly, but it gives us an opportunity to develop some simple proofs by hand, and to learn how to reuse proofs and to develop our own proof strategies.

Let us start off with the first of the termination tccs

16PVS uses the Emacs screen-editor as its interface: the repertoire of Emacs commands is extended to include several dozen that invoke PVS operations, and results are returned in Emacs buffers.

20 2 SPECIFICATION IN PVS

%========= THE AUXILIARY LIST THEORY ================================
list_aux[t: TYPE]: THEORY
BEGIN
append(l1,l2: list[t]): RECURSIVE list[t] =
  CASES l1 OF
    null: l2,
    cons(hd, tl): cons(hd, append(tl, l2))
  ENDCASES
  MEASURE (LAMBDA (l1,l2: list[t]): length(l1))
END list_aux
%========= MAIN COMPILER THEORY ======================================
compiler: THEORY
BEGIN USING list_aux
%--------- TERMS (of both source and target languages) ----------------
variable: TYPE
term: DATATYPE
BEGIN
 mk_var(var_val: variable): is_var?
 mk_const(const_val: int): is_const?
END term
env: TYPE = [variable -> int]
term_value(t: term, e: env): int =
  CASES t OF
    mk_var(v): e(v),
    mk_const(i): i
  ENDCASES

continues…

Figure 1: The PVS Specification, Part 1 2.3 Typechecking the Specification and Proving the TCCs 21

%--------- SOURCE LANGUAGE --------------------------------------------
crude_source_stmt: TYPE = [# lhs: variable, rhs: list[term] #]
good_source_stmt?(s: crude_source_stmt): bool =
  every((LAMBDA (t: term): is_var?(t) => var_val(t) /= lhs(s)), rhs(s))
    AND NOT null?(rhs(s))
source_stmt: TYPE = (good_source_stmt?)
source_prog: TYPE = list[source_stmt]
source_rhs_val(l: list[term], e: env): RECURSIVE int =
  CASES l OF
    null: 0,
    cons(t, expr): source_rhs_val(expr, e) + term_value(t, e)
  ENDCASES MEASURE (LAMBDA (l: list[term]), (e: env): length(l))
source_stmt_interp(s: source_stmt, e: env): env =
  e WITH [(lhs(s)) := source_rhs_val(rhs(s), e)]
source_interpreter(p: source_prog, e: env): RECURSIVE env =
  CASES p OF
    null: e,
    cons(stmt, rest): source_interpreter(rest, source_stmt_interp(stmt, e))
  ENDCASES MEASURE (LAMBDA (p:source_prog), (e:env) : length(p))
%--------- TARGET LANGUAGE --------------------------------------------
opcode: TYPE = LOAD, ADD
target_instr: TYPE = [# op: opcode, dest: variable, src: term #]
target_instr_interp(i:target_instr, e: env): env =
  e WITH [(dest(i)) := CASES op(i) OF
                         LOAD: term_value(src(i), e),
                         ADD:  e(dest(i)) + term_value(src(i), e)
                       ENDCASES]
target_prog: TYPE = list[target_instr]
target_interpreter(t:target_prog, e: env): RECURSIVE env =
  CASES t OF
    null: e,
    cons(instr, rest): target_interpreter(rest, target_instr_interp(instr, e))
  ENDCASES MEASURE (LAMBDA (t:target_prog), (e:env): length(t))

continues…

Figure 2: The PVS Specification, Part 2

%------- COMPILER ----------------------------------------------------
generate_adds(target: variable, l: list[term]): RECURSIVE target_prog =
CASES l OF
  null: null,
  cons(t, rest): cons( (# op := ADD, dest := target, src := t #),
                       generate_adds(target, rest))
ENDCASES
MEASURE (LAMBDA (target: variable), (l: list[term]): length(l))
compile_stmt(s: source_stmt): target_prog =
cons( (# op := LOAD, dest := lhs(s), src := mk_const(0) #),
      generate_adds(lhs(s), rhs(s)))
compiler(sp: source_prog): RECURSIVE target_prog =
CASES sp OF
  null: null,
  cons(hd, tl): append(compile_stmt(hd), compiler(tl))
ENDCASES
MEASURE length
%------- VERIFICATION -----------------------------------------------
correctness: THEOREM FORALL (sp:source_prog), (e:env):
source_interpreter(sp, e) = target_interpreter(compiler(sp), e)
END compiler

Figure 3: The PVS Specification, Part 3

% Termination TCC generated (line 55) for source_rhs_val
% unproved
source_rhs_val_TCC1: OBLIGATION
(FORALL (expr, l : list[term]), (t : term):
  l = cons[term](t, expr) IMPLIES length[term](expr) < length[term](l))

Moving the cursor to this formula and typing the command M-x pr (prove) moves us to the interactive *pvs* buffer with the display

source_rhs_val_TCC1:
|-------
{1} (FORALL (expr, l : list[term]), (t : term):
     l = cons(t, expr) IMPLIES length(expr) < length(l))
Rule?

2.3 Typechecking the Specification and Proving the TCCs 23

% Existence TCC generated (line 46) for source_stmt
% unproved
source_prog_TCC1: OBLIGATION
  (EXISTS (x : crude_source_stmt) : good_source_stmt?(x))
% Termination TCC generated (line 55) for source_rhs_val
% unproved
source_rhs_val_TCC1: OBLIGATION
  (FORALL (expr, l : list[term]), (t : term):
    l = cons[term](t, expr) IMPLIES length[term](expr) < length[term](l))
% Termination TCC generated (line 67) for source_interpreter
% unproved
source_interpreter_TCC1: OBLIGATION
  (FORALL (p : source_prog), (rest : list[source_stmt]), (stmt : source_stmt):
    p = cons[source_stmt](stmt, rest)
     IMPLIES length[source_stmt](rest) < length[source_stmt](p))
% Termination TCC generated (line 97) for target_interpreter
% unproved
target_interpreter_TCC1: OBLIGATION
(FORALL (instr : target_instr), (rest, t : list[target_instr]):
  t = cons[target_instr](instr, rest)
     IMPLIES length[target_instr](rest) < length[target_instr](t))
% Termination TCC generated (line 109) for generate_adds
% unproved
generate_adds_TCC1: OBLIGATION
(FORALL (l : list[term]), (rest : list[term]), (t : term):
  l = cons[term](t, rest) IMPLIES length[term](rest) < length[term](l))
% Termination TCC generated (line 124) for compiler
% unproved
compiler_TCC1: OBLIGATION
(FORALL (hd : source_stmt), (sp : source_prog), (tl : list[source_stmt]):
   sp = cons[source_stmt](hd, tl)
     IMPLIES length[source_stmt](tl) < length[source_stmt](sp))

Figure 4: Typecheck Correctness Conditions for the Specification The PVS prover uses an interactive approach based on the sequent calculus: the user types a proof command at the Rule? prompt, the prover performs the indicated proof step and displays the result and waits for another command. Some steps cause the proof to branch; in this case the prover first follows the main branch, then returns to the subsidiary branches when the main one is complete. (The user can inspect the other branches and switch to them at any time.) The prover displays the current goal (a leaf of the proof tree) as a sequent: a list of negatively-numbered formulas (here empty) above the |------- line, and a list of positively-numbered formulas (here just the one numbered 1) below the line. The interpretation is that the conjunction of the formulas (called the antecedents) above the line should imply the disjunction of the formulas (called the succedents) below the line. When the prover recognizes that this is indeed so, that branch of the proof terminates and attention shifts to another branch of the proof. The proof is complete when all branches are terminated.

Unlike other PVS operations, which are invoked by Emacs commands, dialog with the PVS prover takes place in an interactive Lisp buffer: prover commands are typed directly into the buffer and the results are printed out into the same buffer PVS prover commands are written in Lisp syntax: (<cmd> <arguments>) where <cmd> is the name of the command, and <arguments> is an optional list of arguments (written without commas). The arguments may include numbers of specific formulas in the sequent, keyword arguments (written in the form :<key> <val>, where <key> is the name of the keyword argument, and <val> is the value to be assigned to it), and fragments of PVS specification text enclosed in quotes. The possible arguments to command <cmd> can be inspected by the command (help <cmd>). For example, here is the result of (help inst?).

   (inst? &optional <fnums[*]> subst <where[*]>  copy? if-match):
     Tries to automatically instantiate a quantifier.
     <fnums> indicates which quantified formula:  *,-, +, or (n1, n2,..)
     <subst> is a partial substitution for the bound variable names.
     <where> indicates which fnums to search for a match.
     <copy?> is T if the quantified formula should be copied.
     <if-match> is T if the instantiation should only happen if the match
        succeeds, otherwise the given partial substitution will be used.

Here, all arguments are optional (since they follow the &optional flag); defaults are indicated in square brackets (the angle brackets have no meaning). Thus the command (inst?) instructs the PVS prover to perform heuristic instantiation on all suitable formulas; the form (inst? -) restricts it to antecedent formulas, while (inst? -1 4) instructs it to perform instantiation on formulas -1 and 4. A partial substitution is indicated by a parenthesized

list of the form (<var1> <val1> ...  <varn> <valn>), for example ("x" "0") indicates

that the variable x is to get the value 0 and heuristic instantiation is to be used for the remaining variables. Arguments can simply be given in order: for example (inst? * ("x" "0")); if, however, optional arguments are omitted and allowed to default, then it is necessary to indicate the identity of any following arguments by keyword. For example (inst? :subst ("x" "0")): here, the :subst keyword is needed because the fnums argument is omitted.

The sequence of PVS prover commands used to prove a particular formula is attached to the formula and saved as a “proof script.” If the specification is changed, the status of proved formulas reverts to “unchecked” and the script must be rerun to restore the formula to the “proved” status (assuming the proof succeeds when it is rerun). For proofs to be robust in the face of reasonably small changes to the specification, it is generally best if its individual proof commands are not overly specific: for example, the command (inst? -3) (which does heuristic instantiation on formula -3) will no longer be correct if an additional clause in a modified definition, say, causes the formulas to be numbered differently. Accordingly, the PVS proof steps are fairly “intelligent” and generally do something sensible if arguments are omitted. It is generally a good idea to give as few arguments as possible, and to make arguments no more specific than necessary. For example, rather than (inst? -3), it may be better to say (inst? -), or even just (inst?).

There are about a dozen basic PVS proof commands: split and flatten do conjunctive and disjunctive splitting, respectively; case does case-splitting on a given (boolean) expression; lift-if brings conditional expressions to the top-level; skolem and inst do Skolemization and instantiation of quantified variables, respectively; beta does beta (and other) reductions; replace replaces all instances of the left hand side of an equational formula by its corresponding right hand side; lemma introduces a named formula from the specification as a lemma; rewrite rewrites using a named formula from the specification; expand expands a definition; extensionality and induct apply extensionality and induction schemes, respectively; and assert simultaneously performs automatic rewriting of formulas (or theories) that have been designated to be available as rewrite rules (using commands auto-rewrite and auto-rewrite-theory), and applies decision procedures for arithmetic. There are also commands delete and hide, for deleting or hiding formulas in the sequent (in order to reduce clutter); undo for backing out of fruitless paths; and postpone for hopping from one branch of the proof to another.

PVS proof steps can be composed into more powerful steps called strategies. The simplest control construct (though not the most primitive) is (then* <strat> <strat-list>). This applies <strat> to the current goal, and then applies <strat-list> to each of the remaining subgoals (if any). Several strategies are provided as part of PVS, and users can also write their own. Most proofs are performed using about a dozen very powerful strategies: prop is a decision procedure for propositional calculus; ground combines prop with assert; skosimp combines Skolemization with flatten (and skosimp* iterates skosimp); inst? does heuristic instantiation of quantified formulas by looking for matches in other formulas of the sequent; tcc iteratively applies all the above (its name derives from its use to automatically discharge tcc proof obligations, but it has wider applicability than that); apply-extensionality figures out the correct instance of extensionality to use for a named equational formula; replace-extensionality uses extensionality reasoning to replace one function (or record) by another; and induct-and-rewrite does what its name suggests.

Recall that our current proof goal is the following.

source_rhs_val_TCC1:
  |-------
{1} (FORALL (expr, l : list[term]), (t : term):
         l = cons(t, expr) IMPLIES length(expr) < length(l))
Rule?

When a universally quantified formula appears as a succedent (i.e., below the line) in a sequent, we generally either have to Skolemize it, or induct on it. Here Skolemization is appropriate, so we give the command (skolem!) at the rule? prompt, with the following effect.^{17}

Skolemizing, this simplifies to:
  |-------
{1} l!1 = cons(t!1, expr!1) IMPLIES length(expr!1) < length(l!1)

Next, a (flatten) command is appropriate.

Applying disjunctive simplification to flatten sequent, this simplifies to:
{-1} l!1 = cons(t!1, expr!1)
  |-------
{1} length(expr!1) < length(l!1)

At this point, we need to replace the l!1 appearing at the bottom right of the sequent by its value cons(t!1, expr!) from formula -1. We do this with the command (replace

-1).
Replacing using formula -1, this simplifies to:
[-1] l!1 = cons(t!1, expr!1)
  |-------
{1} length(expr!1) < length(cons(t!1, expr!1))

Now we need to expand the definition of the length function, so we type (expand

"length").
Expanding the definition of length, this simplifies to:
[-1] l!1 = cons(t!1, expr!1)
  |-------
{1} CASES expr!1 OF null : 0, cons(x, y) : length(y) + 1 ENDCASES
          < length(expr!1) + 1

17Convenient shorthands for PVS prover commands are available if the file cmh-pvs-prover-helps is loaded into PVS Emacs. These shorthands (due to C. Michael Holloway of NASA Langley Research Center)

are initiated by striking the TAB key, followed one or two additional keys to indicate the particular PVS prover command and any options required. For example, the (skolem!) command is invoked by TAB !, (assert)

by TAB a, and (expand "<name>") by TAB e with the cursor positioned on the function name to be expanded.

Unfortunately, this command expands both instances of length; the second one simplified, but the first one looks rather ugly. Accordingly, we go back a step using the command (undo 1), and give the more specific command (expand "length" 1 2), which instructs PVS to expand just the second instance of the function length in formula number 1.

 Expanding the definition of length, this simplifies to:
   |-------
 {1} length(expr!1) < length(expr!1) + 1

Finally, we give the command (assert) and we are done.

 Invoking decision procedures,
 Q.E.D.

Having proved the theorem, the PVS prover returns the cursor to the buffer displaying the tccs. If we now type M-x edit-proof, a summary of the proof script appears.

   ("" (SKOLEM!)
       (FLATTEN)
       (REPLACE -1)
       (EXPAND "length" 1 2)
       (ASSERT))

The outer set of parentheses and the empty string quotes in this display are there to guide the control mechanism that is necessary when there are several branches to a proof. PVS has attached this proof script to the formula source rhs val TCC1, so that next time we try to prove this formula (either explicitly, or using M-x tcp), it will rerun this script.

The next tcc, source interpreter TCC1 is rather similar to the one we have just proved, so perhaps the existing proof script will also prove this new formula. We can attach a copy of the proof script in the Proof buffer to the formula source interpreter TCC1 by placing the cursor on that formula and typing C-c C-i. PVS will attach a copy of the proof script to the new formula and ask whether we wish to run the proof. If we say “yes,” we will see that this proof script does indeed prove the new formula and, in fact, it also proves all the other termination tccs in the file. This “cut and paste” method for proving many similar formulas is quite convenient, particularly since ordinary Emacs commands can be used to edit the Proof buffer in order to customize the script from one formula to the next.

If we anticipate that a proof script will be widely useful, we may want to make it into a named proof strategy that can be invoked just like the built-in prover commands. The script we have so far is rather too specific to make into a proof strategy: the explicit naming of the formula “length” and the explicit position numbers appearing in some of the commands make it rather fragile. We can avoid the need to name the position where length should be expanded by using the form (expand "length" :if-simplifies t). The colon introduces the keyword argument if-simplifies, followed by the value that is to be assigned to it.

Here the value is t, which means true in Lisp. The keyword argument restricts expand to those instances that can be simplified after expansion.

This modification makes our proof script a little more robust, but it still mentions the function length explicitly. In [3], Shankar describes a verification concerning ordered binary trees where the termination tccs have exactly the form of those here, except that the measure function is called size rather than length. The best way to accommodate these different measure functions is to use automatic rewriting instead of explicit expansion of definitions. Automatic rewriting is performed as part of the (assert) command that also invokes the arithmetic decision procedures^{18} but it is necessary to indicate beforehand which formulas are available for rewriting. The formulas that are to be rewritten automatically can either be named explicitly, or whole theories can be named, or PVS can be instructed to rewrite anything that has the form of a definition and that appears either directly or indirectly (on expanding other definitions) in the statement of the original formula to be proved. The last of these options is appropriate here, and it is invoked by the command (auto-rewrite-defs). Automatic rewriting is more cautious than expand (to avoid looping on recursive definitions), so it does not require the equivalent of the :if-simplifies parameter.

The tentative form of our proof script is now

   ("" (SKOLEM!)
       (FLATTEN)
       (REPLACE -1)
       (AUTO-REWRITE-DEFS)
       (ASSERT))

Remaining weaknesses in this script are that the first two commands, and the last, may be inadequate to their function if the theorem is more complicated than the ones we have seen. Now, I mentioned before that the tcc strategy is rather powerful: in, fact it does iterated Skolemization, propositional simplification, automatic rewriting of definitions (using (auto-rewrite-defs)), and heuristic instantiation. Consequently, a more muscular and robust form of our script is the following.

   ("" (TCC)
       (REPLACE -1)
       (TCC))

The remaining weakness in this script is that the (replace -1) is excessively specific: the formula on which we need to replace may not be numbered -1 in all cases. We can generalize this using the command (replace*), which does replacement on all formulas.

The next step is to convert our script to a strategy. A script comprises a list of commands that are simply replayed as if the user typed them in. A strategy is more like a program: it has a control structure and can adapt to circumstances. In this case a suitable strategy uses the then* construct of PVS.

18These operations are done together because they are more effective when combined than either done separately.

   (then* (tcc) (replace*) (tcc))

This strategy first does (tcc), then applies (replace*) and (tcc) in sequence to all the subgoals that remain.

The final step is to give the strategy a name and to save it so that it becomes, in effect, an extension to the PVS prover. This is done by adding the following text to the file pvs-strategies in the user’s home directory:

   (defstep term-tcc () (then* (tcc) (replace*) (tcc))
     "Strategy for termination tccs:
      does (replace*) in addition to usual tcc strategy."
     "~%Trying termination-tcc strategy,")

Here term-tcc is the name of the new strategy, and the empty parentheses following indicate that it takes no arguments. The body of the strategy comes next, followed by the help string (this will be displayed when the user types (help term-tcc)), and the commentary string that is printed when the strategy is used during a proof. Once the pvs-strategies file is saved, the new proof strategy term-tcc is automatically available. All the termination tccs in our example file can now be proved by the single step (term-tcc).

In order to automate things further, we need to modify the strategy that is called by the M-X tcp command. Earlier, I said that tcc is this strategy, but that is not strictly correct: tcc is its heart, but the name of the strategy called by M-X tcp is tcc-strategy. It reads as follows:

   (defstrat 'tcc-strategy ()
     '(then*
       (tcc)
       (fail))
     "(tcc-strategy): The strategy used to prove TCCs with M-x tcp.")

Defstrat is an older form of the defstep function used to define strategies. (All uservisible strategies will be redefined using defstep for the next release of PVS.) All that tcc-strategy does is call tcc. If that succeeds, then we are done; if not, it proceeds to call the fail proof step, which erases everything done by tcc and leaves the proof state empty. To cause M-x tcp to call our new strategy, we simply place the following modified definition of tcc-strategy (only the third line is changed) in our pvs-strategies file.

   (defstrat 'tcc-strategy ()
     '(then*
       (term-tcc)
       (fail))
     "(tcc-strategy): The strategy used to prove TCCs with M-x tcp.")

We have now dealt with all the termination tccs, and only the single existence tcc remains.

 % Existence TCC generated (line 46) for source_stmt
   % unproved
   source_prog_TCC1 : OBLIGATION
     (EXISTS (x : crude_source_stmt) : good_source_stmt?(x))

If we invoke the prover and run the (tcc) strategy on this formula, we obtain

 Trying repeated skolemization, instantiation, and if-lifting, this simplifies to:
 source_prog_TCC1 :
   |-------
 {1} (EXISTS (x : crude_source_stmt):
        every((LAMBDA (t: term): is_var?(t) => NOT (var_val(t) = lhs(x))), rhs(x))
        AND NOT null?(rhs(x)))

We need to instantiate x with some crude source stmt that has a nonempty list in its rhs field, and whose lhs field is a variable that does not appear anywhere in the rhs list. The obvious construction is

    (# lhs:= arb, rhs:=cons[term](mk_const(0), null) #)^{19}

where arb is some constant of type variable (the choice of names is confusing here). The problem is, we haven’t declared any constants of type variable yet. We could exit the prover, modify the specification to add a declaration and then start the proof again, but that could be a very costly procedure if we were deep in a complex proof. PVS therefore allows the specification to be modified or extended while a proof is in progress. Clearly, there are opportunities for unsoundness here, so PVS considers such proofs “conditional” until they have been run against a “clean” specification.

In this case, the appropriate thing to do is to move the cursor to the compiler.pvs buffer and place it somewhere above the formula that generated the tcc we are working on and where we want the new declaration to be added. Then give the Emacs command M-x add-declaration. A new buffer will appear; we add the declaration

   arb: variable

and then type C-C C-c to indicate we are done. If there are no parse or typecheck errors detected, the declaration is incorporated into the specification. We can then return to the ongoing proof in the *pvs* buffer and give the following command.

   (inst 1 "(# lhs:= arb, rhs:=cons[term](mk_const(0),null) #)")

This will produce the result

19We need cons[term] rather than just cons in order to identify which instance of the generic list constructor is intended.

 Instantiating the top quantifier in 1 with the terms:
  (# lhs:= arb, rhs:=cons[term](mk_const(0),null) #),  this simplifies to:
 source_prog_TCC1 :
   |-------
 {1} every((LAMBDA (t : term):
        is_var?(t) => NOT (var_val(t) =
                  lhs((# lhs := arb,
                         rhs := cons[term](mk_const(0), null) #)))),
        rhs((# lhs := arb, rhs := cons[term](mk_const(0), null) #)))
       AND NOT null?(rhs((# lhs := arb, rhs := cons[term](mk_const(0), null) #)))

which can be finished off with (assert).

3 Verification

Now that we have parsed and typechecked the specification, and discharged the tcc proof obligations, we can start work on the main correctness theorem. As the proof develops, number of subsidiary lemmas will be introduced; the proof of each is described in a separate subsection.

3.1 Theorem correctness

Recall that our statement of correctness for the compiler specification is the following.

   correctness: THEOREM FORALL (sp: source_prog), (e: env):
     source_interpreter(sp, e) = target_interpreter(compiler(sp), e)

We fairly obviously are going to have to prove this by inducting on the correctness of the compilation of individual source language statements, so we propose the following lemma.

   correct_step: LEMMA FORALL (s: source_stmt), (e:env) :
      source_stmt_interp(s,e) = target_interpreter(compile_stmt(s), e)

At this point, we might want to check that the correctness theorem does indeed follow from this lemma. Accordingly, we move the cursor to the theorem correctness and give the command M-x pr. This produces the following display.^{20}

 correctness :
   |-------
 {1} FORALL (sp: source_prog), (e: env):
         source_interpreter(sp, e) = target_interpreter(compiler(sp), e)

20From now on, I will show prover displays in a small font in order to accommodate larger formulas.

32 3 VERIFICATION

We give the command (induct "sp"), indicating that we wish to induct on the variable sp. PVS chooses the correct induction scheme (here, structural induction on lists) and generates two subgoals, corresponding to the base and inductive cases. It shows the base case first.

Inducting on sp, this yields  2 subgoals:
correctness.1 :
  |-------
{1} FORALL (e: env): source_interpreter(null, e) = target_interpreter(compiler(null), e)

This is a trivial consequence of the definitions concerned, so we give the command (tcc), since this strategy will rewrite the definitions and also apply other routine steps that may be necessary.

source_interpreter rewrites source_interpreter(null, e) to e
compiler rewrites compiler(null) to null
target_interpreter rewrites target_interpreter(null, e) to e
Trying repeated skolemization, instantiation, and if-lifting,
This completes the proof of correctness.1.
correctness.2 :
  |-------
{1} (FORALL (cons1_var: source_stmt), (cons2_var: list[source_stmt]):
         (FORALL (e: env):
            source_interpreter(cons2_var, e) = target_interpreter(compiler(cons2_var), e))
           IMPLIES FORALL (e: env):
             source_interpreter(cons(cons1_var, cons2_var), e)
               = target_interpreter(compiler(cons(cons1_var, cons2_var)), e))

We see that the tcc strategy has disposed of the base case, and we are now left with the inductive case. We use the (skosimp*) strategy to eliminate most of the quantifiers.

Repeatedly Skolemizing and flattening, this simplifies to:
correctness.2 :
{-1} FORALL (e: env):
        source_interpreter(cons2_var!1, e)
          = target_interpreter(compiler(cons2_var!1), e)
  |-------
{1} source_interpreter(cons(cons1_var!1, cons2_var!1), e!1)
        = target_interpreter(compiler(cons(cons1_var!1, cons2_var!1)), e!1)

Both the functions source interpreter and compiler are applied to cons-type lists in formula 1, and should simplify if they are expanded. We therefore give the commands (expand

"source interpreter" +) and (expand "compiler" +). (The + arguments constrain the

expansions to positively-numbered formulas, since we do not want to expand the formulas above the line. The keyword arguments :if-simplifies t would serve as well.)

3.1 Theorem correctness 33

Expanding the definition of source_interpreter, this simplifies to:
 ...
Expanding the definition of compiler, this simplifies to:
correctness.2 :
[-1] FORALL (e: env):
       source_interpreter(cons2_var!1, e)
         = target_interpreter(compiler(cons2_var!1), e)
  |-------
{1} source_interpreter(cons2_var!1, source_stmt_interp(cons1_var!1, e!1))
      = target_interpreter(append(compile_stmt(cons1_var!1), compiler(cons2_var!1)), e!1)

Next we do an (inst?) in order to instantiate the quantified variable e appropriately. This command selects instantiations heuristically by matching in other formulas of the sequent.

Found substitution:
  e gets source_stmt_interp(cons1_var!1, e!1),
Instantiating quantified variables, this simplifies to:
correctness.2 :
{-1} source_interpreter(cons2_var!1, source_stmt_interp(cons1_var!1, e!1))
      = target_interpreter(compiler(cons2_var!1), source_stmt_interp(cons1_var!1, e!1))
  |-------
[1]  source_interpreter(cons2_var!1, source_stmt_interp(cons1_var!1, e!1))
      = target_interpreter(append(compile_stmt(cons1_var!1), compiler(cons2_var!1)), e!1)

It is now time to bring in the lemma correct step, using the command (lemma

"correct step").

Applying correct_step, this simplifies to:
correctness.2 :
{-1} (FORALL (s: source_stmt), (e: env):
      source_stmt_interp(s, e) = target_interpreter(compile_stmt(s), e))
[-2] source_interpreter(cons2_var!1, source_stmt_interp(cons1_var!1, e!1))
       = target_interpreter(compiler(cons2_var!1), source_stmt_interp(cons1_var!1, e!1))
  |-------
[1]  source_interpreter(cons2_var!1, source_stmt_interp(cons1_var!1, e!1))
       = target_interpreter(append(compile_stmt(cons1_var!1), compiler(cons2_var!1)), e!1)

Clearly, the next step is to instantiate the variables in formula -1. Again, the substitutions are so obvious that the heuristic strategy (inst?) is able to choose them automatically.

 Found substitution:
   e gets e!1,
   s gets cons1_var!1,
 Instantiating quantified variables, this simplifies to:
 correctness.2 :
 {-1} source_stmt_interp(cons1_var!1, e!1)
       = target_interpreter(compile_stmt(cons1_var!1), e!1)
 [-2] source_interpreter(cons2_var!1, source_stmt_interp(cons1_var!1, e!1))
       = target_interpreter(compiler(cons2_var!1), source_stmt_interp(cons1_var!1, e!1))
   |-------
 [1]  source_interpreter(cons2_var!1, source_stmt_interp(cons1_var!1, e!1))
       = target_interpreter(append(compile_stmt(cons1_var!1), compiler(cons2_var!1)), e!1)

At this point, we can see that the left hand side of formula -1 matches the second argument to the right hand side of formula -2, so we do (replace -1), and then delete formula -1 (by doing (delete -1)), since it has now served its purpose.

Belatedly, we realize that the last several steps could have been accomplished in one by simply rewriting with the lemma correct step. It is generally best to try and perform a proof using the fewest and most automatic steps, since this will make the saved proof more robust in the face of small changes to the specification. In addition, the larger steps correspond more closely to those of an informal “journal style” proof: we would like to be able to easily derive an argument fit for human consumption from the saved proof description. Accordingly, we undo everything since we introduced correct step by giving the command (undo lemma) (which says undo back to just before the last lemma command),

and then give the command (rewrite "correct step").
 Rewriting using correct_step, this simplifies to:
 correctness.2 :
 {-1} source_interpreter(cons2_var!1, target_interpreter(compile_stmt(cons1_var!1), e!1))
       = target_interpreter(compiler(cons2_var!1),
                            target_interpreter(compile_stmt(cons1_var!1), e!1))
   |-------
 {1} source_interpreter(cons2_var!1, target_interpreter(compile_stmt(cons1_var!1), e!1))
       = target_interpreter(append(compile_stmt(cons1_var!1), compiler(cons2_var!1)), e!1)

The left hand sides of the two formulas are identical, so we need to show that the right sides are equal also. We can see that this should be so, because the right hand side of formula 1 is the result of appending two compilations and then executing them on the target machine, while the right side of formula -1 is the result of executing the result of the second compilation in the context resulting from execution of the first. In order to prove this, we will need to generalize it so that we can apply induction. Something like the following seems suitable.

   target_append: LEMMA FORALL (t1,t2:list[target_instr]), (e: env):
     target_interpreter(append(t1, t2), e)
       = target_interpreter(t2, target_interpreter(t1, e))

3.1 Theorem correctness 35

We could use add-declaration to insert this lemma into the specification, but perhaps we should first test whether doing so will enable us to complete the proof. We can do this using the command

  (case "FORALL (t1,t2:list[target_instr]), (e: env):
     target_interpreter(append(t1, t2), e)
        = target_interpreter(t2, target_interpreter(t1, e))")

This command allows us to assume the formula in the current branch of the proof, and will generate a new branch on which we are required to prove it.

Case splitting on
  FORALL (t1,t2:list[target_instr]), (e: env):
    target_interpreter(append(t1f, t2), e)
      = target_interpreter(t2, target_interpreter(t1, e)),
this yields  2 subgoals:
correctness.2.1 :
{-1} FORALL (t1, t2: list[target_instr]), (e: env):
      target_interpreter(append(t1, t2), e)
        = target_interpreter(t2, target_interpreter(t1, e))
[-2] source_interpreter(cons2_var!1, target_interpreter(compile_stmt(cons1_var!1), e!1))
       = target_interpreter(compiler(cons2_var!1),
                             target_interpreter(compile_stmt(cons1_var!1), e!1))
  |-------
[1]  source_interpreter(cons2_var!1, target_interpreter(compile_stmt(cons1_var!1), e!1))
       = target_interpreter(append(compile_stmt(cons1_var!1), compiler(cons2_var!1)), e!1)

Here the combination (inst?) followed by (assert) finishes this part of the proof. We can give more than one prover command at a time using the then* strategy: (then* (inst?)

(assert)):

Found substitution:
  e gets e!1,
  t2 gets compiler(cons2_var!1),
  t1 gets compile_stmt(cons1_var!1),
Instantiating quantified variables, this simplifies to:
correctness.2.1 :
{-1} target_interpreter(append(compile_stmt(cons1_var!1), compiler(cons2_var!1)), e!1)
      = target_interpreter(compiler(cons2_var!1),
                           target_interpreter(compile_stmt(cons1_var!1), e!1))
[-2] source_interpreter(cons2_var!1, target_interpreter(compile_stmt(cons1_var!1), e!1))
      = target_interpreter(compiler(cons2_var!1),
                           target_interpreter(compile_stmt(cons1_var!1), e!1))
  |-------
[1]  source_interpreter(cons2_var!1, target_interpreter(compile_stmt(cons1_var!1), e!1))
      = target_interpreter(append(compile_stmt(cons1_var!1), compiler(cons2_var!1)), e!1)
Invoking decision procedures,
This completes the proof of correctness.2.1.
correctness.2.2 :
[-1] source_interpreter(cons2_var!1, target_interpreter(compile_stmt(cons1_var!1), e!1))
      = target_interpreter(compiler(cons2_var!1),
                           target_interpreter(compile_stmt(cons1_var!1), e!1))
  |-------
{1} FORALL (t1, t2: list[target_instr]), (e: env):
        target_interpreter(append(t1, t2), e)
          = target_interpreter(t2, target_interpreter(t1, e))
[2]  source_interpreter(cons2_var!1, target_interpreter(compile_stmt(cons1_var!1), e!1))
      = target_interpreter(append(compile_stmt(cons1_var!1), compiler(cons2_var!1)), e!1)

We have finished the proof we were interested in and are now being invited to prove the lemma that we introduced in the case command. We decide that we have learned what we wanted from this proof and abandon it with the command letter q. Now that we know the approach works, we prefer to introduce the lemma target append into the specification text and to construct “clean” proofs for it and for the theorem correctness.

Once we have added target append to the specification text, we return to correctness with the intention of constructing the clean proof. We remember from the previous proof attempt that induction, an application of the tcc strategy, expansion of source interpreter and compiler, and rewriting by correct step and target append should do the job. There is a PVS strategy called induct-and-rewrite that performs precisely this kind of activity. Accordingly, we give the command.

  (induct-and-rewrite "sp" 1 "target_append" "correct_step"
    "source_interpreter" "compiler")

We find that this completes most of the proof, but that the base case terminates with the following sequent.

 correctness.1 :
   |-------
 [1]   e!1 = target_interpreter(null, e!1)

Rewriting by target interpreter finishes off this case, so we revise our proof command by adding target interpreter to the list of rewrites.

   (induct-and-rewrite "sp" 1 "target_append" "correct_step"
     "target_interpreter" "source_interpreter" "compiler")

This version does, indeed, perform the proof completely automatically. Similarly, the command

   (induct-and-rewrite "t1" 1 "append" "target_interpreter")

generates a proof for the lemma target append automatically.

In these induct-and-rewrite commands, the first argument ("sp" and "t1", respectively) is the name of the induction variable, the second argument is the number in the sequent of the formula on which to induct, and the remaining arguments are the names of definitions or equations that are to be used as automatic rewrites. It can be rather tedious to have to enumerate (and, through failed proof attempts, discover) the correct list of formulas to use as rewrites. In the first example, it seems reasonable to name target append and correct step, since recognizing the need for these is, in some sense, the crux of the

proof, but the other three (source interpreter, target interpreter, and compiler) are

simply definitions that surely ought to be rewritten automatically the way the tcc strategy does. It looks as though the strategy induct-and-rewrite could be improved a little. The Lisp source for this strategy is shown below.

   (defstrat 'induct-and-rewrite '(var &optional (fnum 1)  &rest rewrites)
     '(then (let ((x `(auto-rewrite ,@rewrites)))
             x)
       (try (induct var fnum)
        (then*
         (skosimp*)
         (assert)
         (repeat* (apply (then* (inst?)(lift-if)(prop)(skosimp*))
         "~%Applying instantiation, if-lifting, propositional
                     simplification, and skolemization,"))
         (assert)
         (assert))
        (skip)))
     "(induct-and-rewrite var &optional fnum  &rest rewrites):
       Performs induction according to the type of var using fnum
       to formulate induction predicate, and then simplifies using
       rewrites."
     "~%By induction on ~a and rewriting,")

We don’t need to be Lisp experts to form a general idea of how this works, and we can see that what we need to do is add an (auto-rewrite-defs) into the let clause on the second and third lines so that it becomes

(let ((x `(auto-rewrite-defs))
(y `(auto-rewrite ,@rewrites)))
(then x y))

We place the modified strategy in our pvs-strategies file, calling it induct-and-rewrite-defs, and modifying the help and comment strings appropriately. To check it out, we re-prove correctness with the command

(induct-and-rewrite-defs "sp" 1 "target_append" "correct_step")

and note that it is successful.

If we now type M-x edit-proof in order to examine the proof script, we see that it contains not the single command that we just gave, but the much more elaborate script shown below.

(""
(AUTO-REWRITE "compiler.compiler"
"compiler.target_interpreter"
"compiler.source_interpreter"
"list_props.length"
"compiler.compile_stmt"
"list_aux.append"
"compiler.generate_adds"
"list_props.length"
"list_props.length"
"list_props.length"
"compiler.target_instr_interp"
"compiler.term_value"
"list_props.length"
"compiler.source_stmt_interp"
"compiler.source_rhs_val"
"list_props.length"
"compiler.term_value")
(AUTO-REWRITE "target_append" "correct_step")
(INDUCT "sp" 1)
(("1" (SKOSIMP*) (ASSERT))
("2" (SKOSIMP*)
(ASSERT)
(APPLY (THEN* (INST?)
       (LIFT-IF)
       (PROP)
       (SKOSIMP*))
"~%Applying instantiation, if-lifting, propositional
simplification, and skolemization,"))))

3.2 Lemma target append  39

What has happened here is that PVS has saved the commands generated during execution of the induct-and-rewrite-defs strategy (or rather, those commands that caused a change in the proof state). There are two types of strategy in PVS: those that are properly called strategies operate in a “glass-box” manner and display their inner workings during execution and are saved in their expanded form; those that are properly called defined rules operate as “black boxes” and do not display their operation and are saved as atomic commands. When we create a new “strategy” with the defstep function, we actually create both a strategy and a defined rule: (defstep foo …) creates a defined rule called foo and a strategy called foo$. The defstrat function creates only a strategy; however, any strategy can be made to execute (and be saved) in an atomic, black box manner by calling it within an apply command. In particular, our proof for the theorem correctness becomes atomic if given as follows.

   (apply (induct-and-rewrite-defs "sp" 1 "target_append" "correct_step"))

Its saved form is then

   ("" (APPLY (INDUCT-AND-REWRITE-DEFS "sp"
                                       1
                                       "target_append"
                                       "correct_step")))

“Glass box” strategies can be useful when developing a proof, or when debugging one after changes to the specification, but finished proofs are generally more robust (and readable) when their steps are saved as “black box” defined rules. The current arrangement where some compound proof steps are defined only as strategies and others as defined rules is a holdover from experimentation performed during the development of PVS. In a forthcoming version of PVS, all compound proof steps will be defined by defstep and the confusing distinction between strategies and defined rules will be dropped: there will simply be two forms for each strategy, the normal atomic one, and the expanded one that is indicated by a $ on the end of the name. For the rest of this example, I will speak only of “strategies” but will use them in their “defined rule” form; those that exist only as true strategies (these are the induct-and-rewrite forms) will be silently enclosed in an apply.

3.2 Lemma target append

This lemma is proved completely automatically, using the strategy just introduced, by the

command (apply (induct-and-rewrite-defs "t1" 1)).
3.3 Lemma correct step

Our next task is to prove correct step. If we invoke the prover on this formula and start things off with (skosimp) (which combines Skolemization and disjunctive simplification), and reach the following state.

 Skolemizing and flattening, this simplifies to:
 correct_step :
   |-------
 {1} source_stmt_interp(s!1, e!1) = target_interpreter(compile_stmt(s!1), e!1)

Now the values of the function applications on either side of the equality are environments— and an environment is a function from variables to integers. Thus, we need to demonstrate the equivalence of functions. This is done by showing that the values of the functions are the same for all arguments: that is, we must apply the principle of function extensionality. In PVS, this is most conveniently done by the strategy (apply-extensionality), which yields the following proof state:

 Applying extensionality, this simplifies to:
 correct_step :
   |-------
 {1} source_stmt_interp(s!1, e!1)(x!1)
         = target_interpreter(compile_stmt(s!1), e!1)(x!1)
 [2]   source_stmt_interp(s!1, e!1) = target_interpreter(compile_stmt(s!1), e!1)

The original formula has become number 2, and a new formula that asserts the equivalence of the functions for some arbitrary value x!1 has been introduced as number 1. (Note that curly braces indicate formulas that are new or changed since the previous proof state; it is a useful heuristic to focus your attention on these formulas.) The original formula is superfluous to our needs, so we remove it with (delete 2).

 Deleting some formulas, this simplifies to:
 correct_step :
   |-------
 [1]   source_stmt_interp(s!1, e!1)(x!1) = target_interpreter(compile_stmt(s!1), e!1)(x!1)

Several choices are possible at this stage, but the most profitable is to consider two cases, depending on whether x!1 is the same as the left hand side of the source statement s!1: if it is, then we need to consider the behavior of the compiler and of the source and target and interpreters; but if it is not, then the result will follow because only the value of the left hand side of an assignment statement should be changed as a result of executing the statement. The case-split is performed by the command (case-replace "x!1 = lhs(s!1)"). We are first presented with the case where x!1 does equal lhs(s!1).

 Assuming and applying x!1=lhs(s!1), this yields  2 subgoals:
 correct_step.1 :
 {-1} x!1 = lhs(s!1)
   |-------
 {1} source_stmt_interp(s!1, e!1)(lhs(s!1))
         = target_interpreter(compile_stmt(s!1), e!1)(lhs(s!1))

3.3 Lemma correct step  41

To make progress, we need to expand definitions. The (tcc) strategy does this conveniently.

 Trying repeated skolemization, instantiation, and if-lifting, this simplifies to:
 correct_step.1 :
 [-1] x!1 = lhs(s!1)
   |-------
 {1} source_rhs_val(rhs(s!1), e!1)
         = target_interpreter(generate_adds(lhs(s!1), rhs(s!1)),
                              e!1 WITH [lhs(s!1) := 0])(lhs(s!1))

We notice that the left hand side of the equality in formula 1 involves the environment e!1, while the right hand side involves that which results from setting the value of lhs(s!1) to zero (specified by the construction e!1 WITH [lhs(s!1) := 0]). Because the variable on the left of a source language assignment statement must not appear in the expression on its right, it ought to be that the value of the left hand side variable is irrelevant to the value of source rhs val. We postulate this as a lemma that we add to the specification using M-x

add-declaration.
   prior_value_irrelevant: LEMMA FORALL (s: source_stmt), (e: env), (x:int):
     source_rhs_val(rhs(s), e) = source_rhs_val(rhs(s), e WITH [(lhs(s)) := x])

We  attempt  to  rewrite  with  this  formula,

using the command (rewrite "prior value irrelevant"), but are told “No matching
instance for prior value irrelevant found.” The reason for this is that the variable

x does not appear in the left hand side of the formula. We explicitly indicate that the value 0 should be substituted for x with the command

    (rewrite "prior_value_irrelevant" :subst ("x" "0"))

This yields the following sequent.

 Rewriting using prior_value_irrelevant, where
   x gets 0,
 this simplifies to:
 correct_step.1 :
 [-1] x!1 = lhs(s!1)
   |-------
 {1} source_rhs_val(rhs(s!1), e!1 WITH [(lhs(s!1)) := 0])
         = target_interpreter(generate_adds(lhs(s!1), rhs(s!1)),
                              e!1 WITH [lhs(s!1) := 0])(lhs(s!1))

We now observe that formula 1 looks very much like the natural statement of correctness for the compilation of the expression on the right hand side of a source language expression. However, the e!1 WITH [lhs(s!1) := 0] looks too specific for a general lemma. We should generalize formula 1 to the case of an arbitrary environment. We speculate that the following statement is the one we want.

  FORALL (s:source_stmt), (e:env) :
    source_rhs_val(rhs(s),e) =
      target_interpreter(generate_adds(lhs(s), rhs(s)), e)(lhs(s))

However, a little more thought shows that this is not correct. The function application generate adds(lhs(s), rhs(s)) generates a series of ADD instructions, using lhs(s) as an accumulator. Consequently, the value in lhs(s) after interpretation of these instructions is the result of adding the values in rhs(s) to the original value of lhs(s). This, we need to add this value to the left hand side of our proposed lemma. This leads to the formulation of the following lemma which we add to the specification with M-x add-declaration.

  correct_expr: LEMMA FORALL (s:source_stmt), (e:env) :
       source_rhs_val(rhs(s),e) + e(lhs(s)) =
         target_interpreter(generate_adds(lhs(s), rhs(s)), e)(lhs(s))

We cannot rewrite with this lemma because no instance of its left hand side appears in the sequent. Consequently, we introduce it with the command (lemma "correct expr").

Applying correct_expr, this simplifies to:
correct_step.1 :
{-1} (FORALL (s: source_stmt), (e: env):
         source_rhs_val(rhs(s), e) + e(lhs(s))
           = target_interpreter(generate_adds(lhs(s), rhs(s)), e)(lhs(s)))
[-2] x!1 = lhs(s!1)
  |-------
[1]  source_rhs_val(rhs(s!1), e!1 WITH [(lhs(s!1)) := 0])
      = target_interpreter(generate_adds(lhs(s!1), rhs(s!1)),
                           e!1 WITH [lhs(s!1) := 0])(lhs(s!1))

We then use (inst?) to instantiate the quantified variables.

Found substitution:
  e gets e!1 WITH [(lhs(s!1)) := 0],
  s gets s!1,
Instantiating quantified variables, this simplifies to:
correct_step.1 :
{-1} source_rhs_val(rhs(s!1), e!1 WITH [(lhs(s!1)) := 0])
        + e!1 WITH [(lhs(s!1)) := 0](lhs(s!1))
        = target_interpreter(generate_adds(lhs(s!1), rhs(s!1)),
                             e!1 WITH [(lhs(s!1)) := 0])(lhs(s!1))
[-2] x!1 = lhs(s!1)
  |-------
[1]  source_rhs_val(rhs(s!1), e!1 WITH [(lhs(s!1)) := 0])
      = target_interpreter(generate_adds(lhs(s!1), rhs(s!1)),
                           e!1 WITH [lhs(s!1) := 0])(lhs(s!1))

We see that formulas -1 and 1 will become identical when the WITH clauses are simplified by the decision procedures, so we can finish this case with (assert), and are then presented with the second branch of our earlier case-split.

 Invoking decision procedures,
 This completes the proof of correct_step.1.
 correct_step.2 :
   |-------
 {1} x!1 = lhs(s!1)
 [2]   source_stmt_interp(s!1, e!1)(x!1)
         = target_interpreter(compile_stmt(s!1), e!1)(x!1)

In sequent calculus, the appearance of an equation (such as formula 1) among the succedents is equivalent to its negation appearing among the antecedents. Thus, this branch of the proof is “really” the case where we must show that formula 2 holds, when x!1 does not equal lhs(s!1). It looks as though the left hand side of formula 2 should simplify, so we

give the command (expand "source stmt interp").
 Expanding the definition of source_stmt_interp, this simplifies to:
 correct_step.2 :
   |-------
 [1]   x!1 = lhs(s!1)
 {2} e!1(x!1) = target_interpreter(compile_stmt(s!1), e!1)(x!1)

The reason this simplified version of formula 2 should hold is that all the target instructions generated by compile stmt(s!1) should have a single destination (namely, lhs(s!1)) that

is different from x!1. Thus the value of target interpreter(compile stmt(s!1), e!1)

should be an environment that has the same value for x!1 as the original environment e!1. We use M-X add-declaration to introduce these additional notions into the specification.

   single_dest?(dest: variable, tp: target_prog): bool =
      NOT null?(tp) AND every((LAMBDA (i: target_instr): dest(i)=dest), tp)
   independence: LEMMA FORALL (dest, v:variable), (t:target_prog), (e: env):
      single_dest?(dest, t) and dest/=v => target_interpreter(t, e)(v) = e(v)

Then we give the command (lemma "independence") to bring this lemma into the proof.

 Applying independence, this simplifies to:
 correct_step.2 :
 {-1} (FORALL (dest, v: variable), (t: target_prog), (e: env):
         single_dest?(dest, t) AND dest /= v => target_interpreter(t, e)(v) = e(v))
   |-------
 [1]  x!1 = lhs(s!1)
 [2]  e!1(x!1) = target_interpreter(compile_stmt(s!1), e!1)(x!1)

Next, we try (inst?) but this reports “Couldn't find a suitable instantiation for
any quantified formula.  Please provide partial instantiation.” The reason is

that there is no obvious match for the variable dest. In my opinion, inst? should make a partial substitution in this case, but the present version does not do this,^{21} so we help it along by explicitly providing the correct substitution for dest in the command

   (inst? :subst ("dest" "lhs(s!1)"))

This yields the following sequent.

 Found substitution:
   v gets x!1,
   e gets e!1,
   t gets compile_stmt(s!1),
   dest: variable gets lhs(s!1),
 Instantiating quantified variables, this simplifies to:
 correct_step.2 :
 {-1} single_dest?(lhs(s!1), compile_stmt(s!1)) AND lhs(s!1) /= x!1
         => target_interpreter(compile_stmt(s!1), e!1)(x!1) = e!1(x!1)
   |-------
 [1]  x!1 = lhs(s!1)
 [2]  e!1(x!1) = target_interpreter(compile_stmt(s!1), e!1)(x!1)

We would be finished if we could establish single dest?(lhs(s!1), compile stmt(s!1)).

Now this ought to be a property of the compilation algorithm, given that s!1 is a valid source stmt. We introduce this as another lemma using M-x add-declaration:

   good_compile: LEMMA (FORALL (s: source_stmt):
      single_dest?(lhs(s), compile_stmt(s)))

and then the proof can be completed by (lemma "good compile"), (inst?) and (assert).

We can review the proof script by the command M-x edit-proof:

21PVS is in beta-test; the occasional deficiencies mentioned here are being remedied before its “official”

release. In particular, a recent enhancement to inst? does perform partial substitutions. With the latest version of PVS, a simple (inst?) is all that is required here.

("" (SKOSIMP)
(APPLY-EXTENSIONALITY)
(DELETE 2)
(CASE-REPLACE "x!1=lhs(s!1)")
(("1" (TCC)
(REWRITE "prior_value_irrelevant" :SUBST ("x" 0))
(LEMMA "correct_expr")
(INST?)
(ASSERT))
("2" (EXPAND "source_stmt_interp")
(LEMMA "independence")
(INST? :SUBST ("dest" "lhs(s!1)"))
(LEMMA "good_compile")
(INST?)
(ASSERT)
(PROPAX))))

Notice that on three occasions in this script we introduce a lemma and then do an (inst?) to heuristically instantiate its variables. This sequence seems generally useful, so we define a strategy use to combine these steps (it also does a beta-reduction, which is useful when the lemma contains let expressions).

(defstep use (l &optional subst)
(then* (lemma l subst)(beta)(inst?))
"(use formula &optional subst) :
introduces lemma l, then does (beta) and (inst?)."
"~%Using lemma ~a,")

As we have defined it, use takes an optional substitution argument that is passed to the invocation of lemma. This new strategy allows our proof script to be simplified to that shown below. (This modified proof script can be attached to correct step and run using

C-c C-i).

("" (SKOSIMP)
(APPLY-EXTENSIONALITY)
(DELETE 2)
(CASE-REPLACE "x!1=lhs(s!1)")
(("1" (TCC)
 (REWRITE "prior_value_irrelevant" :SUBST ("x" 0))
 (USE "correct_expr")
 (ASSERT))
("2" (EXPAND "source_stmt_interp")
  (USE "independence" ("dest" "lhs(s!1)"))
  (USE "good_compile")
  (ASSERT)
  (PROPAX))))

3.4 Lemma correct expr

We now need to prove the various lemmas we introduced during the proof of correct step. The first one to work on is correct expr:

   correct_expr: LEMMA FORALL (s:source_stmt), (e:env) :
        source_rhs_val(rhs(s),e) + e(lhs(s)) =
          target_interpreter(generate_adds(lhs(s), rhs(s)), e)(lhs(s))

It is obvious that we need to prove this by induction on rhs(s), but this is a term, not a quantified variable. It appears, therefore, that we should generalize the formula to yield the following.

   FORALL (v:variable), (l: list[term]), (e:env) :
      source_rhs_val(l,e) + e(v) =
        target_interpreter(generate_adds(v, l), e)(v)

The trouble is, this is not true if the variable v appears among the terms in the list l. The natural way to remedy this is to require that v and l should constitute a good source stmt. We therefore introduce the following lemma with M-X add-declaration.

   correct_expr_aux: LEMMA FORALL (v:variable), (l: list[term]), (e:env) :
     good_source_stmt?((# lhs := v, rhs := l #)) =>
        source_rhs_val(l,e) + e(v) =
          target_interpreter(generate_adds(v, l), e)(v)
To prove correct expr, we can now do (skosimp) followed by (use "correct expr aux").

This gives

 {-1} good_source_stmt?((# lhs := lhs(s!1), rhs := rhs(s!1) #))
         => source_rhs_val(rhs(s!1), e!1) + e!1(lhs(s!1))
           = target_interpreter(generate_adds(lhs(s!1), rhs(s!1)), e!1)(lhs(s!1))
   |-------
 [1]  source_rhs_val(rhs(s!1), e!1) + e!1(lhs(s!1))
        = target_interpreter(generate_adds(lhs(s!1), rhs(s!1)), e!1)(lhs(s!1))

We now need to persuade the prover that (# lhs := lhs(s!1), rhs := rhs(s!1) #) and s!1 are the same thing. This is done by

   (replace-extensionality "(# lhs := lhs(s!1), rhs := rhs(s!1) #)" "s!1")

which uses the extensionality axiom for crude source stmt to yield the necessary equality, then replaces the first term by the second.

 {-1} good_source_stmt?(s!1)
         => source_rhs_val(rhs(s!1), e!1) + e!1(lhs(s!1))
           = target_interpreter(generate_adds(lhs(s!1), rhs(s!1)), e!1)(lhs(s!1))
   |-------
 [1]  source_rhs_val(rhs(s!1), e!1) + e!1(lhs(s!1))
        = target_interpreter(generate_adds(lhs(s!1), rhs(s!1)), e!1)(lhs(s!1))

Now the type of s!1 is source stmt, which is the predicate subtype of crude source stmt satisfying good source stmt?. Thus (assert) is able to finish the proof from this point.

3.5 Lemma correct expression aux  47

3.5 Lemma correct expression aux

We now turn our attention to correct expr aux. This clearly requires a proof by induction, but the induct-and-rewrite strategy and its variants are unable to prove it. Therefore, we take over the direction of the proof and give the command (induct "l" 1). The base case is dealt with by (tcc), and we are left with

 correct_expr_aux.2 :
   |-------
 {1} (FORALL (cons1_var: term), (cons2_var: list[term]):
        (FORALL (v: variable), (e: env):
           good_source_stmt?((# lhs := v, rhs := cons2_var #))
             => source_rhs_val(cons2_var, e) + e(v)
               = target_interpreter(generate_adds(v, cons2_var), e)(v))
          IMPLIES FORALL (v: variable), (e: env):
            good_source_stmt?((# lhs := v, rhs := cons(cons1_var, cons2_var) #))
              => source_rhs_val(cons(cons1_var, cons2_var), e) + e(v)
                = target_interpreter(generate_adds(v, cons(cons1_var, cons2_var)), e)(v))

Two (skosimp)s in succession (which can be done in a single command by (skosimp*)) give us the following sequent.

 correct_expr_aux.2 :
 {-1} FORALL (v: variable), (e: env):
       good_source_stmt?((# lhs := v, rhs := cons2_var!1 #))
         => source_rhs_val(cons2_var!1, e) + e(v)
           = target_interpreter(generate_adds(v, cons2_var!1), e)(v)
 {-2} good_source_stmt?((# lhs := v!1, rhs := cons(cons1_var!1, cons2_var!1) #))
   |-------
 {1} source_rhs_val(cons(cons1_var!1, cons2_var!1), e!1) + e!1(v!1)
         = target_interpreter(generate_adds(v!1, cons(cons1_var!1, cons2_var!1)), e!1)(v!1)

There are several defined functions in this sequent, and it seems likely that most of them will need to be expanded. The boldest way to do this is by turning all definitions and equations in the theory (prior to the declaration of correct expr aux) into automatic rewrites with

(auto-rewrite-theory "compiler"), then doing (assert). We discover that this leaves

us with some complicated expressions involving the function every. These come from the definition of good source stmt?, so we undo the (assert), and turn off rewriting on this

one definition by (stop-rewrite "good source stmt?"), then do the (assert) again.

This leaves us with.

correct_expr_aux.2 :
[-1] FORALL (v: variable), (e: env):
      good_source_stmt?((# lhs := v, rhs := cons2_var!1 #))
        => source_rhs_val(cons2_var!1, e) + e(v)
          = target_interpreter(generate_adds(v, cons2_var!1), e)(v)
[-2] good_source_stmt?((# lhs := v!1, rhs := cons(cons1_var!1, cons2_var!1) #))
  |-------
{1} source_rhs_val(cons2_var!1, e!1) + term_value(cons1_var!1, e!1) + e!1(v!1)
       = target_interpreter(generate_adds(v!1, cons2_var!1),
                            e!1 WITH [v!1 := e!1(v!1)
                                               + term_value(cons1_var!1, e!1)])(v!1)

We try an (inst?) to instantiate the quantifiers in formula -1 but observe that it chooses the wrong instantiation, so we specify the obvious correct one by

   (INST -1 "v!1" "e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)]")

which leaves us with

correct_expr_aux.2 :
{-1} good_source_stmt?((# lhs := v!1, rhs := cons2_var!1 #))
        => source_rhs_val(cons2_var!1,
                          e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)])
            + e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)](v!1)
            = target_interpreter(generate_adds(v!1, cons2_var!1),
                                 e!1 WITH [v!1 := e!1(v!1)
                                                   + term_value(cons1_var!1, e!1)])(v!1)
[-2] good_source_stmt?((# lhs := v!1, rhs := cons(cons1_var!1, cons2_var!1) #))
  |-------
[1]  source_rhs_val(cons2_var!1, e!1) + term_value(cons1_var!1, e!1) + e!1(v!1)
       = target_interpreter(generate_adds(v!1, cons2_var!1),
                            e!1 WITH [v!1 := e!1(v!1)
                                              + term_value(cons1_var!1, e!1)])(v!1)

Now formula -2 ought to discharge the antecedent to formula -1, so we try the strategy (prop) that does propositional simplification. This splits the proof into two branches; the first is shown below.

Applying propositional simplification, this yields  2 subgoals:
correct_expr_aux.2.1 :
{-1} source_rhs_val(cons2_var!1,
                    e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)])
       + e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)](v!1)
        = target_interpreter(generate_adds(v!1, cons2_var!1),
                             e!1 WITH [v!1 := e!1(v!1)
                                                + term_value(cons1_var!1, e!1)])(v!1)
[-2] good_source_stmt?((# lhs := v!1, rhs := cons(cons1_var!1, cons2_var!1) #))
  |-------
[1]  source_rhs_val(cons2_var!1, e!1) + term_value(cons1_var!1, e!1) + e!1(v!1)
       = target_interpreter(generate_adds(v!1, cons2_var!1),
                            e!1 WITH [v!1 := e!1(v!1)
                                               + term_value(cons1_var!1, e!1)])(v!1)

The right hand side of formula -1 matches that of formula 1, so we do a right-to-left replacement with formula -1 using (replace -1 :dir RL), then remove formula -1 with the command (delete -1).

Replacing rhs by lhs from -1, this simplifies to:
correct_expr_aux.2.1 :
[-1] good_source_stmt?((# lhs := v!1, rhs := cons(cons1_var!1, cons2_var!1) #))
  |-------
{1} source_rhs_val(cons2_var!1, e!1) + term_value(cons1_var!1, e!1) + e!1(v!1)
       = source_rhs_val(cons2_var!1,
                        e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)])
           + e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)](v!1)

We do an (assert) to simplify things a bit.

Invoking decision procedures, this simplifies to:
correct_expr_aux.2.1 :
[-1] good_source_stmt?((# lhs := v!1, rhs := cons(cons1_var!1, cons2_var!1) #))
  |-------
{1} source_rhs_val(cons2_var!1, e!1)
       = source_rhs_val(cons2_var!1,
                        e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)])

Now this is similar to a situation we have met before (on page 41): the two sides of formula 1 ought to be the same because v!1 is the lhs of a source statement, and its value is irrelevant to that of (part of) the rhs. Accordingly, we do (lemma "prior value irrelevant") to invoke the lemma we introduced previously for just this circumstance.

Applying prior_value_irrelevant, this simplifies to:
correct_expr_aux.2.1 :
{-1} (FORALL (s: source_stmt), (e: env), (x: int):
       source_rhs_val(rhs(s), e) = source_rhs_val(rhs(s), e WITH [(lhs(s)) := x]))
[-2] good_source_stmt?((# lhs := v!1, rhs := cons(cons1_var!1, cons2_var!1) #))
  |-------
[1]  source_rhs_val(cons2_var!1, e!1)
       = source_rhs_val(cons2_var!1,
                        e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)])

Heuristic instantiation with (inst?) is unable to help here, so we give an explicit substitution for just the first variable s with the command

  (INST -1 "(# lhs := v!1, rhs := cons2_var!1 #)" __)

The underscores at the end indicate that the variables e and x are not to be instantiated yet.

Instantiating the top quantifier in -1 with the terms:
   (# lhs := v!1, rhs := cons2_var!1 #), _, _,
this yields  2 subgoals:
correct_expr_aux.2.1.1 :
{-1} (FORALL (e: env), (x: int):
       source_rhs_val(rhs((# lhs := v!1, rhs := cons2_var!1 #)), e)
         = source_rhs_val(rhs((# lhs := v!1, rhs := cons2_var!1 #)),
                          e WITH [(lhs((# lhs := v!1, rhs := cons2_var!1 #))) := x]))
[-2] good_source_stmt?((# lhs := v!1, rhs := cons(cons1_var!1, cons2_var!1) #))
  |-------
[1]  source_rhs_val(cons2_var!1, e!1)
       = source_rhs_val(cons2_var!1,
                        e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)])

Notice that this substitution generated two subgoals. The other branch, which we will see shortly, is a tcc necessary to establish that the literal record we gave as the substitution is indeed a source stmt (i.e., satisfies the subtype predicate good source stmt?). We give an (assert) to simplify things a bit

Invoking decision procedures, this simplifies to:
correct_expr_aux.2.1.1 :
{-1} (FORALL (e: env), (x: int):
       source_rhs_val(cons2_var!1, e)
         = source_rhs_val(cons2_var!1, e WITH [v!1 := x]))
[-2] good_source_stmt?((# lhs := v!1, rhs := cons(cons1_var!1, cons2_var!1) #))
  |-------
[1]  source_rhs_val(cons2_var!1, e!1)
       = source_rhs_val(cons2_var!1,
                        e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)])

Now the substitutions are obvious, so we do (inst?).

Found substitution:
  x gets e!1(v!1) + term_value(cons1_var!1, e!1),
  e gets e!1,
Instantiating quantified variables,
This completes the proof of correct_expr_aux.2.1.1.
correct_expr_aux.2.1.2 :
[-1] good_source_stmt?((# lhs := v!1, rhs := cons(cons1_var!1, cons2_var!1) #))
  |-------
{1} good_source_stmt?((# lhs := v!1, rhs := cons2_var!1 #))
[2]  source_rhs_val(cons2_var!1, e!1)
       = source_rhs_val(cons2_var!1,
                        e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)])

That finishes off this branch of the proof and we are now presented with the subtype tcc branch mentioned earlier. Here we do need to expand the definition of good source stmt? (remember, we turned off automatic rewriting on this definition), and this is most easily accomplished by (tcc).

Trying repeated skolemization, instantiation, and if-lifting,
this simplifies to:
correct_expr_aux.2.1.2:
{-1} (is_var?(cons1_var!1) => NOT (var_val(cons1_var!1) = v!1))
      & every((LAMBDA (t: term): is_var?(t) => NOT (var_val(t) = v!1)), cons2_var!1)
  |-------
{1} every((LAMBDA (t: term): is_var?(t) => NOT (var_val(t) = v!1)), cons2_var!1)
      AND NOT null?(cons2_var!1)
[2]  source_rhs_val(cons2_var!1, e!1)
       = source_rhs_val(cons2_var!1,
                        e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)])

This looks like it ought to follow trivially from definitions and type-constraints, so we do (tcc) again.

Trying repeated skolemization, instantiation, and if-lifting,
This completes the proof of correct_expr_aux.2.1.2.
This completes the proof of correct_expr_aux.2.1.
correct_expr_aux.2.2 :
[-1] good_source_stmt?((# lhs := v!1, rhs := cons(cons1_var!1, cons2_var!1) #))
  |-------
{1} good_source_stmt?((# lhs := v!1, rhs := cons2_var!1 #))
[2]  source_rhs_val(cons2_var!1, e!1) + term_value(cons1_var!1, e!1) + e!1(v!1)
       = target_interpreter(generate_adds(v!1, cons2_var!1),
                            e!1 WITH [v!1 := e!1(v!1)
                                               + term_value(cons1_var!1, e!1)])(v!1)

Indeed, that does finish this branch of the proof, and we are left with one from the (prop) that we did earlier. This looks similar to the tcc branch that we just dealt with, so we try the same technique of (tcc) followed by another (tcc) and the proof is complete. The complete script (shown by M-x edit-proof) is the following.

   ("" (INDUCT "l" 1)
       (("1" (TCC))
         ("2" (SKOSIMP*)
              (AUTO-REWRITE-THEORY "compiler")
              (STOP-REWRITE "good_source_stmt?")
              (ASSERT)
              (INST -1
                    "v!1"
                    "e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)]")
              (PROP)
              (("1" (REPLACE -1 :DIR RL)
                    (DELETE -1)
                    (ASSERT)
                    (LEMMA "prior_value_irrelevant")
                    (INST -1 "(# lhs := v!1, rhs := cons2_var!1 #)" __)
                    (("1" (ASSERT) (INST?)) ("2" (TCC) (TCC))))
                ("2" (TCC) (TCC))))))

Because we did need to expand the definition of good source stmt? in the subsidiary cases, it is worth checking whether the proof succeeds without the (STOP-REWRITE "good source stmt?") command. We simply strike that line out of the Proof Edit buffer and attach and run the modified proof using C-c C-i. Most of the proof goes through as before, but there are some differences and the replay finally stops with the goal

 correct_expr_aux.2.3 :
 {-1} null?(cons2_var!1)
 [-2] every((LAMBDA (t: term): is_var?(t) => var_val(t) /= v!1),
             cons(cons1_var!1, cons2_var!1))
   |-------
 [1]  source_rhs_val(cons2_var!1, e!1) + term_value(cons1_var!1, e!1) + e!1(v!1)
        = target_interpreter(generate_adds(v!1, cons2_var!1),
                             e!1 WITH [v!1 := e!1(v!1)
                                                + term_value(cons1_var!1, e!1)])(v!1)

This looks like a candidate for (tcc), and with that command the proof does terminate. The new proof script is slightly simpler (and probably more robust) than the previous one.

3.6 Lemma good compile  53

("" (INDUCT "l" 1)
(("1" (TCC))
("2" (SKOSIMP*)
(AUTO-REWRITE-THEORY "compiler")
(ASSERT)
(INST -1
"v!1"
"e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)]")
(PROP)
(("1" (REPLACE -1 :DIR RL)
(DELETE -1)
(ASSERT)
(LEMMA "prior_value_irrelevant")
(INST -1 "(# lhs := v!1, rhs := cons2_var!1 #)" __)
(("1" (ASSERT) (INST?)) ("2" (TCC))))
("2" (TCC))
("3" (TCC))))))

3.6 Lemma good compile

We now turn our attention to the lemma good compile. As with correct expr, we need to create a generalization of this lemma so that we will be able to apply induction. The generalization is

good_compile_aux: LEMMA (FORALL (dest:variable), (expr:list[term]):
LET s = (# lhs := dest, rhs := expr #) IN
good_source_stmt?(s) => single_dest?(dest, compile_stmt(s)))

We begin the proof of good compile with the commands (skosimp) and (lemma "good compile aux"). We then have the sequent

good_compile :
{-1} (FORALL (dest: variable), (expr: list[term]):
LET s = (# lhs := dest, rhs := expr #)
IN good_source_stmt?(s) => single_dest?(dest, compile_stmt(s)))
|-------
[1]  single_dest?(lhs(s!1), compile_stmt(s!1))

We give the command (beta) in order to reduce the LET form:

Applying beta-reduction, this simplifies to:
good_compile :
{-1} (FORALL (dest: variable), (expr: list[term]):
good_source_stmt?((# lhs := dest, rhs := expr #))
=> single_dest?(dest, compile_stmt((# lhs := dest, rhs := expr #))))
|-------
[1]  single_dest?(lhs(s!1), compile_stmt(s!1))

Heuristic instantiation fails, so we provide some help with a partial substitution:

(inst?  :subst ("expr" "rhs(s!1)")).^{22}

Found substitution:
  dest gets lhs(s!1),
  expr: list[term] gets rhs(s!1),
Instantiating quantified variables, this simplifies to:
good_compile :
{-1} good_source_stmt?((# lhs := lhs(s!1), rhs := rhs(s!1) #))
      => single_dest?(lhs(s!1), compile_stmt((# lhs := lhs(s!1), rhs := rhs(s!1) #)))
  |-------
[1]  single_dest?(lhs(s!1), compile_stmt(s!1))

(The previous three commands could have been accomplished more simply by

  (use "good compile aux" ("expr" "rhs(s!1)"))

but I wanted to display the effect of beta-reduction on a LET form.) Next we do

  (replace-extensionality "(# lhs := lhs(s!1), rhs := rhs(s!1) #)" "s!1")

and obtain

Replacing (# lhs := lhs(s!1), rhs := rhs(s!1) #) by s!1 using extensionality,
this simplifies to:
good_compile :
{-1} good_source_stmt?(s!1) => single_dest?(lhs(s!1), compile_stmt(s!1))
  |-------
[1]  single_dest?(lhs(s!1), compile_stmt(s!1))

A final (assert) finishes off the proof.

The auxiliary lemma good compile aux is dispatched by

  (apply (induct-and-rewrite-defs "expr" 1))

3.7 Lemma independence
The next lemma is independence. The command (apply (induct-and-rewrite-defs

"t" 1)) completes most of the proof, but leaves three unfinished branches. The simplest of these is

22In the latest version of PVS, (inst?) is adequate on its own here.

3.8 Lemma prior value irrelevant  55

independence.3.1 :
[-1] FORALL (dest, v: variable), (e: env):
       (NOT null?(cons2_var!1)
         AND every((LAMBDA (i: target_instr): dest(i) = dest), cons2_var!1))
         AND NOT (dest = v)
        => target_interpreter(cons2_var!1, e)(v) = e(v)
[-2] dest(cons1_var!1) = dest!1
[-3] every((LAMBDA (i: target_instr): dest(i) = dest!1), cons2_var!1)
  |-------
[1]  target_interpreter(cons2_var!1,
                        e!1 WITH [(dest(cons1_var!1)) :=
                                    term_value(src(cons1_var!1), e!1)])(v!1)
        = e!1(v!1)
[2]  dest!1 = v!1

The problem is that (inst?) is unable to find a suitable substitution since the obvious match for dest is found in a different formula from those for v and e. We move things

along with (inst?  :subst ("dest" "dest!1")) and then (tcc) finishes that branch.

The other two branches succumb to the same procedure.^{23} Thus, the complete proof can be dealt with by the command

  (then* (induct-and-rewrite-defs "t" 1)
         (inst? :subst ("dest" "dest!1"))
         (tcc))

3.8 Lemma prior value irrelevant
The next lemma, prior value irrelevant is like good compile and correct expr in need-

ing an auxiliary lemma for induction:

  prior_value_irrelevant_aux: LEMMA
   FORALL (v:variable), (l: list[term]), (e: env), (x:int):
     LET s = (# lhs := v, rhs := l #) IN
       good_source_stmt?(s) =>
         source_rhs_val(l, e) = source_rhs_val(l, e with [(v) := x])

A similar proof script to that used for the other lemmas of this kind works here.

  ("" (SKOSIMP)
      (USE "prior_value_irrelevant_aux")
      (ASSERT)
      (REPLACE-EXTENSIONALITY "(# lhs := lhs(s!1), rhs := rhs(s!1) #)"
                              "s!1")
      (ASSERT))

23In the latest version of PVS, (inst?) does find the substitution, and the whole proof is performed

automatically by (induct-and-rewrite-defs "t" 1).

3.9 Lemma prior value irrelevant aux

The remaining lemma prior value irrelevant aux is mostly proved by the strategy

(apply (induct-and-rewrite-defs "l" 1)), but two branches are left unproved. The

simplest is

 prior_value_irrelevant_aux.2.1 :
 [-1] source_rhs_val(cons2_var!1, e!1)
        = source_rhs_val(cons2_var!1, e!1 WITH [v!1 := x!1])
 [-2] every((LAMBDA (t: term): is_var?(t) => NOT (var_val(t) = v!1)),
             cons2_var!1)
   |-------
 [1]  (var_val(cons1_var!1) = v!1)
 [2]  term_value(cons1_var!1, e!1)
         = term_value(cons1_var!1, e!1 WITH [v!1 := x!1])

This can be dealt with by with by (expand "term value") followed by (tcc). The other unproved branch succumbs to the same treatment.

Notice that we had to explicitly expand term value here, even though it is among the definitions that should automatically be rewritten by the induct-and-rewrite-defs strategy. The explanation is that this strategy invokes a rather cautious form of rewriting, in which a term is rewritten only if its expanded form is can be simplified in some way. It is possible to invoke automatic rewriting in a more muscular mode using the command (auto-rewrite! "<name>") (note the ! in the name). We can incorporate this into a modified induction strategy that substitutes the following five lines for the first three of

induct-and-rewrite.
 (defstrat 'induct-and-rewrite-defs! '(var &optional (fnum 1) &rest rewrites)
   '(then (let ((x `(auto-rewrite-defs))
                (y `(stop-rewrite ,@rewrites))
                (z `(auto-rewrite! ,@rewrites)))
           (then* x y z))

This strategy will rewrite named formulas in the more muscular manner. Notice that it first turns off automatic rewriting for those formulas, in case they have been enabled in the weak form by the auto-rewrite-defs strategy that is called earlier. With this new strategy available, prior value irrelevant aux can be proved automatically by the command.

    (apply (induct-and-rewrite-defs! "l" 1 "term_value"))

4 Summary

We have now finished this example specification and verification using PVS. In this section, I display a few of the summaries and displays that PVS can generate.

4.1 Proof Summary 57

4.1 Proof Summary

To make sure we really are done, we can do M-x prf (prove file), and obtain the following display.

Proof summary for theory list_aux
append_TCC2............................................proved - complete
Theory totals: 1 formulas, 1 attempted, 1 succeeded.
Proof summary for theory compiler
source_prog_TCC1.......................................proved - complete
source_rhs_val_TCC1....................................proved - complete
source_interpreter_TCC1................................proved - complete
target_interpreter_TCC1................................proved - complete
generate_adds_TCC1.....................................proved - complete
compiler_TCC1..........................................proved - complete
prior_value_irrelevant_aux.............................proved - complete
prior_value_irrelevant.................................proved - complete
independence...........................................proved - complete
good_compile_aux.......................................proved - complete
good_compile...........................................proved - complete
correct_expr_aux.......................................proved - complete
correct_expr...........................................proved - complete
correct_step...........................................proved - complete
target_append..........................................proved - complete
correctness............................................proved - complete
Theory totals: 16 formulas, 16 attempted, 16 succeeded.
Grand Totals: 17 proofs, 17 attempted, 17 succeeded.

4.2 Proofchain Analysis

Another view is obtained by giving the command M-X spc (status-proof-chain) with the cursor on the formula correctness.

correctness has been PROVED.
The proof chain for correctness is COMPLETE.
correctness depends on the following proved theorems:
compiler.independence
compiler.good_compile_aux
list_props.length_TCC2
compiler.correct_expr_aux
list_aux.append_TCC2
compiler.good_compile
compiler.target_append
compiler.source_rhs_val_TCC1
compiler.prior_value_irrelevant

58 4 SUMMARY

integers.plus_TCC1
compiler.prior_value_irrelevant_aux
compiler.generate_adds_TCC1
compiler.target_interpreter_TCC1
compiler.correct_expr
list_props.every_TCC1
compiler.correct_step
compiler.source_interpreter_TCC1
compiler.compiler_TCC1
correctness depends on the following axioms:
list_adt.list_induction
correctness depends on the following definitions:
list_props.length
compiler.generate_adds
compiler.good_source_stmt?
compiler.single_dest?
compiler.source_rhs_val
compiler.source_stmt_interp
compiler.target_interpreter
compiler.target_instr_interp
compiler.compile_stmt
integers.+
list_aux.append
compiler.compiler
compiler.source_interpreter
compiler.term_value
notequal./=
list_props.every

4.3 Proof Scripts

The complete set of proof scripts can be generated by M-x show-proofs-pvs-file.

Proof scripts for file compiler.pvs:
list_aux.append_TCC2: PROVED
("" (TERM-TCC))
compiler.source_prog_TCC1: PROVED
("" (TCC)
 (TCC)
 (INST 1
       "(# lhs:= arb, rhs:=cons[term](mk_const(0),null) #)")
 (ASSERT)
 (PROPAX))

4.3 Proof Scripts 59

compiler.source_rhs_val_TCC1: PROVED
("" (TERM-TCC))

Other termination tcc proofs deleted for brevity…

compiler.prior_value_irrelevant_aux: PROVED
("" (APPLY (INDUCT-AND-REWRITE-DEFS! "l" 1 "term_value")))

compiler.prior_value_irrelevant: PROVED
("" (SKOSIMP)
    (USE "prior_value_irrelevant_aux")
    (ASSERT)
    (REPLACE-EXTENSIONALITY "(# lhs := lhs(s!1), rhs := rhs(s!1) #)"
                            "s!1")
    (ASSERT))

compiler.independence: PROVED
(""
  (APPLY
    (THEN* (INDUCT-AND-REWRITE-DEFS "t" 1) (INST? - ("dest" "dest!1")) (TCC))))

compiler.good_compile_aux: PROVED
("" (APPLY (INDUCT-AND-REWRITE-DEFS "expr" 1)))

compiler.good_compile: PROVED
("" (SKOSIMP)
    (USE "good_compile_aux" ("expr" "rhs(s!1)"))
    (REPLACE-EXTENSIONALITY "(# lhs := lhs(s!1), rhs := rhs(s!1) #)" "s!1")
    (ASSERT)
    (PROPAX))

compiler.correct_expr_aux: PROVED
("" (INDUCT "l" 1)
    (("1" (TCC))

("2" (SKOSIMP*)
(AUTO-REWRITE-THEORY "compiler")
(ASSERT)
(INST -1
      "v!1"
      "e!1 WITH [v!1 := e!1(v!1) + term_value(cons1_var!1, e!1)]")
(PROP)
(("1" (REPLACE -1 :DIR RL)
      (DELETE -1)
      (ASSERT)
      (LEMMA "prior_value_irrelevant")
      (INST -1 "(# lhs := v!1, rhs := cons2_var!1 #)" __)
      (("1" (ASSERT) (INST?)) ("2" (TCC))))
  ("2" (TCC))
  ("3" (TCC))))))

compiler.correct_expr: PROVED
("" (SKOSIMP)
(USE "correct_expr_aux")
(REPLACE-EXTENSIONALITY "(# lhs := lhs(s!1), rhs := rhs(s!1) #)" "s!1")
(ASSERT)
(PROPAX))

compiler.correct_step: PROVED
("" (SKOSIMP)
(APPLY-EXTENSIONALITY)
(DELETE 2)
(CASE-REPLACE "x!1=lhs(s!1)")
(("1" (TCC)
(REWRITE "prior_value_irrelevant" :SUBST ("x" 0))
(USE "correct_expr")
(ASSERT))
("2" (EXPAND "source_stmt_interp")
(USE "independence" ("dest" "lhs(s!1)"))
(USE "good_compile")
(ASSERT)
(PROPAX))))

compiler.target_append: PROVED
("" (APPLY (INDUCT-AND-REWRITE-DEFS "t1" 1)))

compiler.correctness: PROVED

4.4 Typeset Specification Text 61

("" (APPLY (INDUCT-AND-REWRITE-DEFS "sp" 1 "target_append" "correct_step")))

4.4 Typeset Specification Text

The specification can be typeset using the command M-x ltf (LaTEX-print file).

list aux[t : type] : theory begin

append(l_{1}, l_{2} : list[t]) : recursive list[t] = cases l_{1} of null : l_{2}, cons(hd, tl) : cons(hd, append(tl, l_{2})) endcases measure (λ (l_{1}, l_{2} : list[t]) : length(l_{1}))

end list aux

compiler : theory begin

using list aux

variable : type

arb : variable

term : datatype begin mk var(var val : variable) : is var? mk const(const val : int) : is const?

end term

env : type = [variable → int]

term value(t : term, e : env) : int = cases t of mk var(v) : e(v), mk const(i) : iendcases

crude source stmt : type = [# lhs : variable, rhs : list[term] #]

good source stmt?(s : crude source stmt) : bool =

every((λ (t : term) : is var?(t) ⇒ var val(t) ≠ lhs(s)), rhs(s)) ∧ ¬ null?(rhs(s))

source stmt : type = (good source stmt?)

source prog : type = list[source stmt]

source rhs val(l : list[term], e : env) : recursive int = cases l of null : 0, cons(t, expr) : source rhs val(expr, e) + term value(t, e) endcases

measure (λ (l : list[term]), (e : env) : length(l))

source stmt interp(s : source stmt, e : env) : env = ewith [(lhs(s)) := source rhs val(rhs(s), e)]

source interpreter(p : source prog, e : env) : recursive env = cases p of null : e, cons(stmt, rest) :

source interpreter(rest, source stmt interp(stmt, e)) endcases

measure (λ (p : source prog), (e : env) : length(p))

4.4 Typeset Specification Text 63

opcode : type = {LOAD, ADD}

target instr : type = [# op : opcode, dest : variable, src : term #]

target instr interp(i : target instr, e : env) : env = e with [(dest(i)) :=

cases op(i) of LOAD : term value(src(i), e), ADD : e(dest(i)) + term value(src(i), e) endcases]

target prog : type = list[target instr]

target interpreter(t : target prog, e : env) : recursive env = cases t of null : e, cons(instr, rest) :

target interpreter(rest, target instr interp(instr, e)) endcases

measure (λ (t : target prog), (e : env) : length(t))

generate adds(target : variable, l : list[term]) : recursive target prog = cases l of null : null, cons(t, rest) :

cons((# op := ADD, dest := target, src := t#),

generate adds(target, rest))

endcases measure (λ (target : variable), (l : list[term]) : length(l))

compile stmt(s : source stmt) : target prog =

cons((# op := LOAD, dest := lhs(s), src := mk const(0) #), generate adds(lhs(s), rhs(s)))

compiler(sp : source prog) : recursive target prog =

cases sp of

null : null,

cons(hd, tl) : append(compile stmt(hd), compiler(tl))

endcases

measure length

prior value irrelevant : lemma ∀ (v : variable), (l : list[term]), (e : env), (x : int) : let s = (# lhs := v, rhs := l#) in good source stmt?(s)

⇒ source rhs val(l, e) = source rhs val(l, ewith [(v) := x])

prior value irrelevant aux : lemma ∀ (s : source stmt), (e : env), (x : int) : source rhs val(rhs(s), e) = source rhs val(rhs(s), ewith [(lhs(s)) := x])

single dest?(dest : variable, tp : target prog) : bool = ¬ null?(tp) ∧ every((λ (i : target instr) : dest(i) = dest), tp)

independence : lemma ∀ (dest, v : variable), (t : target prog), (e : env) : single dest?(dest, t) ∧ dest ≠ v ⇒ target interpreter(t, e)(v) = e(v)

good compile : lemma (∀ (dest : variable), (expr : list[term]) :

let s = (# lhs := dest, rhs := expr #)

in good source stmt?(s) ⇒ single dest?(dest, compile stmt(s)))

good compile aux : lemma (∀ (s : source stmt) : single dest?(lhs(s), compile stmt(s)))

correct expr : lemma ∀ (v : variable), (l : list[term]), (e : env) : let s = (# lhs := v, rhs := l#) in good source stmt?(s)

⇒ source rhs val(l, e) + e(v)

= target interpreter(generate adds(v, l), e)(v)

correct expr aux : lemma ∀ (s : source stmt), (e : env) : source rhs val(rhs(s), e) + e(lhs(s))

= target interpreter(generate adds(lhs(s), rhs(s)), e)(lhs(s))

correct step : lemma ∀ (s : source stmt), (e : env) : source stmt interp(s, e) = target interpreter(compile stmt(s), e)

target append : lemma ∀ (t_{1}, t_{2} : list[target instr]), (e : env) : target interpreter(append(t_{1}, t_{2}), e)

= target interpreter(t_{2}, target interpreter(t_{1}, e))

correctness : theorem ∀ (sp : source prog), (e : env) : source interpreter(sp, e) = target interpreter(compiler(sp), e)

end compiler

4.5 Cross-Reference to Specification Identifiers 65

4.5 Cross-Reference to Specification Identifiers

Finally, a cross-reference to the identifiers defined in the specification can be produced by the command M-x list-declarations. The $ characters indicate truncation (the treatment of long identifiers will be improved in a future release of PVS).

Declaration               Type                      Theory
append                    [list[t], list[t] -> lis$ list_aux
arb                       variable                  compiler
compile_stmt              [source_stmt -> target_p$ compiler
compiler                  [source_prog -> target_p$ compiler
correct_expr              lemma                     compiler
correct_expr_aux          lemma                     compiler
correct_step              lemma                     compiler
correctness               theorem                   compiler
crude_source_stmt         type                      compiler
env                       type                      compiler
generate_adds             [variable, list[term] ->$ compiler
good_compile              lemma                     compiler
good_compile_aux          lemma                     compiler
good_source_stmt?         [crude_source_stmt -> bo$ compiler
independence              lemma                     compiler
opcode                    type                      compiler
prior_value_irrelevant    lemma                     compiler
prior_value_irrelevant_a$ lemma                     compiler
single_dest?              [variable, target_prog -$ compiler
source_interpreter        [source_prog, env -> env] compiler
source_prog               type                      compiler
source_rhs_val            [list[term], env -> int]  compiler
source_stmt               type                      compiler
source_stmt_interp        [source_stmt, env -> env] compiler
target_append             lemma                     compiler
target_instr              type                      compiler
target_instr_interp       [target_instr, env -> en$ compiler
target_interpreter        [target_prog, env -> env] compiler
target_prog               type                      compiler
term_value                [term, env -> int]        compiler
variable                  type                      compiler

5 Conclusions

TBD. In particular, comparison with the Boyer-Moore version.

References

[1] R. S. Boyer and J S. Moore. A Computational Logic Handbook. Academic Press, New York, NY, 1988.

[2] S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), pages 748–752, Saratoga, NY, June 1992. Volume 607 of Lecture Notes in Artificial Intelligence, Springer-Verlag.

[3] N. Shankar. Abstract datatypes in PVS. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA, December 1993. Forthcoming.

[4] J. M. Spivey, editor. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science. Prentice Hall, Hemel Hempstead, UK, 1989.

[5] Debora Weber-Wulff. Proof Movie—a proof with the Boyer-Moore prover. Formal Aspects of Computing, 5(2):121–151, 1993.