RESOLVE (REusable SOftware Language with VErification) is a specification and programming language designed for verifying correctness of object oriented programs.
Suppose our function was A(i) and we have a substitution from A to A'. A' is a VCVarExp containing a VarExp with the name A. Somehow we need to support this, but not break the compiler...
Suppose our function was
A(i)
and we have a substitution fromA
toA'
.A'
is aVCVarExp
containing aVarExp
with the nameA
. Somehow we need to support this, but not break the compiler...