Interpreter fails to find object member

[peterwvj]

If you execute Entry`Run(), as defined below, the interpreter wrongly reports that the operation member is missing. The problem is the same in VDMJ.

class A

operations

public op : nat ==> ()
op (-) == skip;

end A

class B

operations

public op : bool ==> ()
op (-) == skip;

end B

class Entry

operations

public static Run : () ==> nat
Run () ==
let
	c1 : nat | bool = 1,
	c2 : nat | bool = true,
	objs = [new A(), new B()]
in
(
	for i = 1 to 2 do
		objs(i).op(if i = 1 then c1 else c2);
		
	return 2;	
);

end Entry

Expected result is 2, but actually the following error is produced:

Error 4035: Object has no field: op in 'Entry' (...A.vdmpp) at line 32:11

[nickbattle]

Because the objs sequence is a mixture of class types, it is creating a simulated "union" class for the sequence that has the signatures of the unions of the common members. Unfortunately it seems to have got that process wrong in this case. The simulated class/op is *union_A_B'op(nat), rather than *union_A_B'op(nat | bool). So the lookup of the second bool operation call is failing to find the actual bool member of B. I'll look at the simulated class creation process...

[nickbattle]

In fact the creation of the simulated union class is correct. But when the first operation call is made via objs(i), it assumes (wrongly) that it can use the current arg type as the type of the argument for all future invocations at this point in the spec. So the second invocation is looking for op(nat) again, which fails. I think the fix is simple.

[peterwvj]

Cool, thanks for explaining!

[nickbattle]

OK, now fixed in ncb/development.