Variable-visibility-preservation
Preservation of variable visibility 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 a variable with the same name
is visible in the computation state after the execution function.
The variable may be the same or a different one,
e.g. after executing a block item declaration
that introduces a variable that hides one in an outer scope.
The visibility is expressed via 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-visible-preservep-of-exec
- Preservation of variable visibility under execution,
for any number of peeled frames and scopes.
- Var-visible-preservep
- Check if all variable names visible in a computation state
are also visible in another computation state,
for any number of peeled frames and scopes.
- Var-visible-of-exec
- Preservation of variable visibility under execution.
- Var-visible-preservep-of-exit-scope-when-enter-scope
- If variable visibility is preserved between
a computation state just after entering a scope
and another computation state,
it is preserved also between
the first computation state before entering the scope
and the second computation state after exiting a scope.
- Var-visible-preservep-of-pop-frame-when-push-frame
- If variable visibility is preserved between
a computation state just after pushing a frame
and another computation state,
it is preserved also between
the first computation state before pushing the frame
and the second computation state after popping a frame.
- Var-visible-preservep-of-exit-scope-and-exit-scope
- Preservation of variable visibility is invariant
under exiting a scope in both computation states.
- Var-visible-preservep-of-pop-frame-and-pop-frame
- Preservation of variable visibility is invariant
under popping a frame in both computation states.
- Var-visible-preservep-of-trans-exit-scope-when-enter-scope
- This combines
var-visible-preservep-of-exit-scope-when-enter-scope
with transitivity.
- Var-visible-preservep-of-create-var
- Preservation of variable visibility under create-var.
- Var-visible-preservep-of-write-object
- Preservation of variable visbility under write-object.
