Execution in the presence of type bindings

Question

Consider the two function definitions

  test1 (x:nat) res:set of nat
    == { m | m:nat & m in set {0,...,x} };

  test2 (x:nat) res:set of nat
    == { m | m in set {0,...,x} & true };

Running test2(1000) in Overture gives the set of natural numbers up to 1000. Running test1(1000) gives the set of natural numbers up to 255. I understand there are complications when there are explicit type bindings in explicit function definitions, but in this case it just silently gives the wrong answer. It seems that when a type binding for natural numbers appears in a definition, the range is restricted to 0..255. At least, thats what seems to be happening from the outside.

Chapter 8 of the language manual states "Notice that type binds can only be executed by the VDM interpreters in case the type can be deduced to be finite statically." Are there any rules for when the type can be deduced to be finite statically?

Answer 1

I'm pretty sure now that this behaviour is a feature of Overture that I didn't know about. By default, the interpreter cannot handle type binds for infinite types, but there is an option in the "Debugger" launcher tab to allow numeric type binds (int, nat, nat1 and curiously, real) to expand to a range of integer values from "minint" to "maxint". You also have to tick the "numeric_type_bind_generation" box to enable the functionality.

So I'm sorry about the earlier confusion. I don't think this feature is particularly useful and I've never heard of anyone using it, but I'm pretty sure it explains what you're seeing.

Answer 2

I'm not sure what's happening here for you. When I try this specification with Overture 2.3.0 (as well as the 2.3.1 snapshot and VDMJ) the test1 function always fails immediately saying:

Error 4: Cannot get bind values for type nat

Are you running this test as part of a larger specification? The manual is correct. Overture cannot execute type bindings unless it can determine that the type is finite, like "bool", or something composed entirely of finite types, like "set of bool" or "map P to Q" where P and Q are finite.

The basic finite types are bool and all quote types. These types can then be used to build more complex types with the type constructors - "set of" etc. All of the type constructors, apart from "seq of", will yield a finite type as long as all the member types are finite. Note that this includes [optional] types, product types like A*B, type unions like A|B|C, and record constructors.