Pure-expression-execution
Execution of pure expressions for ATC.
We introduce functions to execute
pure expressions and lists of pure expressions.
These do not depend on function environments,
because pure expressions do not have any function calls,
and do not depend on limits,
because pure expressions always terminate execution.
We prove properties that relate these specialized execution functions
to the general execution functions for expressions and lists thereof.
This is a more general concept than ATC,
but it is currently only used for ATC;
this is why it is under ATC.
The functions exec-expr-pure and exec-expr-pure-list
were part of an earlier version of our dynamic semantics of C,
and that is part of why ATC is based on that.
Since then, we have evolved our dynamic semantics of C,
but ATC is still based on these functions to execute pure expressions.
In the future, we may evolve ATC to use directly
exec-expr and exec-expr-list,
and eliminate these concepts about pure expression execution.
Subtopics
- Exec-expr-pure
- Execute a pure expression.
- Expr-pure-limit
- Limit to pass to exec-expr
for the execution of the given pure expression to terminate.
- Exec-expr-pure-list
- Execute a list of pure expression.
- Expr-list-pure-limit
- Limit to pass to exec-expr-list
for the execution of the given list of pure expressions to terminate.
- Exec-expr-list-to-exec-expr-pure-list-when-expr-pure-list-limit
- Reduction of exec-expr-list to exec-expr-pure-list
under a hypothesis about the limit.
- Induct-exec-expr-of-pure
- Induction scheme for exec-expr applied to a pure expression.
- Exec-expr-to-exec-expr-pure-when-expr-pure-limit
- Reduction of exec-expr to exec-expr-pure,
under a hypothesis about the limit.
- Exec-expr-list-to-exec-expr-pure-list-when-not-errorp
- Reduction of exec-expr-list to exec-expr-pure-list,
under a hypothesis about the absence of errors.
- Exec-expr-to-exec-expr-pure-when-not-errorp
- Reduction of exec-expr to exec-expr-pure,
under a hypothesis about the absence of errors.
- Induct-exec-expr-list-of-pure
- Induction scheme for exec-expr-list
applied to a list of pure expressions.
