A Practical Formal Semantic Definition and Verification System for Typed LISP.

摘要

Despite the fact that computer scientists have developed a variety of formal methods for proving computer programs correct, the formal verification of a non-trivial program is still a formidable task. Moreover, the notion of proof is so imprecise in most existing verification systems, that the validity of the proofs generated is open to question. With an aim toward rectifying these problems, the research discussed in this dissertation attempts to accomplish the following objectives: 1. To develop a programming language which is sufficiently powerful to express many interesting algorithms clearly and succintly, yet simple enough to have a tractable formal semantic definition. 2. To completely specify both proof theoretic and model theoretic formal semantics for this language using the simplest possible abstractions. 3. To develop an interactive program verification system for the language which automatically performs as many of the straightforward steps in a verification as possible.