VDMJ dynamic type check problem

[joey-coleman]

The following bug was originally reported on Sourceforge by nick_battle, 2009-09-28 11:08:35:

There is an error in VDMJ's dynamic type checking, such that it cannot distinguish maps and sequences during assignments if the target type is a union of a map and a sequence. For example, the following:

op: () ==> int
op() ==
(
    dcl m:map int to bool | seq of int := {1 |-> true };
    m(2) := 123;
    return m(2);
)

This returns 123, even though internally that means the map has the value {1 |-> true, 2 |-> 123}, which is clearly an illegal value and should fail a dynamic type check at the point of the assignment. The static type check of this is OK as the type could be a seq of int, but at runtime it is actually a map int to bool.

[joey-coleman]

Comment by nick_battle, 2013-05-31 21:08:50.606000:

• Release: --> v2.0.0beta2

[joey-coleman]

Comment by nick_battle, 2013-05-31 21:08:50.911000:

Still present in 2.0.0b2

[joey-coleman]

Comment by nick_battle, 2013-08-09 07:31:51.166000:

• Release: v2.0.0beta2 --> v2.0.0beta4

[joey-coleman]

Comment by nick_battle, 2013-08-27 15:48:15.821000:

• Release: v2.0.0beta4 --> v2.0.0beta5

[joey-coleman]

Comment by nick_battle, 2013-09-02 11:05:56.669000:

• Release: v2.0.0beta5 --> v2.0.0beta6

[joey-coleman]

Comment by nick_battle, 2013-10-16 07:05:17.207000:

• Release: v2.0.0beta6 --> v2.0.0

[joey-coleman]

Comment by nick_battle, 2013-10-16 07:05:17.860000:

Still in 2.0

[nickbattle]

For what it's worth, VDMTools throws an internal error for this case as well...

C:\Cygwin\home\eclipse.overture\VDMJTests\test.vdm, l. 6, c. 8:
  Run-Time Error 164: Internal error, please report

The problem is that the type checker determines that the type of the thing being assigned should be "int | bool", and checks this at runtime. The runtime does not realise that "m" has already been committed to hold the map value rather than the sequence, and hence that the assignment should only work for "bool".

[nickbattle]

Now fixed in ncb/development. The example given produces the following:

> p op()
Error 4087: Cannot convert 123 (nat1) to bool in 'DEFAULT' (test.vdm) at line 6:9
Stopped in 'DEFAULT' (test.vdm) at line 6:9
6:          m(2) := 123;