Marktoberdorf Summer School, 2008

August 5-16, 2008

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.

Mechanized Operational Semantics Lecture 1 Lecture 2 Lecture 3 Lecture 4 Lecture 5 ACL2 Support Books - scripts/certify-all.lisp -- script for recertifying all books
- scripts/compile.lisp -- the J1 compiler
- scripts/fast.lisp -- Boyer-Moore fast string searching algorithm proof (done in collaboration with Matt Martinez)
- scripts/g-direct.lisp -- direct proof of iterative factorial
- scripts/g-invariant.lisp -- inductive assertion proof of iterative factorial
- scripts/m1-fast.lisp -- direct proof of M1 implementation of Boyer-Moore fast string searching algorithm
- scripts/m1.lisp -- operational semantics for M1
- scripts/perm.lisp -- permutation
- scripts/preliminary-material.lisp -- all the definitions and theorems mentioned in the preliminary material
- scripts/utilities.lisp -- lemmas for string matching proof (by Matt Martinez)