Type intersection clarification / warning

[leouk]

Everywhere in VDM expressions resulting types are a union of the expression parts. Except in map comprehensions like

vWarning1 = { 1 |-> 5 | x in set {1,2,3}, x in set {4,5,6} & x > 3 };
vWarning11= { 1 |-> 5 | x in set {4,5,6}, x in set {1,2,3,4} & x > 3 };
vWarning2 = { 1 |-> 5 | x in set {1,2,3}, x in set {4,5,6} & x > 3 };
vWarning3 = { 1 |-> 5 | x in set {1,2,3}, x in set {4,5,6}, x in set {7,8,9} & x > 6 };
vWarning4 = { 1 | fv in set {3,4,5}, x in set {1,2,3} & x >= fv };
vWarning5 = { 1|-> 5 | x in set {<A>,<B>,<C>}, x in set {1,2,3} & x = <A> };

The last one in particular is quite wicked given that intersecting quote with basic types is empty, but "x=" is not a type error! So some warning clarifying things to the user in these degenerate cases might be useful.

I've checked through the email conversation I had with Leo when this point was originally raised during the Isabelle work. There were two problems: firstly, there was a type checking error in VDMJ, such that it did not correctly determine the type of a bound variable if it occurred in more than one bind clause (now fixed); second, the behaviour of VDM in this case is quite surprising, if you're not expecting it.

When there is a collection of bindings that bind the same variable(s), the effect is to only select those bindings that satisfy all of the bind clauses - in effect it is an "and" of them. So x in set {4,5,6}, x in set {1,2,3,4} will bind x to the value 4 because that is common to both sets. But that is the only binding.

The last case should probably be identified by the type checker because it is impossible to bind any "x" values, since the types of the sets do not overlap. More generally, the types of the bound variables (which may be components of the set elements) must overlap for all bindings of a given name. So you might have mk_(-, x) in set A, {x} in set B, which would be impossible to bind if the second element of the tuples in A does not overlap with the type of the singleton subsets in B.

The same checking behaviour would then naturally extend to other cases, like the binding of parameters in a function, where the same is possible: multiple occurrences of a name are allowed, but they must bind the same value, which is impossible if the types do not overlap.

So I think the type checker can be improved, but that the tools are correctly interpreting the VDM language (VDMTools is the same in this regard).

[nickbattle]

I've drafted something to make the checking here the same as that done for function parameters. It produces the following for vWarning5:

Error 3322: Duplicate patterns bind to different types in 'DEFAULT' (test.vdm) at line 2:17
x: (<A> | <B> | <C>)
x: nat1
Type checked 1 module in 0.272 secs. Found 1 type error

The other vWarning examples are not errors or warnings.

[nickbattle]

That change is now pushed to the development branch, if anyone wants to try it.

[nickbattle]

Incidentally, the equivalent case for function parameter bindings could be something like this:

functions
    f: set of (<A>|<B>|<C>) * set of nat1 -> bool
    f({x}, {x}) ==
        is_(x, nat1);

Error 3322: Duplicate patterns bind to different types in 'DEFAULT' (test.vdm) at line 2:5
x: (<A> | <B> | <C>)
x: nat1
Type checked 1 module in 0.143 secs. Found 1 type error

[kgpierce]

Changes were added for new warnings. Closed by LB.