You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Combinatorial traces can reference state data in VDM-SL (just as they can reference instance variables in VDM++). But there is a bug which prevents state values from being populated in the runtime environment. So the following specification has no type errors, but at runtime the "s" state variable cannot be found.
state Sigma of
s : nat
init z == z = mk_Sigma(1)
end
traces
T: let x = s in op(x) -- "s" is not found at test expansion
The fix will be available in 2.0.2.
The text was updated successfully, but these errors were encountered:
Combinatorial traces can reference state data in VDM-SL (just as they can reference instance variables in VDM++). But there is a bug which prevents state values from being populated in the runtime environment. So the following specification has no type errors, but at runtime the "s" state variable cannot be found.
The fix will be available in 2.0.2.
The text was updated successfully, but these errors were encountered: