By adopting an ``interpretive'' style, one can execute the model in the functional language to ``run'' programs in the von Neumann language. Given the ability to reason about the functional language, one can use the model to reason about programs in the von Neumann language. By mechanizing the formal logic, we mitigate the problems Plotkin describes with the interpretive style.
Such a formal semantics has a dual use which industrial users of formal methods find very appealing: as a simulation engine and as an axiomatic basis for code proofs.
The beauty of this approach is that the user need build no more logical machinery than needed to simulate the language in question. The proof facility is inherited from the underlying system.
In these lectures we will illustrate the techniques by formalizing a simple programming language called ``M1,'' for ``Machine (or Model) 1.'' It is loosely based on the Java Virtual Machine but has been simplified for pedagogical purposes. We will demonstrate the executability of M1 models. We will develop several styles of code proofs, including direct (symbolic simulation) proofs based on Boyer-Moore ``clock functions'' and Floyd-Hoare inductive assertion proofs. We construct proofs only for the the simplest of programs, namely an iterative factorial example. But to illustrate a more realistic use of the model, we discuss the correctness proof for an M1 implementation of the Boyer-Moore fast string searching algorithm.
We also define a compiler for a higher level language called ``J1'' and show how to do proofs about J1 code without benefit of a formal semantics for that code. Throughout we use the ACL2 logic and theorem proving system.