A Proof-Checker for Dynamic Logic

Introduction

A PROOF-cHECKER FOR DYNAMIC LOGIC

S.D. Litvintchouk and V.R. Pratt Massachusetts Institute of Technology Cambrid11e, MA 02.139

is borrowed from modal logic. Dynamic logic is more intimately connected with modal logic than one might at first suppose; the connection is discussed in more detail in ·section 3.2. of [2.1]. Fischer and Ladner [6] demonstrate the connection between various restrictions of dynamic logic and the classical systems K, T, S4 and SS of modal logic. We call [a] and <«> modalities (respectively box and diamond modalities), and formulae of the form [«lP and <a>P modal formulae. We shall call a quantifier-free logic augmented with such modalities a dynamic logic. Syntactically, modalities behave exactly like logical negation; they are placed in front of a formula, and their precedence is such that [alPAQ is parsed ([aJP)AQ, just as .,p/\Q would have been parsed (-,P)AQ.

The programming language

In order to understand the meaning of a formula such as .,[X:=llfalse, we first need a precise account of X:=l. We shall think or programs solely in terms of their effect on the state of the world. A state is defined by the values taken on by the function and predicate symbols of the language in some domain. (A logician would call a state an interpretation.) We call the set of all possible states (keeping the domain fixed) the universe. Thus a universe is defined by the available function and predicate symbols and the choice or domain.

We could restrict our attention to deterministic programs, permitting US to think of them as functions from ·States to states. As we shall see later however, reasoning nondeterministically about deterministic programs can simplify the argument. Hence we shall allow for nondeterministic programs by capturing the effect of a program on a universe as a binary relation on that universe. This of course means that we will be able to discuss nondeterministic programs in general. However, the question of what first-order facts one wants to assert about nondeterministic programs is presently the subject of much discussion in the literature (see [5] in particular), and we shall avoid that issue in this paper beyond observing that dynamic logic as presented here can express many user ul ideas about nondeterministic programs.

Prosramming constructs

The programs we want to discuss have five constructs. These constructs, while not all entirely conventional, have been chosen primarily for the ease with which one can discuss programs written using them.

(i) Assignments. X:=l is an instance of an assignment, as is C(I,J():=C(I,K)+A(I,J)xB(J,K). In general an assignment is a pair of terms (respectively the left-hand and right-hand sides or the assignment) of our logical language. (A term is an expression constructed solely from function symbols.) We shall take zeroary functioh symbols to be ordinary variables. Then when the left-hand term is simply a zeroary function symbol the assignment is simple variable assignment; for other left­ hand sides we have array assignments. Formally, the simple variable assignment X:=t, where t is an arbitrary term, is {(,,aliXa=t, and otherwise 9=a}. (Xg denotes the value of X in 8, t' the value of t in ,,) Array assignments are slightly harder to define; see [211

• (ii) Tests. Conditionals are usually introduced with "if-then­ else." However reasoning is more smoothly conducted with a "smaller" notion of conditional, the test, which we shall use in conjunction with the next two constructs to synthesize if­ then-else. X>O? is an instance of a test, as is J=OvPattern(J)=Text(K)?. In general a test P? is constructed from a formula P of the logical language. The idea of a test is that a computation may proceed past a test just when that test ev~luates to true in the current environment, otherwise the computation must block (which for our purposes is equivalent to going into an infinite loop). formally, the test P? is the restriction of the identity binary relation on the universe to those states satisfying P, i.e. {(,,,)191=P}. Most of what we say holds even for tests containing modalities, corresponding to the side-effect-free programming construct "if P would be the result of running a then_" However we shall confiM" our examples to the more familiar modality-free variety.
• (iii) Alternation. Execution of altJ entails the execution of either one (but not both) of a and ~. the choice being made nondeterministically. Formally, altJ is the union of a and fj.

(iv) Sequencing. Execution of a:ft entails execution of first a then tJ, Formally, a;fl is the composition of a and tJ.

Using tests, alternation, and sequencing, we may express "if P then a else tJ," where P is a formula and a and tJ are programs, as P?;ai.,P?;fl. In effect, P and .,p act as "guards," to use Dijkstra's [$] terminology. P?;a can only be executed when P holds, and convers.ely for .,p?;tJ. Hence when P is true P?;ai.,P?;fl must be equivalent to a, and otherwise to fj, which is the property "if P then a else fj" should have.

• (v) Iteration. Execution of a* entails iterating a zero or more times, the choice being made nondeterministically. Formally, a* is the reflexive transitive closure of a.

Using tests, sequencing, and iteration, we may express "while P do a" in much the same spirit as if-then-else, namely as (P;a)*;.,P. This permits a to be iterated for as long as P remains true. Moreover, the iteration may not termtnate while P remains true, on account of the .,p guarding the exit. (This usage of a guard at the end is not permitted in [$].)

With these five constructs we can express any flowchart program that has decision boxes and manipulates arrays. This can be done without introducing additional variables. This follows from the fact that state transition diagrams can always be translated into equivalent regular expressions. This is not possible with assignments, sequencing, if-then-else and while­ do [2], the difference having to do with the determinism of the latter. ·

Quasi-programming constructs

In addition to the five constructs for our programming language, we shall find two more constructs of interest, not in writing programs but in talking about them.

• (vi) Random assignment. X:=? is an instance of a random assignment, which nondeterministically assigns an arbitrary element of the domain to X. Consider the sense of [X:=?J(X<OvX~O). This says that no matter what element is assigned to X, after the assignment X will be either negative or non-negative. It should be clear that this has the same sens{' as VX(X<OvX~O). This demonstrates that we can introduce ordinary quantification into dynamic logic as just another modality. This permits simplification of reasoning about quantifiers, by combining certain aspects of it with aspects of reasoning about ordinary assignment.
• (vii) Converse. Execution of a- entails the reverse execution of a. Formally, a- is the converse of a, satisfying 'a! != !a-,, This permits us to reason either forwards or backwards about a program's behavior. Paradoxically, [alP entails backward reasoning while [c:r-JP entails forward reasoning. Generally backward reasoning is easier. We have not capitalized on converse as much as we would like in our work to date.

Truth-value Semantics of Dynamic logic

Now that we have settled on the programming languag{', we can return to the question of what .,[X:=lJfalse means, or more generally what any formula containing [c:rlP means. It is important here to realize the distinction between truth and validity. What we are about to define is the truth value of a formula of dynamic logic in a single state. This is to be contrasted with, say, Hoare's notion of "P{a}Q," whose truth is not defined on a state-by-state basis but rather is defined for the whole universe, and so corresponds to the usual notion in logic of validity.

In state '· [c:rJP is true just when P is true in {'Very state 8 satisfying 9a9. That is, P is true no matter which state a terminates in when started in state 9. It follows that <a>P is true just when pis true in~ state a satisfying 9aa, that is, when it is possible for c:r to terminate and satisfy P if started in state '·

Expressive power of dynamic logic

We may now show how dynamic logic may be used to express a variety of concepts.

Pb}Q

Termination

a:j3

a deterministic

a a I ways ha I ts

a 1-1

a onto

weakest antecedent

strongest consequent I=!P::>IaJQI

I=!P::><a>QI

I=VX!!<a>Y=XI:!<j3>Z=XII

I=VX!<a>Y=X ::> lalY=XI

l=<a>true

~VX!<a->Y=X ::> la-IY=XI

l=<a->true

!alP

<U->P

~eakest invariant strongest invariant convergent

[a*lP

<a-*>P

<aN>P

The reader wishing to pursue these concepts further is referred to [9]. Some simple statements expressible in dynamic logic that do not fall into any of the above categories, and are not expressible in Hoare's partial correctness formalism or the total correctness formalism of Manna and Waldinger U71, art>:

"If you set V to X+S and then add 2 to Van indefinite number of times then it is possible by repeatedly executing V:=Y-1 to make V=X"

"If P holds then after executing tl(~e ~iII be in a state accessible from some state satisfying P."

All of the above concepts can be stated in a second order logic that permits explicit manipulation of statE's and/ or programs as individuals, as in [3] where states can be quantified over, or [10] where programs are terms. The interest in dynamic logic is that it achieves its expressive power using only rirst-order language. The advantage of keeping the language restricted in this way is that it is easier to completely axiomatize parts or the logic, though loops present an insurmountable obstacle to completeness as demonstrated in Theorem 16 of [211

An axiom system for dynamic logic

Let us now exhibit a sound complete effE>ctive axiom system for first-order logic. (By effective we mean one whose axioms r orm a recursive set and whose inference rules are recursive relations on formulae.) The theorems of the following system are exactly the valid formulae of first order logic. A novelty of this system is that it separates into logical and non-logical components what are usually taken to be entirely logical rules and axioms, on the principle that facts about X:=? are program-specific facts.

Logical Axioms

AI I tautologies of Propositional Calculus.

[a] !P::>Ol :::> ([a] P :::> [a] Ql !Axiom Ml Logical Inference Rules P, P::>O r Q !Modus Ponensl P r [alP (subsumes generalization, P r VxP l. Non-logical Axioms VXP :::> P~ (any term T; P~ is P ~ith T for Xl P :::> VXP unless X occurs free in P

The second logical axiom (M) above can be thought or as a claim about programs; it says that for all states g, if P implies Q in every state a that can be reached rrom g by executing Cl, and if p holds in every state a similarly accessible from g via a, then Q holds in every state a accessible from g via <1. And indeed this evident, for in every state a accessible from g via

[V:=X+S;V:=V+2*1

<Y:=V-l*>Y=X

Q we have both P=>Q and P, whence we have Q in every such state.

The second inference rule (really the rule of necessitation of modal logic) can be considered as an upper bound on thE' power of programs, which cannot falsify theorems. If P is a theorem then P is true in every state, whence in particular it must be true after executing <1. In our system it is straightforward to prove as theorems the axioms or, say, Mendelson's system K [18] (p. 51), and it should be clear that the second rule subsumes the rule of generalization; in fact, if the only modalities allowed are those with values of the form X:=? then the rule or necessitation is the rule or generalization, and the theorems or this syst~ coincide with the theorems of K. It is interesting to note that Mendelson manages to express as one axiom what we take two to exprE>ss, namely our Axiom M and the second quantirication axiom. The advantage or our decomposition or this axiom is that we get two axioms abo.ut quantifiers that serve respectively as a lower and an upper bound on what the binary relation X:=? may be.

So far we have only given axioms for random assignments. Now let us ax.iomatize the four loop-free programming constructs.

[P?JQ : P::>O

[X:=tlP = P~ (see £211 for array assignment)

[ai~JP ;; [a]PA[~JP

[a;~JP = [a] [~JP

Interestingly (but fairly obviously, as demonstratt>d in [211), the axiom system with these four new axioms remains sound, complete and effective. (It is possible to give furtht>r axioms to handle the converse op.eration, still preserving soundness, completeness and effectiveness. However we shall not make use of this in the following.)

A derived rule

We could at this point proceed with the discussion of our ultimate objective, the construction of a proof -checking program that would check proofs expressed in the above axiom system. Unfortunately the above system is too weak to permit reasonably succinct proofs; for example, it appears that 6 lines are needed to prove <X:=1>X=1 from the assumption 1=1 using the above system. In this section we explore a derived rult> with an eye on strengthening the axioms and rules. In this respect we are emulating J.A. Robinson [221, who prescribed a new rule to facilitate the construction of automatic theorem­ provers. The constraints on a proof-checker are somewhat different from those of a theorem-prover, and the argumt>nts for Robinson's resolution rule are not sufficiently comp(>lling r or us. In particular, the convenience of having a clause as the unit of information, which helps an automatic theorem prover organize the proof, may be more hindrance than h(>lp in a proof-checker because the user may not have conceived his proof in terms or clauses that are disjunctions or literals. This is not to say that we shall not make use or unification; ind(>ed, unification is a most valuable tool in automated logic.

We now give the details of the rule, which we call the Show Rule for lack of a more descriptive term. A proof step using it looks like Sho~ S {ps} using TO {pQ}, Tl {pl}, T2 {p2}, For the moment ignore the items inside braces { }. ldPally, we would like this rule to apply whenever the formulae TO, Tl, T2, - logically entail the formula S, a semantic characterization of the rule. Unfortunately that would lead to a non-eHective proof-checker, since logical entailme.nt is not even partially decidable for our language [9]. Instead we resort to an effective syntactic characterization. This is where the it('ms in braces enter the picture. The braces enclose "templates" which contain the propositional content of th(' proof stPp, in the sense that each template is a propositional "approximation" to the formula it follows. For example, we might say Sho~ IX: =11 X: =21 X>O {p"q} using "1 >0 {p}, 2>0 {q}.

The template pAq refers to the result of expanding [X:=liX:=2lX>O first to [X:=llX>OA[X:=2lX>O and then to l>0/\2)0. It should be clear that the two uses of p in the templates refer to the same formula, 1>0, and similarly for the two uses of q. More generally, we shall require only that multiple occurrences of the same letter refer to unifiable formulae.

We check this proof step in two phases, which can be don(' independently and in either order (or in parallel by two processors). One phase, called IDENTifY, is to check that repetitions of the same letter can be justified. We do this by attempting to unify corresponding formulae. The other phase, called VERIFY, is to see whether the templates alone constitute a sound argument in modal propositional logic. In this example all modalities were eliminated so that we were left with the argument

Sho~ p"q using p, q

which is in fact a sound argument of non-modal propositional logic. A situation where modal logic would help is:

Sho~ [U; VJ Y>O {[ex] [IJJ p} using [UlX=l {[ex]q}, X=l~[VJY>O {q~[IJJp}.

Here we are dealing with "uninterpreted" programs U and V, a situation that arises when we are given a program about which we have previously proved some useful properties and whose code we no longer wish to be bothered with. (This situation arises frequently in the extended example of the next S('ction but one.) In this case, knowing nothing about the programs U and V beyond the facts given, we could not expand them in the way we did with [X:=lJ, so they carry over to the templates. Here the argument of modal logic is:

Sho~. [ex] (IJJ p using [ex] q, q~ [IJJ p.

This argument can readily be seen to follow if we apply Necessitat.ion to q::~[~]p to get [a](q::~[tJ]p) and hence [a]q::>[a][tJ]p. The rest is propositional reasoning.

The IDENTIFY phase begins by determining what subformula each occurrence of a template letter refers to. This is done by systematically expanding the formula associated with the template containing the given letter until thE' for mula can be matched to the template. Thus W;Vl[WJX=O will match. [a][tJ]p directly with a matched to U;V, b to W and p to X=O. However W;VlX=O will not match [a][tJ]p directly but must first be expanded as [U][VJX=O. [VIWJX=O will not match pAq directly but must first be expanded as [VJX=OA[WJX=O. Once the formula matches the template, the subformula corresponding to each letter can immediately be determined. Then all the subformulae corresponding to occurrencE's of the same letter are checked for whether they can be unified. This ma.y require further expansion; for example, attempting to un1fy [X:=llX>O and W>O involves eliminating the assignment m~dality to give 1>0, and instantiating W as 1, this latter stPp bemg performed by a unification algorithm. All instantiations necessary must be compatible with each other.

Any formulae that fail to unify are put to one side while the remainder of the proof step is checked. When that is done, then the failed pairs are expressed as an equivalence and tested by a routine that checks for validity of quantifier-free Presburger arithmetic, in the hope that the formulae turn out to be equivalent on arithmetic grounds. (This together with the Rule of Convergence described in the next section is the only concession to domain-dependencies in the system.)

The VERIFY phase is a satisfiability tester for modal propositional logic. It begins by determining what applications of the Rule of Necessitation are sufficient to make the proof go through. Boxes are then eliminated from the formula by the appropriate generalization of the transformation <a>PA[alQ -> <a>(P/\Q), which preserves satisfiability for th(' intuitively obvious reason that [a]Q acts only as a constraint on those worlds one might construct (in attempting to satisfy <a>P) that are accessible via a and satisfy P, namely that in any such world Q must be true. In our present implementation, we first eliminate all top-level propositional letters by ('Xpressing the formula in conjunctive normal form and applying the Davis­ Putnam algorithm for each of those letters. Then w~ convert the resulting formula involving only modalities to disjunctive normal form and apply the above transformation. Then the process is repeated on the arguments of the top-level diamond modalities. Though this approach can be inefficient, in practice on the kinds of formulae we encounter it is the most eHici('nt of the methods we have tried. With all boxes eliminat('d th(' satisfiability of the result no longer depends on the nam;s of the diamonds; that is, <a>Pv<tJ>Q and <a>Pv<cr>Q are equally satisfiable. Indeed, satisfiability of the whole is preserved if <a>P is replaced by true when P is satisfiable and false when not. Thus we can proceed recursively, working up from the lowest diamonds to determine satisfiability of progessively larger portions of the formulae.

Axioms for programs with loops

If straight-line programs were all that could be proved correct in our system, it would find relatively little application. for proarams with loops we have the following axioms and rules.

<exn>P ~ <ex*>P AxioMs of Intent {one for each n).

P~[o)P ~ P~[o*)P Rule of Jnvariance. n>z A P A Q(nl ~ <O>J~(zS~<n A Q(~ll ~ n~z A Q(n) ~ <O*>(,pAJ~(zS~SnAO(nll v Q{z)l Rule of Convergence

These axioms and rules are explained and justified in more detail in [21]. The first says that if a can halt in some numbE>r of steps then a* can halt. The second says that if a leaves P unchanged, then so does a*. (Observe how convenient it is to reason about iteration expressed in this form.) The third says that if a "drives" towards z. without passing it, providE>d P remains true, then eventually a* will either make P false somewhere on the way to z., or it will reach z..

Example proof

The following program was devised by Manna and Pnueli [16] to illustrate the erricacy of their method of proving termination.

y :· 0; ~hi le X /. 0 do (~hi leX /. 0 do !X := X-1; Y := Y+11: Y :,. Y-1; ~hile Y /. 0 do !Y := Y-1: X:= X+111

This program represents an obscure way of setting both X and Y to 0, namely by first setting Y to 0, then copying X into Y by repeatedly decrementing X and incremE>nting Y, th!'n decrementing Y once, then copying Y back into X by repE>atedly decrementing Y and incrementing X. This process is repE>ated until X becomes 0. The point of this example was that it was supposed to be diHicult to prove termination of this program by floyd's method but easy by the method described by Manna and Pnueli. Our own interest in this program besides the question of ease of proving termination (not a problem in dynamic logic) is that it is just the right size to illustrate the proof techniques appropriate to dynamic logic.

We may write this program in the programming language dynamic logic caters for thus.

P1: X>O?; X:=X-1; Y:=Y+1. P2: Y>O?; Y:=Y-1; X:=X+1. P3: X>O?; P1*: X=O?; Y:=Y-1; P2*: Y=O?.

P4: Y:=O; P3*; X:O?.

Pl represents one step of "copying" a number from X to Y, while P2 represents one step of copying from Y to X. Pl*;X=O? and P2*;Y=O? each represent the entire copying process, from X to Y and back again. P3 amounts to a program that, provided Y is initially 0, decrements X. P4 is then the whole program for setting X and Y to 0. The statement we want to prove is, <P4>t (t denotes true), which asserts that it is possible for P4 to halt. The following is the proof, which uses 7 hypotheses from arithmetic and 13 theorems. This proof is machine­ readable.

l The Manna-Pnueli program l P1: X>O?; X:=X-1; Y:=Y+1. P2: Y>O?; Y:=Y-1; X:=X+1.

P3: X>O?; P1*; X=O?; Y:=Y-1; P2*: V:O?.

P4: Y:=O; P3*; X=O?. l Formulae occurring commonly in the proofl. AM(n): X=nAY=O. BM!m,nl: X=nAX+Y=m. Ay!nl: Y=nAX=O. By!m,nl: Y=MX+Y=m. l Assumptions from arithmetic- not proved here l H1: Z=n+1 : Z-1=n. H2: W=n+1 ~ W>O. H3: AM!nl = BM!n,nl. H4: Ay!nl = By!n,nl. HS: AM!nl : By!n,OI. H6: Ay!nl = BM!n,OI. H7: W=W. Thm1: BM!m,n+11 ~ <P1>BM!m,nl. Sho~ Thml {pAr ~ <e?>!pArl} using H2 {p~s}. Thm2: By!m,n+ll ~ <P2>By!m,nl. Sho~ Thm2 {pAr ~ <s?>!pAr)} using H2 {p~s}. Thm3: BM!m,nl ~ <P1*>8M(m,OI. Use Convergence{n) Thm3 from Thm1. Thm4: By!m,nl ~ <P2*>By!m,OI. Use Convergence(n) Thm4 from Thm2. ThmS: AM!nl ~ <P1*>Ay!nl. Sho~ ThmS {p~<a>q} using Thm3 {p~<a>q}, ThmS: AM!n+1l ~ <P1*>Ay(n+1l. Sho~ ThmS {p} using Thm3 (p}. Thm7: Ay!nl ~ <P2*>AM!nl. Sho~ Thm7 {r~<a>s} using Thm4 (p~<a>q}, H4 (r:p}, HS (s:q}, Thm8: Ay!n+ll ~ <Y:=Y-l>Ay!nl. Sho~ Thm8 {pAr ~ qAr} using H1 (p:q}. Thm9: AM!n+ll ~ <P3>AM(nl. Sho~ Thm9 {Mn1Ay0 ~ <Mp?;a;MO?;dy;b;y0?>(MnAy01} using H2 (Mn1~Mp}, Thm6 {Mn1Ay0 ~ <a>!yn1AM01}, Thm7 (ynAMO ~ <b>(MnAy01}, Thm8 {ynlAMO ~ <dy>(ynAM01}. ThmlO: AM!nl ~ <P3*>AM!Ol. Use Performance(nl Thm10 from Thm9. Thm11: X=n~<Y:=O>(X,.nAY·Ol. Sho~ Thmll (p~pAq} using H7 {q}. Thml2: Xcn~<P4>t. Sho~ Thm12 (p~<a;c;r?>t} using ThmlO (pAq~<c>(rAq)}, Thm11 {p~<a>!pAq)}. Thm13: <P4>t. Sho~ Thml3 (p} using Thml2 {q~p}, H7 {q},

To avoid being distracted by extraneous issues such as arithmetic truth we have introduced all arithmetic facts in this proof as assumptions. (In fact, in the implemented system we have a very fast proof-checker for quantifier-free Presburger The above proof is not the largest proof we have successrully checked with our system. A substantial part of a total correctness proof of the Knuth-Morris-Pratt pattern­ matching algorithm has been machine-checked, and we are in the process of completing this proor. This extends work on the partial correctness of this algorithm by Wegbreit [241

Discussion of the proof -checker

We have constructed a system for checking proofs of the kind exemplified above. In this we are following in the footsteps of Milner [20,21,261, who is doing for Scott's Logic of Computable functions what we are doing for the above modal extension to first-order logic. Inasmuch as we are treating programs that manipulate their environments, we are also continuing a tradition of several years of implemE'nting systems for proving and checking proors of propertiE's of programs [4,8,13,14,23,241. However the greater expressive power of dynamic logic compared to that of partial correctness assertions (the language used in almost all such systems) adds considerably to the interest of our system. This consideration actually makes Milner's system a closer relative of ours than the partial correctness systems, due to the greater emphasis on "expressions as first class citizens" in MilnE>r's systE'm and ours, resulting in a logic where programs and facts mingle morE' freely than say with Hoare's notation. The major differ<>nce between Milner's system and ours is the LCf treatment of programs (computable functions) as individuals in the underlying domain versus our treatment of programs as "adverbs," analogously to quantifiers. Another system related to ours is Richard Weyhrauch's [1,251 fOL (first-Order Logic) proof­ checker. A detail in which our program differs from Milner's and Weyhrauch's (apart from the obvious one of choice of logical language) is that our program makes less of an effort to help the user interactively than is done by either LCf or fOL, but rather is, at least thus far, a system in which the ust>r prepares his proof exactly as though he were writing a program. This means that his proof exists on a file and is read by the proof -checker just as an interpreter reads a program from a file. This has permitted us to r ocus all of our effort on the proof-checker proper.

The proof-checker is implemented on the POP-10 computer at M.I.T.'s Artificial Intelligence Laboratory. The program written to date has aproximately 100 LISP functions comprising a total of 1800 lines of code averaging 4 LISP atoms per liM. The bulk of this code is for formula manipulation. However, a small amount of it is for book-keeping tasks of a relatively minor nature associated with keeping track of the structure of a proor.

Direction·s for further research

Although our immediate goals may not appear to be particularly ambitious or difficult to achieve, as well as not being obviously "Artificial Intelligence" research, we. admit to far more ambitious and less plausible objectives on a larger time scale. Ultimately we see the proof -checker itself becoming a component of a variety of very intelligent program­ manipulating programs. This depends on our belief that the ability to check proofs is a vital part of any program that pretends to "understand" some domain of discourse where the discussion is at all involved. Two applications that we would like to explore when the proof -checker has reachE'd a satisfactory level of performance are (i) the automatic production of reliable software and (ii) machine-mediatE'd reasoning about programs. Our plan of attack for each of these areas is not presently so crisp that we would feel confid<>nt embarking on either area forthwith, particularly the second, but we can nevertheless at this early stage present thoughts on these subjects.

The notion of program reliability through correctnE'ss proofs has gained momentum in the past few years, spurred on most notably by the axiomatic methods of Floyd [71 and HoarE' Ull. As yet there is not a shred of hard evidence to suggest that this approach supplies the most economical approach to reliability (where the economics takes into account both thE' cost of having unreliable software and the total programming and maintenance cost). Indeed, it may well turn out that thE' bulk of the problems encountered today with unreliablE' software may be disposed of by a happy combination of a good programming language and a clean programming style. Nevertheless, if the proof-oriented approach can be made to work and does not put too great a burden on the programmer and/ or the computer, it may provide reliable software at low cost. We feel it is well worth continuing the experiments that have been going on in this area in the past few years. Although these experiments have not thus far demonstrated the value of correctness proofs, it is still too early to draw any negative conclusions about the method in general.

from a longer-range viewpoint, the burden of programming should become progressively more the computer's responsibility, requiring the computer to "understand" bettE'r the programs it executes. This has been the trend since the first assembler was used, and though the trend is perhaps not as pronounced as some have hoped, there is no doubt that the trend continues. As it does, methods of reasoning about programs will concomitantly become a more E'ssential part of the computer's repertoire. This raises the question of thE' choice of language most appropriate to such reasoning. In view of the expressive power of dynamic logic we feel that it is worth developing the methodology of reasoning in this language with an eye to automating the reasoning as far as possible. A program like our proof-checker is precisely what is neE'ded in the way of a "black box" that "accepts" a reasonably sized step in a discussion about a program. The sort of machine-mediatE'd discussions we envisage could quite well be cast as proofs, albeit in the form of a dialogue. If the notion of a dialogue as a proof seems strange, visualize a conversation - about a program - punctuated with "I don't see why you need that test thE're" and "How do you guarantee that X will never become negative?" Such conversations about programs arise all the time, and it is clear that the questions are ref erring to proofs, probably expressed informally but proofs nonetheless. One might argue that proof-checking is not understanding, but we would insist that it is at least a component of understanding.

As humans are taken progressively further out of the loop (admittedly a very long-ranee view) the dialogue will become more of a monologue. However it may still be appropriate for

,

the computer to reason about tht' programs it is contemplating using a language like dynamic logic. Thus even in this scenario the basic proof-checking methodology may continue to be used. We should add that we see nothing strange in the idea of a computer checking proofs that it generated itself; the best way to generate proofs may be to propose possibly faulty proofs and subject them to detailed criticism. This would require not only the error-detecting capability of our proposed proof -checker but error-correcting capabilities as well.

Acknowledgments

David Hare( and Albert Meyer made substantial contributions to the theoretical underpinnings of dynamic logic. We thank Richard Weyhrauch and Derek Opperi for many helpful ARPA-net-mediated conversations on proof-checking and theorem-proving.