RESOLVE (REusable SOftware Language with VErification) is a specification and programming language designed for verifying correctness of object oriented programs.
Things are crazier when we have #A(i) that needs to be replaced with something else. See the following badly substituted Assume statement that originated from generating VCs for Array_Realiz.
Assume ((E' = #A(i)) and (S.Contents' = lambda (j : Z).( E if ([Universal] j = S.Top)
#A([Universal] j) otherwise)));
Those #A(i) should have been substituted with S.Contents
Things are crazier when we have
#A(i)that needs to be replaced with something else. See the following badly substitutedAssumestatement that originated from generating VCs forArray_Realiz.Those
#A(i)should have been substituted withS.Contents