Mechanized Operational Semantics

J Strother Moore
Marktoberdorf Summer School, 2008
August 5-16, 2008

Caveat

This website was prepared in advance of the Summer School. I may well change the lectures before presenting them and I will probably deviate from the scripts used in the demonstrations below. But this will at least give a good indication of what I plan to say!

Abstract

In these lectures I explain how to formalize an ``operational'' or ``state-transition'' semantics of a von Neumann programming language in a functional programming language. This approach to operational semantics was pioneered by Boyer and Moore in the late 1970s (see, for example, the ``hand-held calculator'' model in A Computational Logic, Academic Press, 1979) and has been used extensively ever since in the Boyer-Moore community.

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.

Relevant Files