VDM++ indirections and invariants

[mortenhaahr]

This issue is somewhat similar to #197.

As part of an upcoming paper for OVT-21, ChessVDM, we were discussing some of the performance optimizations made in VDMJ related to VDM++ invariants and reference types. The question of whether indirections were also affected by the issue from #197 was raised.

Trying to test my hypothesis I found the bug in the snippet below.

Description:

• A is a class that holds some data x.
• B is a class with a reference to an instance of A.
• C defines a type BRule that is B with an invariant stating the value B.a.x <> 42.
• Runner defines the test:
  • An instance a of type A is created with x := 1.
  • An instance b of type B is created with a reference to a
  • An instance c of type C is created with a reference to b
  • The value for a.x is changed to 42 which is the illegal value for type BRule
  • Expected behaviour: Specification fails since invariant for BRule is broken.
  • Actual behaviour: Specification does not fail

class A
instance variables
	public x : nat1;

operations
    public A : nat1 ==> A
    A(a) == x := a;

end A

class B
instance variables
	public a : A;

operations
    public B : A ==> B
    B(a_arg) == a := a_arg;

end B

class C
instance variables
	public b : BRule;

types
    public BRule = B
    inv b_arg == b_arg.a.x <> 42;

operations
    public C : BRule ==> C
    C(b_arg) == b := b_arg;

end C

class Runner

operations
public Run: () ==> ()
Run() ==
(
    dcl a:A := new A(1);
    dcl b:B := new B(a);
    let c = new C(b) in
    (
        a.x := 42;
        IO`print("C: ");
        IO`print(c);
        IO`print("\nNOTICE: Invariant for BRule broken.\n");
    );
)
end Runner