Boyer R.S., Moore J.S. A Computational Logic

Издательство Academic Press, 1979, -441 pp.Mechanical theorem-proving is crucial to the automation of reasoning about computer programs. Today, few computer programs can be mechanically certified to be free of bugs. The principal reason is the lack of mechanical theorem-proving power. In current research on automating program analysis, a common approach to overcoming the lack of mechanical theorem-proving power has been to require that the user direct a proof-checking program. That is, the user is required to construct a formal proof employing only the simplest rules of inference, such as modus ponens, instantiation of variables, or substitution of equals for equals. The proof-checking program guarantees the correctness of the formal proof. We have found proof-checking programs too frustrating to use because they require too much direction.
Another approach to overcoming the lack of mechanical theorem-proving power is to use a weak theorem-proving program and to introduce axioms freely. Often these axioms are called lemmas, but they are usually not proved. While using a proof checker is only frustrating, introducing axioms freely is deplorable. This approach has been abused so far as to be ludicrous: we have seen researchers verify a program by first obtaining formulas that imply the program’s correctness, then running the formulas through a simplifier, and finally assuming the resulting slightly simplified formulas as axioms. Some researchers admit that these lemmas ought to be proved, but never get around to proving them because they lack the mechanical theorem-proving power. Others, however, believe that it is reasonable to assume lots of lemmas and never try to prove them. We are strongly opposed to this latter attitude because it so completely under mines the spirit of proof, and we therefore reply to the arguments we have heard in its defense.
- It is argued that the axioms assumed are obvious facts about the concepts involved. We say that a great number of mistakes in computer programs arise from false obvious observations, and we have already seen researchers present proofs based on false lemmas. Furthermore, the concepts involved in the complicated computer systems one hopes eventually to certify are so insufficiently canonized that one man’s obvious is another man’s difficult and a third man’s false.
- It is argued that one must assume some axioms. We agree, but observe that mathematicians do not contrive their axioms to solve the problem at hand. Yet often the lemmas assumed in program verification are remarkably close to the main idea or trick in the program being checked.
- It is argued that mathematicians use lemmas. We agree. In fact, our theorem-proving system relies heavily on lemmas. But no proof is complete until the lemmas have been proved, too. The assumption of lemmas in program proving often amounts to sweeping under the rug the hard and interesting inferences.
- It is argued that the definition of concepts necessarily involves the addition of axioms. But the axioms that arise from proper definitions, unlike most lemmas, have a very special form that guarantees two important properties. First, adding a definition never renders one’s theory inconsistent. Second, the definition of a concept involved in the proof of a subsidiary result (but not in the statement of one’s main conjecture) can be safely forgotten. It does not matter if the definition was of the wrong concept. But an ordinary axiom (or lemma), once used, always remains a hypothesis of any later inference. If the axiom is wrong, the whole proof may be worthless and the validity of the main conjecture is in doubt.
One reason that researchers have had to assume lemmas so freely is that they have not implemented the principle of mathematical induction in their theorem-proving systems. Since mathematical induction is a fundamental rule of inference for the objects about which computer programmers think (e.g., integers, sequences, trees), it is surprising that anyone would implement a theorem prover for program verification that could not make inductive arguments. Why has the mechanization of mathematical induction received scant attention?
Perhaps it has been neglected because the main research on mechanical theorem-proving, the resolution theorem-proving tradition, does not handle axiom schemes, such as mathematical induction. We suspect, however, that the mechanization of mathematical induction has been neglected because many researchers believe that the only need for induction is in program semantics. Program semantics enables one to obtain from a given program and specification some conjectures (verification conditions) that imply the program is correct. The study of program semantics has produced a plethora of ways to use induction. Because some programs do not terminate, the role of induction in program semantics is fascinating and subtle. Great effort has been invested in mechanizing induction in program semantics. For example, the many verification condition generation programs implicitly rely upon induction to provide the semantics of iteration.
But program semantics is not the only place induction is necessary. The conjectures that verification condition generators produce often require inductive proofs because they concern inductively defined concepts such as the integers, sequences, trees, grammars, formulas, stacks, queues, and lists. If you cannot make an inductive argument about an inductively defined concept, then you are doomed to assume what you want to prove.
This book addresses the use of induction in proving theorems rather than the use of induction in program semantics.
We will present a formal theory providing for inductively constructed objects, recursive definitions, and inductive proofs. Readers familiar with programming languages will see a strong stylistic resemblance between the language of our theory and that fragment of the programming language LISP known as pure LISP. We chose pure LISP as a model for our language because pure LISP was designed as a mathematical language whose formulas could be easily represented within computers. Because of its mathematical nature (e.g., one cannot destructively transform the ordered pair h7,3i into h8,3i), pure LISP is considered a toy programming language. It is an easy jump to the non sequitur: The language and theory presented in this book are irrelevant to real program analysis problems because they deal with a toy programming language. But that statement misses the point. It is indeed true that our theory may be viewed as a programming language. In fact, many programs are naturally written as functions in our theory. But our theory is a mathematical tool for making precise assertions about the properties of discrete objects. As such, it can be used in conjunction with any of the usual program specification methods to state and prove properties of programs written in any programming language whatsoever.A Sketch of the Theory and Two Simple Examples
A Precise Definition of the Theory
The Correctness of a Tautology Checker
An Overview of How We Prove Theorems
Using Type Information to Simplify Formulas
Using Axioms and Lemmas as Rewrite Rules
Using Definitions
Rewriting Terms and Simplifying Clauses
Eliminating Destructors
Using Equalities
Generalization
Eliminating Irrelevance
Induction and the Analysis of Recursive Definitions
Formulating an Induction Scheme for a Conjecture
Illustrations of our Techniques Via Elementary Number Theory
The Correctness of a Simple Optimizing Expression Compiler
The Correctness of a Fast String Searching Algorithm
The Unique Prime Factorization Theorem
Definitions Accepted and Theorems Proved By our System
The Implementation of the Shell Principle
Clauses for our Theory