Interpreter Verification for a Functional Language

Manfred Broy, Ursula Hinkel, Tobias Nipkow^{⋆}, Christian Prehofer^{⋆⋆}, Birgit Schieder

Technische Universität München^{⋆⋆⋆}

Abstract. Starting from a denotational and a term-rewriting based operational semantics (an interpreter) for a small functional language, we present a correctness proof of the interpreter w.r.t. the denotational semantics. The complete proof has been formalized in the logic LCF and checked mechanically with the help of the theorem prover Isabelle. This substantial proof is analyzed in some detail and conclusions for mechanical theorem proving in general are drawn.

1 Introduction

Methods for establishing the correctness of complex software systems have been studied for many years. They are of immense practical importance, especially for highly critical applications, because they can guarantee the desired functionality of software systems.

Proof methods for high level programs, however, help only to establish the correctness of the final software system in operation, if the used compilers and interpreters are correct. Otherwise the carefully verified high level programs might be compiled or interpreted incorrectly. Proving the correctness of machine oriented programs [3] instead may be inevitable for some applications, but is a methodological backwards step. Therefore compiler and interpreter correctness proofs are subjects of major interest in computer science.

Verification of compilers and interpreters is also challenging from a theoretical point of view because complex semantical questions are involved [5, 6]. These comprise the formalization of semantical definitions and proof methods that are powerful enough to show the equivalence between quite different definitions of the semantics of programming languages.

When proving compilers correct, one of the difficulties is the treatment of recursion, which is handled by the fixpoint operator in the denotational semantics of the source language and by a stack discipline and gotos at the level of machine programs. This problem is dealt with in [4]. In the verification of interpreters

⋆ Research supported by ESPRIT BRA 6453, TYPES ⋆⋆ Research supported by DFG grant Br 887/4-2, Deduktive Programmentwicklung ⋆⋆⋆ Institut für Informatik, 80290 München, Germany.

  E-mail: {broy,hinkel,nipkow,prehofer,schieder}@informatik.tu-muenchen.de

similar problems have to be solved: here, recursive definitions are treated by unfolding at the level of syntax. Technically, the operational semantics defined by an interpreter is formalized by a recursive function transforming syntactic terms of the source language. This paper describes the correctness proof of an operational with respect to a denotational semantics for a small functional language. The main contributions are:

– The complete proof has been machine checked with the help of Isabelle [18], a generic theorem prover.

– Our notion of correctness of an interpreter is significantly stronger than most correctness conditions considered in other machine-checked compiler or interpreter proofs. We prove that whenever the outcome of a program is defined according to the denotational semantics, the operational semantics leads to a terminating computation with the same outcome. Thus we prove partial and total correctness by a single verification condition.

The paper is structured as follows. In Section 2 the syntax of the functional language, its denotational semantics, the definition of the interpreter and the basic correctness condition are given. In Section 3 the verification support system Isabelle/LCF is explained by describing its syntax, its basic type concept and its induction proof principle. In Section 4 the proof task is formalized in Isabelle/LCF. In Section 5 the structure and size of the proof is described. In Section 6 general aspects of machine support for large proofs are discussed.

2 The Interpreter and its Correctness

We define syntax and denotational semantics of FOFL, a first-order functional language, and an interpreter for it. Then we outline a correctness proof of the interpreter. FOFL is purposely kept small in order to focus on the main nontrivial aspect: proving the interpretation of recursively defined functions correct. Our interpreter is given as a recursively defined function, whereas in the literature, e.g. [22, 9], operational semantics is often given by means of inference rules. Therefore our verification task differs from those in the literature.

2.1 Syntax

FOFL contains function application, conditional expressions, and recursive function definitions. Let Φ be a set of predefined function symbols with at least two constants true, false ∈ Φ, let F a set of user-definable function symbols, and let V a set of variables. Each function symbol has a fixed finite arity.

The set T of terms is defined inductively:

– x ∈ T for every variable x ∈ V.

– φ(t_{1}, …, t_{n}) ∈ T is an application of a predefined function symbol φ ∈ Φ of arity n to terms t_{1}, …, t_{n} ∈ T.

– f(t_{1}, …, t_{n}) ∈ T is an application of a user-definable function symbol of arity n f ∈ F to terms t_{1}, …, t_{n} ∈ T.

– if t_{0} then t_{1} else t_{2} fi ∈ T for all terms t_{0}, t_{1}, t_{2} ∈ T

– (fix f(x_{1}, …, x_{n}) = t_{0})(t_{1}, …, t_{n}) ∈ T is the application of a recursively defined function f ∈ F (with formal parameters x_{1}, …, x_{n} ∈ V and body t_{0}) to terms t_{0}, …, t_{n} ∈ T.

The set P of programs consists of all closed terms (that is, terms without free variables).

FOFL is first-order because functions cannot have functions as arguments or return them as results.

2.2 Denotational Semantics

We follow the standard theory of denotational semantics, see e.g. [13]. Let D be a set of data values equipped with a flat order. The algebra A assigns a continuous function φ^{A} to each predefined function symbol φ ∈ Φ. Env is the set of environments that assign data values to variables, and functions to user-defined function symbols. The functions lookupvar and lookupfct yield the values assigned to variables and functions, respectively, by an environment η. The operator FIX yields the least fixpoint of a functional. We write IF . THEN . ELSE . FI for the conditional on the meta-level. The notation [./.] is overloaded and denotes substitution as well as update of functions. It is used as a postfix operator.

The denotational semantics of terms is defined by a function

T : T → Env → D

specified as follows:

T [[x]]η = lookupvar x η
T [[φ(t_{1}, …, t_{n})]]η = φ^{A}(T [[t_{1}]]η, …, T [[t_{n}]]η)
T [[f(t_{1}, …, t_{n})]]η = (lookupfctf η)(T [[t_{1}]]η, …, T [[t_{n}]]η)
T [[if t_{0} then t_{1} else t_{2} fi]]η = IF T [[t_{0}]]η THEN T [[t_{1}]]η ELSE T [[t_{2}]]η FI
T [[(fix f(x_{1}, …, x_{n}) = t_{0})(t_{1}, …, t_{n})]]η = (FIX τ)(T [[t_{1}]]η, …, T [[t_{n}]]η)
where τ = λg.λd_{1}, …, d_{n}.T [[t_{0}]]η[d_{1}/x_{1}, …, d_{n}/x_{n}, g/f]

2.3 The Interpreter

Let W be the set of all closed terms over Φ. Let a continuous boolean function normal be given, which yields true on a subset of W. The terms of this subset are called normal forms. Among them are true and false. The continuous function eval evaluates each term of W to its unique normal form. If t is a term in W, we write t^{A} for its interpretation in the algebra A.

The interpreter is based on the function reduce, which performs a single reduction step on a program t ∈ P:

t ∈ W ⇒ reduce[[t]] = eval[[t]]
φ(t_{1}, …, t_{n}) ∉ W ⇒ reduce[[φ(t_{1}, …, t_{n})]] = φ(reduce[[t_{1}]], …, reduce[[t_{n}]])
¬normal[[t_{0}]] ⇒ reduce[[if t_{0} then t_{1} else t_{2} fi]] =
if reduce[[t_{0}]] then t_{1} else t_{2} fi
reduce[[if true then t_{1} else t_{2} fi]] = t_{1}
reduce[[if false then t_{1} else t_{2} fi]] = t_{2}
reduce[[(fix f(x_{1}, …, x_{n}) = t_{0})(t_{1}, …, t_{n})]] =
t_{0}[(fix f(x_{1}, …, x_{n}) = t_{0})/f, t_{1}/x_{1}, …, t_{n}/x_{n}]

The interpreter is recursively defined by the function val, which applies reduce to a program t until a normal form is reached:

val[[t]] = IF normal[[t]] THEN t ELSE val[[reduce[[t]]]] FI

2.4 Interpreter Correctness Proof

We call an interpreter correct with respect to a denotational semantics if the following property holds: whenever the denotational semantics assigns a defined value to a program, then the interpreter terminates with the same value. Since the data domain D carries a flat order, we can state interpreter correctness formally as follows, where void denotes the empty environment:

∀t ∈ P : T [[t]]void ⊑ val[[t]]^{A}  (1)

A proof by structural induction over t looks promising, but there is a problem. In the case of function definitions

(fix f(x_{1}, …, x_{n}) = t_{0})(t_{1}, …, t_{n})

the denotational semantics is defined via

T [[t_{0}]]η[d_{1}/x_{1}, …, d_{n}/x_{n}, g/f].

The induction hypothesis is not applicable for two reasons: t_{0} need not be a closed term and the environment η[d_{1}/x_{1}, …, d_{n}/x_{n}, g/f] is not empty. Hence we face a typical problem of proofs by induction: the induction hypothesis is not strong enough and must therefore be generalized.

The main difficulty consists in finding a suitable generalization of the correctness condition. As we have seen, we need inequations of the form T [[t]]η ⊑ val[[u]]^{A}, where t is not necessarily closed, η not necessarily empty, and u a closed term. Since this inequation does certainly not hold for all such t, η, and u, we must find a relation ∼ between terms and environments on the one hand, and interpreted programs on the other hand, such that ∼ has the following properties:

1. The implication (t, η) ∼ u ⇒ T [[t]]η ⊑ val[[u]]^{A} is provable by structural induction over t.

2. For all closed terms t we have (t, void) ∼ t.

Proposition (1) follows directly from these conditions.

We will not give the exact definition of ∼, but describe it only informally. We say that (t, η) ∼ u holds if u is obtained from t by a substitution with the following two properties:

– For each free variable x of term t the following holds: the environment η assigns a value to x that is less or equal to the result of interpreting the term that is substituted for x in u. This property will be called W V (weaker in variable) in Sect. 5.

– For all user-definable function symbols f the following holds: if the environment η assigns a function to f, then this function is less or equal to the result of interpreting the declaration that is substituted for f in u. If η does not assign a function to f, then f is not substituted in u. This property will be called W F (weaker in function) in Sect. 5.

The generalized correctness condition reads:

∀t ∈ T, ∀η ∈ Env, ∀u ∈ P : (t, η) ∼ u ⇒ T [[t]]η ⊑ val[[u]]^{A}  (2)

We prove this generalized correctness condition by structural induction over t. The most difficult case is application of a function definition (fix f(x_{1}, …, x_{n}) = t_{0})(t_{1}, …, t_{n}). We must find and prove an auxiliary property: the least fixpoint of the functional associated with the declaration is less or equal to the result of interpreting the function definitions. This property is proved by fixpoint induction inside the structural induction.

The remaining cases of t are not difficult to prove, but require a lot of technical lemmata. These lemmata primarily concern invariance of ∼, and substitutions. The whole hand-written proof consists of about 70 pages. More details can be found in [21].

3 Isabelle/LCF

The proof described in the previous section does not make use of a specific logical system but relies on general notions from domain theory, e.g. ⊥, ⊑ and fixpoints. The obvious choice for a machine-assisted version of the proof is LCF [8], a Logic for Computable Functions, which formalizes standard domain theory. Having fixed the precise logic, we still had a choice between (at least) three theorem provers which support this logic: two versions of Cambridge LCF [17] (in Classic ML and Standard ML) and Isabelle/LCF. The first two systems are dedicated solely to theorem proving in LCF. Isabelle [14, 19], on the other hand, is a generic theorem prover which supports a host of other logics apart from LCF, e.g. First-Order Logic (FOL), Zermelo-Fraenkel set theory (ZF) and Higher-Order Logic (HOL). Isabelle can be instantiated with the syntax and proof rules of the object logic; Isabelle/LCF is the LCF instantiation of Isabelle.

Cambridge LCF, although state of the art when it was conceived, is now slightly dated, whereas Isabelle offers many new principles for interactive theorem proving: schematic variables (“logical variables” in Prolog parlance), higherorder unification and proof search via backtracking. On the user level these features manifest themselves in the form of powerful proof procedures, e.g. for FOL, which are a definite advance in automation over what Cambridge LCF has to offer. Thus we opted for Isabelle/LCF, which is an extension of Isabelle/FOL and follows the logic LCF as described by Paulson [17] as closely as possible. We will therefore concentrate on the differences between LCF and Isabelle/LCF.

3.1 Syntax

Due to Isabelle’s flexible front-end, the only syntactic difference is that curried application f x y, where f : τ_{1} → τ_{2} → τ_{3}, is written f(x, y). Correspondingly, τ_{1} → τ_{2} → τ_{3} may be written [τ_{1}, τ_{2}] → τ_{3}. As in LCF, ⊥ and ⊑ are rendered in ascii as UU and <<.

3.2 Types

Isabelle offers a type system which is fairly close to that of LCF, namely MLstyle polymorphism. However, LCF has both continuous functions, which are identified with Isabelle’s built-in function type, and predicates. Predicates are formalized in Isabelle as functions with result type o, the type of formulae. Thus Isabelle/LCF needs to support two kinds of functions, because predicates need not be continuous (even if o were turned into a domain). Otherwise one could define X ≡ F IX(λP.¬P) and derive the contradiction X ↔ ¬X.

This problem can be solved using Isabelle’s type classes, an overloading scheme similar to the one in the functional programming language Haskell [11, 15]. In Isabelle/LCF we simply declare a new class cpo, which is the class of all domains. We can now restrict certain constants to be available only at types which are of class cpo: ⊥ : ∀α:cpo.α, ⊑ : ∀α:cpo.[α, α] → o, F IX : ∀α:cpo.(α → α) → α. In all three cases the type variable α ranges only over types of class cpo. The type o is not of class cpo, thus ruling out the term X above. If a type is declared to be in class cpo, e.g. nat : cpo, this means we can write formulae like ⊥ ⊑ 0. Of course the behaviour of ⊑ on nat has to be axiomatized explicitly and does not follow automatically from nat : cpo.

Finally we need to say that τ_{1} → τ_{2} is of class cpo provided both τ_{1} and τ_{2} are. However, this is only true if all terms of type τ_{1} → τ_{2}, where τ_{1}, τ_{2} : cpo, are constructed from continuous functions by abstraction and application. Unfortunately one can construct λx.f(g(x)), where g : τ_{1} → σ, f : σ → τ_{2} and σ is not a domain, and hence the composition of f and g need not be continuous. Fortunately, this situation can be ruled out quite easily:

1. All types except o are required to be domains, i.e. of class cpo.

2. There are no functions of type o → τ where τ : cpo.

These restrictions correspond exactly to the ones in LCF where all types must be domains (there is no type of formulae), and there are no functions taking formulae as arguments.

The restriction that all types must be domains is a fairly severe one and causes many complications. Regensburger [20] solves this dilemma by a semantic embedding of LCF in Isabelle/HOL which allows to construct a separate space of continuous functions.

3.3 Induction

The only induction principle for LCF is fixpoint induction:

\frac{P (⊥) ∀x.P (x) → P (f(x))}{∀x.P (x)}

where P (x) must be admissible [17]. In Cambridge LCF, the test for admissibility is an ML function which checks certain sufficient syntactic conditions. Most of these can be expressed as inference rules and have thus found their way into Isabelle/LCF. In this respect Isabelle/LCF is a little weaker than Cambridge LCF, which turns out not to be a problem in practice.

Paulson [17] shows how to derive structural induction from fixpoint induction and Cambridge LCF automates this derivation. Since Isabelle/LCF does not yet provide this automation, structural induction schemata were added explicitly.

4 The Specification

The abstract syntax of FOFL, its denotational and operational semantics, and the relation necessary for the correctness proof are all formalized as extensions of Isabelle/LCF. In this section we present some aspects of these formalizations and discuss the adequacy of Isabelle as a specification language.

The syntax of FOFL is represented by the type T. Its constructors correspond to the different syntactic forms of the language. Isabelle’s mixfix notation enabled us to use the following readable syntax:

T ::= var(x) | cst(g) | cstf g [T] | fun f [T] | cons[T,T]
    | if T then T else T fi | fix f(x) = T [T]

This syntax is based upon the types V of variables, F of user-definable function symbols and Φ of predefined function symbols. These auxiliary types are not specified any further.

Let us examine the different cases in detail.

var(x) is the variable x : V. cst(g) is the predefined constant g : Φ. cstf g [t] is the application of the unary predefined function g : Φ to an

argument t. fun f [t] is the application of the user-defined function f : F to an argument

t. cons[t_{1},t_{2}] is the pair (t_{1}, t_{2}). fix f(x) = t_{0} [t_{1}] is the application of the recursive function f : F with

formal parameter x : V and body t_{0} to an argument t_{1}.

Note that since we have constants, unary functions and pairs, we can express arbitrary n-ary functions.

As mentioned above, Isabelle/LCF does not provide a package for defining data types like T automatically. Hence the necessary induction and freeness axioms for T were asserted explicitly.

As an example of a FOFL program we present the recursively defined function length computing the length of a list and apply it to some argument list

cons[cst(a), cst(b)]. The function symbols 0, succ, is_empty and tail have

their usual fixed interpretation.

  fix length(xs) = if cstf is_empty [var(xs)] then cst(0)
                   else cstf succ [fun length [cstf tail [var(xs)]]]
  [cons[cst(a), cst(b)]]

For the specification of the denotational semantics it was essential that Isabelle offers higher order constructs and λ-abstraction. We introduce the function den (T in Sect. 2) which evaluates a term relative to two environments:

den : [T, (V, D)map, (F, D → D)map] → D

The type constructor (α, β)map realizes finite functions from α to β. Its definition is not shown. The two environments provide semantic values for free variables: (V, D)map maps first-order variables V to data values D and (F, D → D)map maps user-defined function symbols F to functions from D to D.

The translation of the different clauses for T in Sect. 2 is fairly straightforward. As an example we look at the case of fix. First we define a functional

tau : [F, V, T, (V, D)map, (F, D)map] → (D → D) → (D → D)

which corresponds to the term τ in Sect. 2 and is parameterized by the name of the recursive function, the name of its formal parameter, its body, and the two environments:

  tau(f, x, t0, envV, envF) = (%g d. den(t0, envV[d/x], envF[g/f]))

In Isabelle the symbol % is the ascii rendition of λ; tau realizes one step in the approximation of the recursive function. LCF’s fixpoint operator F IX is used to define the denotational semantics of recursive functions in FOFL:

  t1 ~= UU ==> den(fix f(x) = t0 [t1], envV, envF) =
               FIX (tau(f, x, t0, envV, envF)) (den(t1, envV, envF))

The premise t_{1} ≠ ⊥ is necessary because we have chosen to define all constructors of T to be strict, i.e. (fix f(x) = t_{0} [⊥]) = ⊥.

The remaining clauses for den and the definition of the operational semantics in Isabelle closely follow the original specification in Sect. 2.

The overall specification defines 45 functions with 138 axioms. Most of the complexity comes from the full formalization of substitution. Fortunately, Isabelle’s type system offers parametric polymorphism, which enabled us to define finite sets and maps once (following Paulson [16]) and use them repeatedly. Both the denotational (den above) and the operational semantics rely heavily on environments, i.e. maps, of all kinds.

5 The Correctness Proof in Isabelle

Next we discuss the mechanical verification of the interpreter. Starting from the proof in Sect. 2, it took a student with no previous experience with proof assistants approximately four months [10] to redo the whole proof in Isabelle, including the time to formalize the specification.

The guiding principle was a top down development of the proof. We first studied the top level of the proof of the generalized correctness condition (2):

  ((t, envV, envF) REL u) --> den(t, envV, envF) << ipret(val(u))

The definition of REL (see below) corresponds to the definition of ∼ in Sect. 2, the function ipret denotes the interpretation of terms.

The main theorem is shown by structural induction on t : T; fixpoint induction is required in the subcase for recursively defined functions. The proof of the main theorem is based on a large body of lemmata about substitution and the interpreter function val. Rather than developing theories for substitutions and val first, we isolated the required lemmata during the proof of the main theorem, asserted them as additional axioms, postponing their proof until later.

Surprisingly, proving the auxiliary theorems for the interpreter function val and for substitution involved a lot more work than proving the main theorem. Unfortunately, this is a phenomenon which is familiar from many case studies in machine checked proofs. Data structures such as numbers and lists, which the human mind manipulates quite easily (because of strong geometrical intuitions), require a large amount of work when dealt with by machine, unless the proof checker offers special support in the form of decision procedures for these domains.

Except for one, all theorems concerning the function val were proved by fixpoint induction. Some theorems required more than 50 tactic steps. The theorems about substitutions are highly technical and rather tedious to prove. Almost every theorem required structural induction and additional lemmata about free variables and closed terms. A typical example is a theorem stating that substitution on a term without free variables has no effect on the term. Proving this theorem took more than 50 commands. One statement about the composition of substitution resulted in more than 100 commands.

[htb]

Purpose of Lemmata  Number of Lemmata
general purpose  156
substitution  46
free variables, closed terms  52
properties of the interpreter, i.e. val  33
main theorem  24

Fig. 1. Structure of Lemmata

The lemmata can be divided into independent classes, as shown in Fig. 1. Most general purpose lemmata required merely a few commands.

As very large formulae are employed in the proofs we introduced abbreviations in order to hide details. Such abbreviations are of the form t == u and can be expanded and folded during a proof. Two important abbreviations used are

  denot_less_oper(t) ==
    ALL envV envF u.
      ((t, envV, envF) REL u) --> den(t, envV, envF) << ipret(val(u))

and

((t, envV, envF) REL u) ==
(t ~= UU & u ~= UU & is_ct (u) &
(EX substV :: (V,T)map. EX substF :: (F,decl)map.
  (substV ~= UU & substF ~= UU &
   u = subst(t, substV, substF) &
   (ALL x.(x: FV_x(t) = TT) --> WV(substV, envV, x)) &
   (ALL f.(f: FV_f(t) = TT) --> substF def f = TT & is_cdecl(substF @ f))
   (ALL f. (envF def f = FF --> substF def f = FF) &
           (envF def f = TT --> WF(substF, envF, f) )))))

where WF and WV are further abbreviations not shown here.

Not only can the main theorem can now be stated concisely as

  ALL t. denot_less_oper(t)

its inductive proof is also greatly simplified because the induction hypothesis is still readable.

5.1 Tactics

Theorem proving in Isabelle is an interactive process. The user states the desired theorem to Isabelle and guides the proof by choosing the proof techniques and envoking appropriate tactics. Tactics are user-definable proof strategies and can be anything from the application of a single inference rule (single-step) to fullblown decision procedures which can construct subderivations of arbitrary size.

Tactic  Number of Applications
Simplification  680
Single-step^{\{ \begin{matrix}forward \\ backward \\ explicit instantiation \end{matrix}}  \begin{matrix}369 \\ 547 \\ 130 \end{matrix} \} 920
Classical prover  173
Other  555
Total  approx. 2400

Fig. 2. Tactics used in the Verification

Altogether our proof consists of approximately 2400 user interactions. These can be analyzed as shown in Fig. 2 depending on the facillities used.

The Isabelle tactics in the above table, e.g. the classical prover, are explained and discussed in the following. For more details consult [18]. The order in the above table roughly reflects the user effort involved. For instance, the simplifier is fast and easy to use, whereas the (automatic) classical prover is slow and its success is hard to predict.

Isabelle’s simplifier goes beyond classical first-order term rewriting. Its many enhancements and flexiblity explain its extensive use to some degree. Simplification can either be limited to the conclusion of a subgoal or can include the premises as well. Local assumptions are used as additional rewrite rules: simplifying the formula x = 5 --> y = x results in x = 5 --> y = 5. Conditional equations are used as rewrite rules where the conditions are solved recursively before the conclusion is applied.

Isabelle provides several commands for single-step forward or backward reasoning, all of them variations on resolution. For instance structural and fixpoint induction are envoked by a backward resolution step. Reasoning forward from the assumptions can be tricky if there are multiple assumptions matching the premises of the rule to be used. In many cases Isabelle’s higher-order unification finds the correct assumption automatically. In only 15% of all applications of resolution did we have to provide explicit instantiations to guide the search.

Isabelle’s classical prover is based on the sequent calculus plus some heuristics. It offers purely automatic tactics which simulate the classical sequent calculus. Depth-first or best-first search is available. The user can adapt the classical prover to her domain by adding further deduction rules. We used the classical prover only to solve simple theorems. When dealing with more complicated proofs we mostly chose term rewriting or resolution because their effect is more predictable.

Response time is an important aspect of interactive proving. The tactics for term rewriting and resolution are very fast — they normally return within seconds compared to the automatic tactics which sometimes take up to minutes. This is another reason why we preferred term rewriting and resolution. Executing the whole proof takes 40 minutes (on a Sun Sparc 10).

Isabelle encourages users to construct new tactics by composing existing tactics via tacticals, thus customizing the prover for their particular application. However, it may take some time until a user recognizes typical proof situations and finds suitable tactics. Once found, they allow for shorter and more abstract proofs. This was particularly important for us, because our proofs were undergoing frequent change, and small proofs are easier to maintain than large ones.

6 Proving in the Large

In this section we will discuss some general aspects of large verification tasks. The following is thus a summary of the lessons we have learned and is of course biased by our case study. Let us first recall some often stated properties of interactive proof:

– Proofs can grow to a huge size, and it is a serious problem to extract the important information from a proof (state).

– Interactive proofs are produced incrementally, which has implications for the kinds of proof procedures that are useful. For instance, procedures that transform the proof into a low-level representation such as clauses are not useful at intermediate steps. (They have, however, proved very useful when applied as concluding steps in interactive proofs.)

– Proofs have to meet a range of sometimes conflicting criteria, among them: efficiency, elegance, readability, robustness under change, reusability, etc. Conflicts arise because some users are interested in the proof as an object of study (typically mathematicians or logicians), and others are primarily interested in getting the theorem by whatever means possible (those involved in a large verification, for example).

With these observations in mind, we now turn to a few general issues concerning the support by theorem provers.

6.1 Structuring Proofs

Although most verification tasks require only a few core ideas, a major problem is to organize the often large and tedious proof obligations. Ideally, one would like to structure a proof in many abstract definitions and small lemmata until the proofs are easy. This is typically done in math books. We believe, however, that this is very hard in software verification where the details are overwhelming. First of all, this divide and conquer approach usually takes many attempts, often by skilled people, to find the right structuring. Although structuring is essential, mechanical verification requires a much more detailed and careful decomposition than typical proofs on paper. For instance, mathematicians often achieve elegant proofs by simply leaving most things implicit and by changing the perspective, which is hard to model formally. We identified the following concepts to alleviate this problem:

– Definitions and abbreviations are essential for structuring and decomposing larger proofs. With large systems, properties (e.g. invariants) of systems easily grow to pages. In mathematics finding the right definitions and notation is often essential; this holds to a much larger extent for complex software systems. Usually, abbreviations are global, but they may be also local to a proof. For instance, stating theorems as often done in math books yields local abbreviations. Typically, theorems are stated as “Let p = …, q = … such that P (p, q). Then Q(p, q) holds”. In a theorem prover this is stated as p = …, q = …, P (p, q) ⊢ Q(p, q). Now it is important that the system gives the user the control over expanding such local abbreviations. However, definitions not only need expanding but also contracting. This is often ignored because it requires higher-order rewriting: the left-hand side of a definition is a first-order term, whereas the right-hand side can be considerably more complex. For instance the abbreviation denot_less_oper above contains quantifiers on the right-hand side, which means that matching modulo αconversion is required. Introducing abbreviations during an interactive proof would often be convenient, but is rarely available. Notable exceptions are type theoretic systems like Coq [7].

– Structuring large proofs vertically: divide and conquer Apart from abbreviations, the only effective tool for structuring large verifications is the division into subtheories and lemmata. It is well known that verification begins with the design of a system. A clear and systematic design is is essential for successful verification. Case studies with functional programs [1] suggest writing a program in small units, in the hope that properties of these are easier and more compact to state.

– Structuring large proofs horizontally: intermediate lemmata It is frequently necessary to introduce intermediate lemmata which are superfluous from a human point of view but are necessary to convince the theorem prover of the correctness of a proof step. In contrast to vertical structuring, these lemmata are tailored only towards a particular theorem prover. Most of them are tedious to find and obscure. Theorem provers with a high degree of automation and a low degree of user control, e.g. Boyer-Moore [2] and Ontic [12], often require such intermediate lemmata to guide the search.

Of course vertical structuring is to be preferred over horizontal structuring, even if the latter may facilitate automation in some cases. In our case study the efforts to structure the proof vertically turned out to be essential for success. Yet for several proofs horizontal structuring by intermediate lemmata was used, although a detailed and well structured proof on paper was available. One reason was that many seemingly simple lemmata required a large number of interactive steps, which made intermediate lemmata necessary.

6.2 Automated Proof Support

For interactive verification, strong and incremental automated proof support is necessary to avoid wasting the user’s time on easily proved theorems. Ideally, the user only has to give very abstract input to the prover, such as “do rewriting”, or “use decision procedures”. For instance, the Boyer-Moore system [2] is designed for automatic proof without any input from the user, except for providing some “hints”. However, in our case studies we found that finer control is frequently necessary. Now the problem is that in many proof systems there is a wide gap between the automatic facilities and the low-level stepwise facilities: for lack of a middle ground, the user is too often forced to work at an unnaturally low level. The following different levels of user control seem very natural, but are rarely fully supported:

1. In the first refinement, the user gives the prover hints on what to use, e.g., suggesting certain rewrite rules, lemmata or proof strategies.

2. The user sometimes wants to have more control over where to use a tactic. For instance, one might want to apply simplification only to a particular premise of the goal.

3. Even more control can be exercised by specifying how a step should be done, e.g., by providing explicit substitutions for instantiating a lemma.

For instance, in our case study higher-order unification combined with backtracking was used as a schematic method to compute desired instantiations of logic variables. This often relieves the user of the burden to provide concrete substitutions. Thus tactics can be expressed more abstractly, e.g. a tactic may roughly express “apply rule x in such a way that rule y applies afterwards”. This is useful to avoid low-level proofs in situations where fully automatic support fails.

Abstract high-level proof methods facilitate reuse, as shown in our work: we first completed the verification for one language. Changing the syntax of the language invalidated most proofs, but redoing the proofs was a matter of days. Similarly, we added new constructs to the language, while being able to reuse most of the proof successfully.

In some cases, however, users knowing the proof in detail still insist on using low-level proof methods. For difficult proof steps, where automatic methods fail, low-level support is needed and sometimes may be faster (in user and system time) than attempting higher-level support. Higher-level proofs, however, are clearly desirable, in particular for reusing proofs. Acknowledgments. We thank Konrad Slind for his contributions to Section 6.

References

1. M. Aagaard and M. Leese. Verifying a logic synthesis tool in Nuprl: A case study in software verification. In Proc. 4th Workshop on Computer Aided Verification. LNCS, 1992.

2. Robert S. Boyer and J Strother Moore. A Computational Logic Handbook. Academic Press, 1988.

3. Robert S. Boyer and Yuan Yu. Automated correctness proofs of machine code programs for a commercial microprocessor. In Deepak Kapur, editor, 11th International Conference on Automated Deduction, LNAI 607, pages 416–430, Saratoga Springs, New York, USA, June 15–18, 1992. Springer-Verlag.

4. M. Broy. Experiences with software specification and verification using LP, the Larch proof assistant. Technical Report SRC 93, DIGITAL Systems Research Center, November 1992.

5. B. Buth, K.-H. Buth, Arting Fränzle, B. v. Karger, Y. Lakhmeche, H. Langmaarck, and M. Müller-Olm. Provably correct compiler developement and implementation. In Compiler-Construction ’92. Springer-Verlag, LNCS, 1992.

6. Paul Curzon. A verified compiler for a structured assembly language. In Procc. of the 1991 International Workshop on Higher Order Logic Theorem Proving and its applications. North-Holland, 1992.

7. G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq proof assistant user’s guide version 5.8. Technical Report 154, INRIA, May 1993.

8. M.C.J. Gordon, Robin Milner, and C.P. Wadsworth. Edinburgh LCF: a Mechanised Logic of Computation. LNCS 78, 1979.

9. Carl A. Gunter. Semantics of Programming Languages. MIT Press, 1992.

10. Ursula Hinkel. Maschineller Beweis der Korrektheit eines Interpreters. Master’s thesis, TU München, 1993. In German.

11. Paul Hudak, Simon Peyton Jones, and Philip Wadler. Report on the programming language Haskell: A non-strict, purely functional language. ACM SIGPLAN Notices, 27(5), May 1992. Version 1.2.

12. D. McAllester. Ontic: Tools for an inference laboratory. In E. Lusk and R. Overbeek, editors, Proc. 9th Int. Conf. Automated Deduction. Springer LNCS, 1988.

13. P. D. Mosses. Denotational semantics. In J. van Leeuwen, editor, Handbook of TCS, volume B. Elsevier, 1990.

14. Tobias Nipkow and Lawrence C. Paulson. Isabelle-91. In Deepak Kapur, editor, Proc. 11th Int. Conf. Automated Deduction, pages 673–676. LNCS 607, 1992.

15. Tobias Nipkow and Christian Prehofer. Type checking type classes. In Proc. 20th ACM Symp. Principles of Programming Languages, pages 409–418. ACM Press, 1993. Revised version to appear in J. Functional Programming.

16. Lawrence C. Paulson. Deriving structural induction in LCF. In G. Kahn, D. B. MacQueen, and G. Plotkin, editors, Semantics of Data Types, pages 197–214. Springer, 1984. LNCS 173.

17. Lawrence C. Paulson. Logic and Computation. Cambridge University Press, 1987.

18. Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361–385. Academic Press, 1990.

19. Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume ??? of Lect. Notes in Comp. Sci. Springer-Verlag, 1994. To appear.

20. Franz Regensburger. HOLCF: Eine konservative Erweiterung von HOL um LCF. PhD thesis, Technische Universität München, 1994. To appear.

21. Birgit Schieder. Logic and Proof Method of Recursion. PhD thesis, TU München, 1994. To appear.

22. Glynn Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993.