Variable-resolution-preservation
Preservation of variable resolution under execution.
We prove theorems saying that,
in our dynamic semantics of C,
if a variable with a certain name
is visible in the computation state before an execution function,
then the same variable is also visible
in the computation state after the execution function,
with a slight exception explained shortly.
Here visibility is expressed via objdesign-of-var;
the fact that the same variable is visible
(as opposed to a possibly different one with the same name)
is expressed via the equality of objdesign-of-var
before and after the execution.
Compare this notion with
the one in variable-visibility-preservation.
The exception mentioned above applied to
the execution of
object declarations,
block items,
and lists of block items:
since those may introduce any number of new variables,
which may hides ones with the same names in outer scopes,
objdesign-of-var may not resolve to the same variable,
i.e. to the same object designator.
Here the term `resolution' refers to
the object designator returned by objdesign-of-var.
We prove an inductively stronger property, involving the peeling of frames and scopes, from which the desired theorems follow as corollaries.
Subtopics
- Var-resolve-preservep-of-exec
- Preservation of variable resolution under execution,
for any number of peeled frames and scopes.
- Prev-scope/frame
- Go to the previous scope or frame.
- Var-resolve-of-exec
- Preservation of variable visibility under execution.
- Var-resolve-preservep
- Check if all the variable names visible in a computation state
are also visible in another computation state
and they resolve to the same variables,
for any number of peeled frames and scopes.
- Var-resolve-preservep-of-exit-scope-when-enter-scope
- If variables resolution is preserved between
a computation state just after entering a scope
and another computation state,
then variable resolution is also preserved between
the first computation state before entering the scope
and the second computation state after exiting a scope,
and without going to the previous scope or frame.
- Var-resolve-preservep-of-prev-of-exit-scope-when-enter-scope
- If variables resolution is preserved between
a computation state just after entering a scope
and another computation state,
by going to the previous scope or frame,
then variable resolution is also preserved between
the first computation state before entering the scope
and the second computation state after exiting a scope,
and without going to the previous scope or frame.
- Var-resolve-preservep-of-pop-frame-when-push-frame
- If variables resolution is preserved between
a computation state just after pushing a frame
and another computation state,
by going to the previous scope or frame,
then variable resolution is also preserved between
the first computation state before pushing the frame
and the second computation state after popping a frane,
and without going to the previous scope or frame.
- Var-resolve-preservep-of-exit-scope-and-exit-scope
- Preservation of variable visibility is invariant
under exiting a scope in both computation states.
- Var-resolve-preservep-of-prev-scope/frame-and-prev-scope/frame
- Preservation of variable resolution
when going back to the previous scope or frame.
- Var-resolve-preservep-of-prev-scope/frame-of-create-var
- Preservation of variable resolution under create-var,
for the previous scope or frame.
- Var-resolve-preservep-of-prev-scope/frame-and-create-var
- Combination of preservation of variable resolution
under create-var
and going back to the previous scope or frame.
- Var-resolve-preservep-of-trans-exit-scope-when-enter-scope
- This combines
var-resolve-preservep-of-exit-scope-when-enter-scope
with transitivity.
- Var-resolve-preservep-of-write-object
- Preservation of variable resolution under write-object.
