Functions for Manipulating these Objects
Consider a typical ``stack'' of control frames.
Suppose the model required that we express the idea of ``the most recent
frame whose return program counter points into
The natural expression of this notion involves
function application — ``fetch the
case analysis — ``if the pc is
iteration or recursion — ``pop this frame off and repeat.''
The designers of ACL2 have taken the position that a programming language is the natural language in which to define such notions, provided the language has a mathematical foundation so that models can be analyzed and properties derived logically.
Common Lisp is the language supported by ACL2. To be precise, a small applicative subset of Common Lisp is the language supported by ACL2.