Renaming-variables-safety
Proof that variable renaming preserves the static safety checks.
As mentioned in renaming-variables,
the renaming list/alist consists of
the variables in scope for the old code (the keys of the alist) and
the variables in scope for the new code (the values of the alist).
Thus, we prove theorems saying that
if two pieces of code are related by variable renaming,
and the old code is safe with respect to
the variables that are the keys of the renaming alist,
then the new code is safe with respect to
the variables that are the values of the renaming alist;
furthermore, if the renaming list is updated,
the updated variables in scope are still the keys and values,
for the old and new code;
furthermore, if the static safety checks
return information other than updated variables in scope
(e.g. modes, or numbers of values),
that information is the same for old and new code.
The above is just a sketch.
Things are explained in more detail below.
Subtopics
- Renaming-variables-statements/blocks/cases/fundefs-safety
- Proof that variable renaming preserves the safety of
statements, blocks, and related entities.
- Renaming-variables-expression-safety
- Proof that variable renaming preserves the safety of expressions.
- Theorems-about-function-tables-and-variable-renaming
- Theorems about function tables and related concepts
for code related by variable renaming.
- Varset-old
- Variables in scope for the old code in variable renaming.
- Varset-new
- Variables in scope for the new code in variable renaming.
- Varset-old/new-of-add-var/vars-to-var-renaming
- Theorems about varset-old and varset-new
applied to
add-var-to-var-renaming and add-vars-to-var-renaming.
- Check-safe-path/paths-when-path/paths-renamevar
- If two (lists of) paths are related by variable renaming,
the safety of the old one implies the safety of the new one.
- Add-var/vars-not-error-when-add-var/vars-to-var-renaming
- If variables can be added to a variable renaming,
then the new variables can be added to the ones in the new scope.
- Check-var-when-var-renamevar
- If a variable is in scope for the old code,
its renamed counterpart is in scope for the new code.
