|
|
|---|
|
|
|
|---|
Modeling State Machines
“The meaning of a program is defined by its effect on the state vector” — John McCarthy, Towards a Mathematical Science of Computation (1962).
Users of ACL2 (see bib::kmm00a and bib::kmm00b) and its predecessor, Nqthm (see bib::bm97), have long modeled state machines and verified interesting properties of programs running on those machines. The basic idea is to represent the state of the machine (including its programs) by an ACL2 object and then define an interpreter that computes a “final” state from an initial state. In this documentation topic we fill out that sketch of the methodology without being specific about any particular machine. We then dive into details in subsidiary topics.
If you have ideas for additions or other improvements to the documentation of the ACL2 approach to operational semantics, please add suitable documentation or simply send your comments to the ACL2 developers. Note that we have intentionally limited our literature survey to models and proof methods in ACL2 and Nqthm. Widening the focus to operational semantics in general is simply beyond the scope of this documentation topic. But if you see omissions or errors in our discussion of ACL2 or Nqthm models and proof methods, please either fix them or bring them to our attention, making your suggestions as detailed as possible, e.g., what documentation topic are you looking at and precisely how would you change it? If your change involves citing a paper or Nqthm or ACL2 file that we have left out, please include the appropriate bibliographic information as well as a URL to the paper or file if possible. The following documentation topics are of concern:
You won't be able to prove theorems about ACL2 functions interpreting another language unless you can prove theorems about ACL2 functions. An excellent way to test yourself is to think of a program you'd like to verify in that other programming language. Code a function in ACL2 that computes the same answer using the same algorithm, as nearly as possible in an applicative setting. So for example, if your program destructively modifies an array in that other programming language, perhaps model the array in ACL2 as a list but access elements with nth and “modify” elements with update-nth. Then prove that the ACL2 function is correct with ACL2. If you can do that, you're ready to try to embed that other language (or some fragment of it) in ACL2 and reason about such programs with ACL2.
In the approach ACL2 users most often take to model state machines the first step is to represent the relevant parts of the machine's state as an ACL2 object. Then the user defines a single-step (or “small step”) function to compute the next state from the current one (and possibly some inputs). Finally, the user defines a recursive function that iterates the single-step transition from a given initial state a given number of times or until some halting condition is detected in the state. That function is often called the “run” function and is our operational semantic model. See operational-semantics-1__simple-example for a model of an extremely simple machine, the way we configure ACL2 to prove things about it, some example proofs and other uses of the model.
The argument that controls the maximum number of steps taken is often called a “clock” but it has nothing to do with the passage of time. In some models the clock is just a natural number. In others it may be a finite list of inputs to be successively transferred into the state on each cycle. In any case, the clock guarantees that the run function terminates, which is a prerequisite for functions defined recursively in ACL2. But do not be fooled into thinking that all programs running on the machine always terminate. By appropriate use of quantification one can often prove that a given program never terminates or only terminates under certain pre-conditions. This is discussed further in operational-semantics-1__simple-example.
Such a model can be used as a prototype for the machine: the model can be
executed on concrete states for testing purposes. But because ACL2 is a
formal system, it is also possible to do symbolic simulation of the model and
to prove theorems involving the model. Such theorems might be loosely
classified as being “about” a particular program running on the
machine or “about” the machine itself. An example of the first
might be that a certain program for the machine computes the factorial
function. An example of the second might be that when the machine is run
To facilitate such proofs it is common to develop a book of rewrite (and other kinds of) rules that do such things as normalize compositions of functions used in the construction of states and clock expressions. The basic idea is to control the expansions of the step and run functions to contain case explosions that would otherwise occur. E.g., we usually configure the ACL2 database so that
Such a configuration of ACL2 generally makes it possible to prove certain styles of theorems by following a well-understood methodology.
For example, to express a conjecture about the final state produced by a
program on the machine, one might write an implication whose hypothesis
characterizes an acceptable initial state and whose conclusion is an equality
whose left-hand side is a call of run on that state and a clock expression
that measures exactly how many steps it will take to reach the halt state or
return, and whose right-hand side is the symbolic expression of the correct
final state. The two states just mentioned and the clock expression are
usually terms involving variables denoting values found in relevant locations
in the initial state. A very strong total correctness theorem for a
factorial program might be something like “if a natural number,
The clock term,
Proofs of such theorems are most often done by induction, appealing to similar lemmas about the effects of loops and subroutine calls. But proofs using inductive assertions and other mathematical techniques can be used.
The methodology described above generally limits the human to creative contributions (like identifying invariants being maintained) and relegates to ACL2 the tedious unwinding of possibly long chains of symbolic computation. The previously mentioned documentation topic, operational-semantics-1__simple-example, carries out this entire program for a simple machine, explicates the methodology, and uses it to prove a variety of theorems.
Following this approach, users of Nqthm and ACL2 have modeled and verified properties of many interesting machines. More precise references to the work mentioned below as well as models and proofs about other machines — and other kinds of properties, like absence of deadlock — may be found in operational-semantics-2__other-examples.
After you are familiar with how to use ACL2 and have studied some of the models described here, you are ready to try to develop your own models. We offer three pieces of advice.
Our discussion of the details of operational semantics in ACL2 is structured as follows.