|
|
|---|
|
|
|
|---|
Semantics of Imp.
Since Imp is so simple, there is no need to explicitly define a static semantics, i.e. constraints for the well-formedness and type correctness of Imp programs. The separation between the aexp and bexp fixtypes provides an implicit typing of all the Imp expressions. Therefore, in the context of Imp, `semantics' always refer to dynamic (i.e. execution) semantics.
We formalize the variable store as an environment, i.e. a finite map from (names of) variables to (integer values). Imp commands operate on the environment.
We formalize the computation state as a configuration, i.e. a pair consisting of a sequence of zero or more commands and an environment. The commands are the next ones to be executed, in order.
We formalize expression evaluation via ACL2 functions from expressions and environments to values. This is possible because the evaluation of Imp expressions always terminates. We use this modeling approach because it is simple and we are currently not interested in intermediate computation states during the evaluation of expressions, but just in the final result of expression evaluation. If we were interested in those intermediate computation states, we would have to formalize expression evaluation as a multi-step process, similarly to the execution of commands (as explained just below).
We formalize an operational semantics via an ACL2 function that maps old configurations to new configurations. This function performs one step of computation, according to a reasonable level of granularity, but it is possible to define finer- or coarser-grained steps; for instance, if expression evaluation were a multi-step process as mentioned above, then we would have a finer-grained execution model. We cannot have an always-terminating interpreter of Imp commands, because its loops may not terminate. Thus, having the step function, each of whose steps always terminates, lets us talk about sequences of steps that may or may not terminate. The step function captures a small-step operational semantics; its sequentialization captures a big-step operational semantics.