#20 Examplar Incorrectly Substituted For in VCs

[H. Smith]

It would seem that when a type's constraints make their way into VCs, the exemplar variable name is replaced with the name of the variable representing the object of that type in the OPERATION, not the PROCEDURE. For example:

Type Family X is modeled by B;
exemplar C;
constraints C = True;

Enhancement ...
Operation Foo(updates E : X);
end Enhancement;

Relization ...
Procedure Foo(updates R: X);
Confirm R = True;
end;
end Realization;

Will generate a VC like:

E = True
====>
R = True