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

[nickbattle]

So thanks, as usual, for creating a good example to demonstrate the problem. And I can confirm what you're seeing. It's also the same in VDMTools.

Your spec is trying to produce an invariant-enabled BRule version of class B by defining a type, equal to a B reference, but with an invariant over its x field value. This invariant is checked when you create values of type BRule, and you do that when you pass the b value to new C(b). The invariant of that value is not checked subsequently because the runtime believes that the "value" has already been checked and it cannot change. Normally (ie. in VDM-SL) that is true, but with VDM++ it is not true if the type invariant depends on state fields.

So this problem is similar to the other one in the sense that it's about "VDM++ being a semantic mess" :-) Though the detail here is different.

I think what ought to happen here is that you are given a strong warning (possibly even an error) for trying to create a type invariant that references state. If you tried to do something equally daft by calling an operation, the type checker would say:

Error 3181: Cannot access op(nat1) from a static context in 'C'
(That's with inv b_arg == op(b_arg.a.x);

Note that it's referring to a "static context". That's because it only expects to only see functions and expressions over the arguments or constants. Operation calls aren't allowed here because their value can change independently.

So I think the type checker is weak here, but I don't think the resulting behaviour is "wrong". It's a strange situation that has (wrongly) been allowed and which then behaves strangely.

Incidentally, if you create a subclass of B with the invariant set on its state, which in a sense is what I think you meant, "a version of B that has a state restriction", you get this:

class SubB is subclass of B
instance variables
	inv a.x <> 42;

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

end SubB

    dcl a:A := new A(1);
    dcl b:B := new SubB(a);  --<<-- Not a regular B
    let c = new C(b) in

> p new Runner().Run()
Error 4130: Instance invariant violated: inv_SubB in 'Runner' (test.vpp) at line 58:9
58:          a.x := 42;

So now that works because the invariant is (as intended) dynamically checking the state changes for the SubB object. As soon as you break it... you get the error.

I'll check why the type checker doesn't complain, and follow up...

[nickbattle]

Strangely, the type checking of field expressions (like your b_arg.a.x) did not check whether state access is allowed from the environment in which it is used. This is making me wonder whether we decided not to do this for some reason, and I'll check with the Language Board. But with the obvious fix added, your example spec now has a more robust error:

Parsed 5 classes in 0.16 secs. No syntax errors
Error 3366: Cannot access state field 'a' from this context in 'C' (test.vpp) at line 27:24
Error 3366: Cannot access state field 'x' from this context in 'C' (test.vpp) at line 27:26
Type checked 5 classes in 0.28 secs. Found 2 type errors
Bye

This change does not produce any unexpected errors in the CSK test suite (a large suite of VDM specs). It does produce a couple of errors in the VDMJ tests, but both of them look right - ie. it should have raised errors, but didn't.

[mortenhaahr]

Hi Nick, that is a great explanation that you provided.

Incidentally, if you create a subclass of B with the invariant set on its state, which in a sense is what I think you meant, "a version of B that has a state restriction", you get this:

I guess the interpreter prefers inheritance over composition. :-)
I think my formulation of the issue was wrong in that sense. I did not mean to imply that C should inherit from B, the composition was intended (and can be semantically correct in many models).

So I think the type checker is weak here, but I don't think the resulting behaviour is "wrong". It's a strange situation that has (wrongly) been allowed and which then behaves strangely.

I humbly disagree with the statement above as I believe the behaviour is wrong with the current definition in LRM. In my opinion, the only correct options, in this case, are to either:

• Limit the implementation of invariants to not allow placing invariants on values inside references to other objects. (As I believe you have done in your newest comment)
• Make the checking for invariants stronger such that it checks on modifications of reference types. However, I imagine this may provide significant performance implications (based on your responses in Assignment/invariant issue when updating variable twice #197.

If the former is chosen then it should probably be described in the LRM that invariant support for VDM++ is limited in the sense that it does not allow for this type of behaviour.

[nickbattle]

I would agree that the LRM is at fault if it does not adequately discuss the limitations of accessing state data from functional contexts. It may not even adequately define functional contexts. Unfortunately the design of VDM++ did not consider these matters (as far as I can tell) and so the LRM gives the reader the impression that types with invariants are just as "dynamic" as states with invariants, and you can mix the two. But I don't think that can be the case, and was not the intent of the designers.

Whichever way we resolve this, the LRM can be made clearer.

I've asked the LB about it. Let's see what they say :-)

[nickbattle]

It looks like this is a bug - the type checker really ought to prevent access to state data in its invariant. We're just making sure it doesn't break anything else...

We will update the LRM. The important addition will be a better clarification of a "functional context", which is where access to state is illegal. It looks like this covers:

• Explicit and implicit function bodies
• Pre/postconditions of functions or operations - these are functions, like pre_op(...).
• The expressions in type and state invariants, eq/ord clauses and init clauses (these are functions, like inv_T)
• Guard expressions (the RHS of per op => ...). These generate warnings rather than errors, so are different. But you can't call an operation from here, for example.
• The body of lambda expressions, which is obviously functional.

But we'll check this before fixing the LRM.

[nickbattle]

PS,

• Implicit functions don't have bodies (above!) but extended explicit functions, which look similar, do :-)
• Measure expressions are a functional context (because they generate measure_f functions)

[tomooda]

Nick, I think it also includes

• value definition bodies

[nickbattle]

@tomooda Mmm... my first thought was "oh yes, of course". But actually static operation calls are allowed here (by both tools), even if they're impure. This might be another case we can tighten up. It affects initialization though, so we have to be careful.

[tomooda]

@nickbattle Ah, I see your point. I tried in SL and found that values can be initialized by non-pure operation calls. Yes, this is itchy and the impact of changing it could be huge. Hmm.

[mortenhaahr]

Just to clarify, does this mean that any type of invariant where the state of an object is accessed will be prohibited?

[nickbattle]

It would mean that you can only call pure operations to access state from type invariants - and even that would give a warning. Pure operations are very limited in what they can do, but even they cannot guarantee that the state they use doesn't change, hence the warning (about a lack of referential transparency).

You can obviously access state from class invariants - this is what they are for! Similarly with SL invariants on state records.

[mortenhaahr]

This turned out to be a very interesting issue and I am looking much forward to seeing the implications on the language that it brings.

Based on a superficial look into existing examples, I expect that this will be a breaking change for some of them.

[nickbattle]

Several of the examples are very old and depend on dubious "classic" semantics (their READMEs may even say this). If you can give us details, we can check though?

Ideally, we ought to keep the examples up to date, but that's a lot of work unfortunately.

[mortenhaahr]

Discussion related to breaking

I agree that it would be a lot of work to maintain the examples.
Perhaps it would be better to archive them into "working" and "non-working" and let the authors decide if they wish to continue maintaining them. The non-working would be archived until fixed. (However, this is probably the topic of another issue/task.)

What I was more concerned with was code being used in the industry that "suddenly stops working" since they have (incorrectly) been relying on behavior such as the example in the top comment. I am unaware of how much VDM++ has been used in the industry but this might need to be a concern.

Examples

Below is shown a few examples that I think might break (please keep in mind that my understanding of the proposed fix is still limited).

Chemical plant

• Example name AlarmPP
• Used in the book "Validated Designs for Object-oriented Systems" (and during two separate courses I took at Aarhus University)

Breaking invariant:

PlantInv: set of Alarm * map Period to set of Expert ->  bool
PlantInv(as,sch) ==
  (forall p in set dom sch & sch(p) <> {}) and
  (forall a in set as &
     forall p in set dom sch &
       exists expert in set sch(p) &
         a.GetReqQuali() in set expert.GetQuali());

Breaking reason: The bottom line. a is a reference inside a set. a has instance variable reqQuali. We are placing an invariant based on reqQuali.

BusLines

• Example name BusLinesWithDBPP

Breaking invariant:

goal :  Waypoint;
inv goal.IsStop() = true;

Breaking reason: Goal is a reference to the type Waypoint. goal.IsStop() returns the value of the instance variable isStop inside the Waypoint. I believe this is analogous to the top comment.

ChessVDM (from issue)

• I also expect that the example provided in Assignment/invariant issue when updating variable twice #197 would break (both my example and Nick's minimum example) as the invariant placed on BoardState refers to references where the value is checked

[nickbattle]

OK, thanks for looking at these in more detail.

I've only looked at AlarmPP. The PlantInv function is used within the class invariant, so it should legitimately have access to state. But by putting it within a function, the authors force the getters to be pure and this also gives us a warning. But it's not a new warning - that is, this example always had this weakness, I think? If you move the expression from the body of the function and paste it (with renames) into the body of the "inv" clause, it is fine.

So there might be an interesting conversation to be had if this was used as a teaching model (about the pros and cons of using functions to access state via pure operations). But I don't think the new change (created by this issue, blocking object state access via fields in functions) affects this one?