Assignment/invariant issue when updating variable twice

[mortenhaahr]

I found an issue while working on my chess model. The issue appears when updating a variable twice in an operation where the second expression is only valid after the first expression has been executed.

Expected behavior: Looking inside the move operation when debugging test_board operation:

1. The dead_piece is removed from the set of pieces
2. The invariant for board_state is checked
3. The position of piece is updated
4. The invariant for board_state is checked (since piece refers to an object inside of board_state)
5. The BoardState invariant is not violated

Actual behavior: Looking inside the move operation when debugging test_board operation:

1. The dead_piece is removed from the set of pieces
2. The invariant for board_state is checked
3. The position of piece is updated
4. The invariant for board_state is checked (since piece refers to an object inside of board_state)
5. The BoardState invariant is violated

Comments: From debugging I have found the following:

• piece gets assigned the reference number 2.
• dead_piece gets the reference number 3.
• When debugging and putting a breakpoint on the invariant of BoardState it appears as if the invariant is called with a piece with reference number 3 still in s. This appears as a bug to me.

Example:

class Piece
types
    public Coordinate ::
        x : nat1
        y : nat1;

instance variables
    public position : Coordinate;

operations
    public Piece : Coordinate ==> Piece
    Piece(coord) == position := coord;

end Piece

class Board
types
    public BoardState = set1 of Piece
    inv s == forall p1, p2 in set s & p1 <> p2 => p1.position <> p2.position; -- Two Pieces cannot be on the same position
values

instance variables
    public board_state : BoardState;

operations

    public Board : BoardState ==> Board
    Board(s) == board_state := s;

    public move: Piece * Piece * Piece`Coordinate ==> ()
    move(piece, dead_piece, coord) == (
            board_state := board_state \ {dead_piece}; -- Remove `dead_piece` 
            piece.position := coord -- This is where it breaks.
    )
    pre piece in set board_state and dead_piece in set board_state;

end Board

class Test

operations
public test_board : () ==> ()
test_board() == (
    let p1 = new Piece(mk_Piece`Coordinate(1, 1)) in
        let p2 = new Piece(mk_Piece`Coordinate(2, 2)) in
            let board = new Board({p1, p2}) in
                board.move(p1, p2, mk_Piece`Coordinate(2,2));
);

end Test

[nickbattle]

Thanks for reporting this and I can confirm that it is reproducible. I can also confirm that it is not causing violations on VDMTools, which suggests this is a genuine problem. Unpicking invariant issues can be tedious, I'm afraid, but I'll take a look. I'll update you when I find out what's going on.

[nickbattle]

It looks like the problem is that the items within the BoardState set have value listeners that refer to the set value, but when items are removed from the set, those listener values don't get updated to reflect the new set content. Hence they are running the invariant against the wrong set value. Something like that. Still investigating.

[nickbattle]

I think I can see what's wrong (but it will be tough to fix). You're banging up against what is possible for tools to do (with VDM++) by using invariants that reason about the value of object fields.

With VDM-SL, values are simple things that can be composed to build other values, but importantly there is no aliasing: values have names in the specification, but one name only every refers to one thing. By introducing object references, VDM++ brings in aliasing, which makes things harder. So in you case, values are added to a set whose type has an invariant; all of the values inside that set have an InvariantListener so that if you change their values, the invariant can be re-evaluated. When new values are added to the set, they are (usually) stripped of all their listener baggage (from where they came from) and are added to the set with the new InvariantListener. That works fine for simple values, but with object references the same reference can be a part of other structures with other invariants, so we can't strip them when we add them to other invariant values - that might avoid invariant checks elsewhere, or break the concurrent behaviour of the object, for example.

So what seems to have happened is that, in your case, the Piece.position (via a reference) being updated has had a listener added for the original set content, but that has not been removed when the set was updated with the new value (removing the other Piece). So when the change is checked, both listeners run, and the old one refers to a "garbage" value that should have been removed.

Naively, removing all listeners on object assignment would "fix it for you" but break something else! So I need to look at how object reference listeners should be "edited" on assignment. Remember that an object reference is really the root of a graph of object references, any of which could be updated and be tested by the containing invariant. So this is not trivial and may have a significant performance hit. This is what I was hinting at above: ultimately, the tools have limitations of what is possible to simulate in VDM++, otherwise we end up "testing everything every time anything happens".

So leave it with me :-) This should work, but VDM++ simulation will probably still have limitations that VDM-SL does not. I can't think of a simple workaround, unless you can find a way to avoid invariants over object fields.

[mortenhaahr]

Hi @nickbattle, Thank you for the great answers so far.

I am afraid that I have discovered the bug to be of greater scope than only with invariants. It can also happen with normal operations. I will see if I can write a simple example of it.

Edit: Please disregard this comment - it was a logical error in my program.

[nickbattle]

Simple examples help a lot, the simpler the better!

[leouk]

This is an interesting situation. Even though I don't know (or use) VDM++ much, would it be possible to have something akin to a "C-struct" or an object reference with final fields (i.e. immutable)? This way things would be "easier", given it doesn't really make sense to have references to piece-positions (but to pieces)? i.e. positions are fixed, pieces are not?

[mortenhaahr]

Simple examples help a lot, the simpler the better!

@nickbattle I updated my comment - the error does not appear to happen on normal operations.

[nickbattle]

Phew! :-)

[mortenhaahr]

Workaround for people dealing with this issue: If you generate a new variable instead of updating the state of the current it should work. So in my example the move operation becomes:

  public move: Piece * Piece * Piece`Coordinate ==> ()
  move(piece, dead_piece, coord) == (
          board_state := board_state \ {dead_piece}; -- Remove `dead_piece` 
          let new_piece = new Piece(coord) in
              board_state := (board_state \ {piece}) union {new_piece}
  )
  pre piece in set board_state and dead_piece in set board_state;

[nickbattle]

Ah yes, and you can see why that would work because the new object is "clean". I'll still work on a better general solution though.

[nickbattle]

The closer I look at this, the more complicated it gets. We may have to rethink the way value listeners work for updates in the face of object references. But I'm still working on it :-)

[mortenhaahr]

This is definitely an interesting issue that is way above my current understanding but it is very interesting to follow.

To me it almost seems like an issue on the way object references work in general, since it seems odd that a reference can be in an old state. Would it be possible in VDM-J to pass the Java objects by reference to the invariant checker? Of course only for VDM++ class instances

[nickbattle]

The reference/alias nature of object references significantly complicates the way VDMJ handles values, and that is at the root of this bug. In a wider sense (relating to your other problem about "old" object values), yes, it is a strange idea that object references (and their references etc) would be "old". It's as though the VDM++ designers just wanted to be able to write something like post instvar~ < instvar but hadn't thought through all of the ramifications. Things are much better defined in VDM-SL (and I would advise anyone writing serious specifications to consider using it over VDM++).

[nickbattle]

OK, I think I've found a solution to this. When invariant values are updated, the old/current value is cleaned of Java references to that value, since it is about to be overwritten. With VDM-SL, the current value is overwritten in a naive sense and becomes garbage because nothing references it. But with VDM++, a value can contain (VDM) object references, so we cannot guarantee that an overwritten value will never be used, and hence we currently preserve listeners on object values. But by editing the old value selectively, we can clean up just the listener references to the old value that we are about to replace.

It definitely works for your small example. I'm still testing other scenarios though. If you want to give this a try, it is currently in the development branch of VDMJ.

[mortenhaahr]

Hi @nickbattle, that sounds like a great solution! I would love to test it out but I am afraid that I don't have much spare time at moment. (Final projects with tight deadlines followed by exams). If you still need help with testing in February then I would gladly have a look at it.

[nickbattle]

Incidentally, if we ever have to come back to this, the following is the simplest version of the bug that I could produce. It's only slightly simpler than the original, but every little helps - in particular, the test() operation does all the steps, without having to invoke another operation:

class Piece
instance variables
    public x : nat1;

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

end Piece

class Board
types
    BoardState = set1 of Piece
    inv s ==
        forall p1, p2 in set s &
            p1 <> p2 => p1.x <> p2.x;

instance variables
    board_state : BoardState;

operations
    public test: () ==> ()
    test() ==
    (
    dcl p1:Piece := new Piece(1);
        dcl p2:Piece := new Piece(2);
        board_state := {p1, p2};
        board_state := board_state \ {p2}; 
        p1.x := 2 -- This is where it breaks.
    )

end Board

[nickbattle]

Closing this. It seems to behave correctly now.