		Search-engine friendly clone of the ACL2 documentation.

Operational-semantics-3__annotated-bibliography

Bib::bm96

R. S. Boyer and J S. Moore, “Mechanized Formal Reasoning about Programs and Computing Machines”, in R. Veroff, editor, Automated Reasoning and Its Applications: Essays in Honor of Larry Wos, MIT Press, 1966.

Relevance: the basic Nqthm/ACL2 style of operational semantics as a book chapter

———

Abstract

The design of a new processor often requires the invention and use of a new machine-level programming language, especially when the processor is meant to serve some special purpose. It is possible to specify formally the semantics of such a programming language so that one obtains a simulator for the new language from the formal semantics. Furthermore, it is possible to configure some mechanical theorem provers so that they can be used directly to reason about the behavior of programs in the new language, permitting the expeditious formal modeling of the new design as well as experimentation with and mechanically checked proofs about new programs. We here study a very simple machine-level language to illustrate how such modeling, experimentation, and reasoning may be done using the ACL2 automated reasoning system. Of particular importance is how we control the reasoning system so that it can deal with the complexity of the machine being modeled. The methodology we describe has been used on industrial problems and has been shown to scale to the complexity of state-of-the-art processors.

———

This paper describes the basic methodology used to model and reason about machines with ACL2: states as objects, a step function, a run function, clock functions for programs, lemmas to control expansion, and the basic methodology for specifying and verifying programs. The vehicle for this explanation here is a machine almost identical to M1 and this paper covers essentially the same ground as the documentation topic operational-semantics-1__simple-example. Referring to the work described in operational-semantics-5__history-etc and early ACL2 work, the paper says

The approach we describe is essentially that used in the Nqthm and ACL2 projects described above. Furthermore, the Nqthm and ACL2 users above were taught this method of formalization via examples very similar to this one, primarily in our graduate class, Recursion and Induction, at the University of Texas at Austin. That this technique scales up to languages that are many orders of magnitude more complicated than this one is demonstrated by [5, 9]. Therefore, simplicity here should be looked upon as a virtue.

While the paper does not name the machine being formalized, it was in fact called small-machine rather than m1 and it goes all the way back to Nqthm. Indeed, among the students who learned this methodology in Recursion and Induction in the early 1980s were Bevier, Hunt, Young, Flatau, and Wilding — all principals in the CLI Verified Stack work bib::bhmy89. See the 1991 Nqthm script examples/basic/small-machine.events, which demonstrates that most of the methodology described here was developed before ACL2. Coincidentally, it also shows that what we're calling m1 today — informally described as a “toy” Java Virtual Machine — predates the Java and the JVM.

The ACL2 version of the small-machine proof script may be found in the ACL2 book at https://www.cs.utexas.edu/~moore/publications/small-machine.lisp.

By the way, notes for Recursion and Induction have been incorporated into ACL2's documentation. See recursion-and-induction. But when the course was taught by Boyer and Moore in the 1980s the notes were essentially just a list of conjectures to prove or disprove and the class was rather free-form in the sense that student participation was critical and often determined the kinds of problems posed in the latter part of the semester. Operational semantics is not mentioned in the recursion-and-induction documentation.