Execution
Execution of expressions, statements, etc.
We formalize a big-step interpretive operational semantics,
via mutually recursive ACL2 functions
over the abstract syntax of expressions and statements.
The `big-step' attribute means that the ACL2 functions
return the ``final'' result of executing the expression or statement.
The `interpretive' attribute means that the ACL2 functions
are executable as an interpreter of Leo;
note that this interpreter is written for clarity and simplicity,
not for efficiency.
In the absence of static semantic restrictions,
executing Leo code may not terminate,
due to recursive function calls.
Since we want to define a defensive dynamic semantics
that does not assume any static semantics restrictions,
we must therefore include limit counters in the ACL2 functions,
which must always terminate for logical consistency.
Each mutually recursive ACL2 function takes a limit counter,
terminates if the counter reaches 0,
and otherwise it passes a counter decremented by one
to each recursive call;
thus, the counter measures the depth of the recursion
of the ACL2 functions (not of the Leo functions).
An alternative to ensure function termination in ACL2
could be to maintain a sequence of called functions
and stop with an error when a recursive function call happens,
which should therefore let us take into account
the sequence of called functions when formulating the measure
to prove the termination of the ACL2 functions.
However, the limit counters are simpler, and commonly used.
Furthermore, they will still work if Leo is extended with
richer loops that are not amenable to simple termination checks
(although the loops will have to be bounded)
or with recursion
(which will have to be bounded).
At some point we may also formalize a small-step operational semantics,
and formally prove it equivalent to the big step one.
In a small-step operational semantics,
we must formalize more of the Leo computation state,
including a notion of how much of an expression or statement
has been executed vs. must be still executed,
and describe ``small'' changes to the computation state.
These steps, chained together, are equivalent to the big steps.
The small-step approach may provide more flexibility
in formulating and proving properties of interest,
but it is more complicated, because of the need
to explicate more of the computation state as described above.
This is why we use a big-step approach:
it is easier to formulate,
and may turn out to be sufficient for many, if not all,
our verification purposes.
In the current relatively simple version of Leo,
we could avoid explicating the call stack in the dynamic semantics,
and instead use ACL2 call stack for that purpose.
However, explicating the call stack provides more flexibility,
in particular for future versions of Leo
that may include references (via self)
to locations in preceding frames in the call stack.
Subtopics
- Exec-expressions/statements
- Execute expressions and statements.
- Init-for-loop
- Initialize the execution of a for loop.
- Exec-file-main
- Execute the main function of a file.
- Update-variable-value-in-scope-list
- Update the value in a variable in a list of scopes.
- Step-for-loop
- Step the loop variable.
- Update-variable-value-in-scope
- Update the value in a variable in a scope.
- Expr-value-to-value
- Turn an expression value into a value.
- Exec-binary
- Execute a binary operator, on two expression values.
- Exec-expression
- Execute an expression.
- Init-vcscope-dinfo-call
- Initialize the dynamic information about
a variable and constant scope,
for a function call.
- Value?+denv
- Fixtype of pairs consisting of
an optional value and a dynamic environment.
- Exec-statement
- Execute a statement.
- End-of-for-loop-p
- Check if a for loop has ended.
- Expr-value
- Fixtype of expression values.
- Evalue+denv
- Fixtype of pairs consisting of
an expression value and a dynamic environment.
- Write-location
- Write a value into a location.
- Read-location
- Read the value stored in a location.
- Exec-for-loop-iterations
- Execute the iterations of a for loop.
- Update-variable-value
- Update the value in a variable in a dynamic environment.
- Exec-unary
- Execute a unary operator, on an expression value.
- Values+denv
- Fixtype of pairs consisting of
a list of values and a dynamic environment.
- Init-vcscope-dinfo-loop
- Initialize the dynamic information
about a variable and constant scope,
for a loop.
- Extend-denv-with-structdecl
- Extend a dynamic environment with a struct declaration.
- Exec-var/const
- Execute a variable or constant expression.
- Valuemap+denv
- Fixtype of pairs consisting of a value map and a dynamic environment.
- Namevalue+denv
- Fixtype of pairs consisting of
a name-value pair and a dynamic environment.
- Extend-denv-with-fundecl
- Extend a dynamic environment with a function declaration.
- Ensure-boolean
- Ensure that an expression value is a boolean.
- Int+denv
- Fixtype of pairs consisting of
an integer and a dynamic environment.
- Push-vcscope-dinfo
- Push information about a variable and constant scope
onto the scope stack of the top call of a dynamic environment.
- Extend-denv-with-topdecl-list
- Extend a dynamic environment with a list of top-level declarations.
- Exec-literal
- Execute a literal expression.
- Build-denv-from-file
- Build a dynamic environment from a file.
- Namevalue+denv-result
- Fixtype of errors and pairs consisting of
a name-value pair and a dynamic environment.
- Extend-denv-with-topdecl
- Extend a dynamic environment with a top-level declaration.
- Evalue+denv-result
- Fixtype of errors and pairs consisting of
an expression value and a dynamic environment.
- Value?+denv-result
- Fixtype of errors and pairs consisting of
an optional value and a dynamic environment.
- Values+denv-result
- Fixtype of errors and pairs consisting of
a list of values and a dynamic environment.
- Valuemap+denv-result
- Fixtype of errors and pairs consisting of
a value map and a dynamic environment.
- Int+denv-result
- Fixtype of errors and pairs consisting of
an integer and a dynamic environment.
- Push-call-dinfo
- Push information about a call
onto the call stack of a dynamic environment.
- Exec-print
- Execute the printing of a message on the screen.
- Pop-vcscope-dinfo
- Pop information about a variable and constant scope
off the scope stack of the top call of a dynamic environment.
- Exec-if
- Execute the constituents of a conditional statement.
- Exec-function
- Execute a function call.
- Pop-call-dinfo
- Pop information about the top call
off the call stack of a dynamic environment.
- Exec-statement-list
- Execute a list of statements.
- Exec-block
- Execute a block.
- Exec-struct-init-list
- Execute a list of struct component initializers.
- Exec-struct-init
- Execute a struct component initializer.
- Exec-expression-list
- Execute a list of expressions.
