|
|
|---|
|
|
|
|---|
Fixtype of evaluation states.
This is a tagged union type, introduced by fty::deftagsum.
In our current formalization,
the execution of an ACL2 program starts with
a call of a (named) function on some argument values.
For every choice of function and arguments,
there is one possible initial state.
This is captured by the
As formalized elsewhere, the execution from an initial state
proceeds by looking up the function's definition,
binding the argument values to the function's parameters,
and then executing the function's body,
which is put in a frame together with the binding.
As also formalized elsewhere, a frame is executed stepwise,
and may result in new frames being pushed onto the stack.
Thus, a transitional execution state,
i.e. one that is neither initial nor final,
consists of a stack of frames.
This is captured by the
Frames are pushed and popped during execution.
When the last frame is popped,
there is no longer a stack,
but there is a value,
which is the result of the original function call (in the initial state)
that started the whole execution.
The final state thus consists of a single value.
This is captured by the
During execution, certain kinds of errors may occur.
For example, a function definition may not be found.
There are well-formedness conditions on programs
that ensure, via invariants on evaluation states,
the absence of such errors.
This will be formalized as
the static semantics of the ACL2 programming language.
However, as is common in programing language research,
we define the dynamic semantics of the ACL2 programing language
without assumng any static well-formedness,
and therefore we must allow for the occurrence of errors,
which lead to error states.
This is captured by the