4.2.0 Measure Expressions

This release contain the changes for RM42, which makes changes to measure clauses. This is also the first release that contains no new Fujitsu IPR.

Measure clauses can now contain a simple expression, using the same parameter variables as the main function, very much like a precondition. Such expressions also cause a function to be created, called measure_f (similar to the creation of pre_f). This function will have the same parameters as the main function, but return a nat or nat tuple, depending on the type of the measure expression.

For example, a measure can now be written as follows:

sum: seq of nat -> nat
sum(s) ==
    if s = [] then 0 else hd s + sum(tl s)
    -- measure m;      -- measure can be a function
    measure len s;     -- or the expression can now be added inline

m: seq of nat -> nat
m(s) ==
    len s;

If you use an inline measure, a function is created:

> env
sum = (seq of (nat) -> nat)
m = (seq of (nat) -> nat)
measure_sum = (seq of (nat) +> nat)

> p measure_sum([1,2,3])
= 3
Executed in 0.016 secs. 

> p sum([1,2,3])
= 6
Executed in 0.007 secs. 

If you have a complex recursive function that you have not yet written a measure for, or that cannot sensibly have a measure defined, you can suppress the warning by defining a measure as "is not yet specified":

sum: seq of nat -> nat
sum(s) ==
    if s = [] then 0 else hd s + sum(tl s)
    measure is not yet specified;    -- suppress warning about missing measure

4.2.0 Build 180125, Initial release
4.2.0 Build 180126, Correction for type check of subtractions
4.2.0 Build 180317, Fix for lambda values with polymorphic types
4.2.0 Build 180405, Correction for ext rd/wr name/scope lookups
4.2.0 Build 180608, Small correct to POs with old variable identifiers
4.2.0 Build 180705, Experimental annotations feature (see the -annotations jar)
4.2.0 Build 180721, Added extra -verbose output and optimized initialization
4.2.0 Build 181106, Corrected narrow_ execution and reserved word detection
4.2.0 Build 181110, Absorb ContextExceptions during union value conversions
4.2.0 Build 181114, Correct VDMJC Manifest to use the right main class.