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
f: nat -> nat
f(x) ==
let g: nat -> nat
g(a) ==
if a = 0 then 0 else a + g(a-1)
pre a > 0
measure a
in
g(x);
> p f(1)
Error 4034: Name 'measure_g' not in scope in 'DEFAULT' (test.vdm) at line 8:21
The problem is that the FunctionValue created by g does not include a measure function (though it does include a pre_g).
The text was updated successfully, but these errors were encountered:
The "measure" function within a FunctionValue is looked up on the fly, presumably as a hangover from being able to specify measures as the name of a function rather than as an expression. But the Context create that includes "g" (above) does not include a function for "measure_g" because the creation of the Context does not recurse into FunctionValues to see what they "create". It works for pre/post because their FunctionValues can be computed when the containing FunctionValue is defined.
This suggests the solution is to define "measure_g" in the same way as pre_g/post_g, and only do the name lookup if the measure "name" option is used. But be careful about polymorphic and curried functions, which can be awkward.
Consider the following:
The problem is that the FunctionValue created by g does not include a measure function (though it does include a pre_g).
The text was updated successfully, but these errors were encountered: