The syntax/type checker cannot see if a post condition is trying to access an old instance variable

[cakemaster9001]

The syntax/type checker believes that the following program is correct:

class TestSetPost
instance variables
    private data : set of nat1 := {};

operations
public removeFromSet: nat1 ==> ()
removeFromSet(entry) == (
    data := data \ {entry};
)
post 
    (not exists newEntry in set data & newEntry = entry) 
    and
    (forall oldEntry in set data~ &  -- here
        oldEntry = entry or
        (exists newEntry in set data &
            newEntry = oldEntry))

end TestSetPost

In this program, there is a subtle error, which is the line with the --here comment. In that line, the previous data instance is accessed. This is not possible per the VDM10 language manual as specified in section old name on page 82. In this section, it is specified that only old global values can be accessed by the post-condition. The interpreter is implemented in a way such that this will fail, but I believe that it is easier to debug if it is caught in the syntax checker.

[nickbattle]

OK, this is quite subtle.

Firstly, it is perfectly OK to have "old" variables in a postcondition clause - in fact this is the only place where they would make sense, and I read the LRM to mean this.

If you try the same specification in VDM-SL, by converting the instance variable to a state record item, the specification works fine. But as written, in VDM++ you get a runtime scope error for the data~, which is definitely wrong.

If you change the postcondition to entry not in set data and entry in set data~ (which I think is the gist of the one you wrote), then it works correctly and you can put a breakpoint on the postcondition and see the two set values.

The subtlety here is that you are executing a postcondition function called _postremoveFromSet which is passed parameters for the argument and the old and new state. This follows the same pattern from VDM-SL. The difficulty with VDM++ is that the old object state is an arbitrarily complex graph of old object values, because of the potential for an object to reference other objects. So perhaps you should be able to write things like data~.field.member~(1).value~. This presents a challenge to the interpreter! However, unlike VDM-SL, the signature of postcondition functions is not defined for VDM++, so VDMJ (ie. VDM VSCode too) tries to discover the old variables that are referenced by a postcondition and pass just those values through to the postcondition function in a map. This is much more efficient.

But to do this, it has to analyse the postcondition expression to find "old" names. Evidently this is not working properly (though it works with the simpler expression I mentioned), so I will investigate...

[nickbattle]

And the answer... of course... is that the old name searching was not looking inside the forall bind clause, only the predicate itself. That's why it works correctly with the alternative post expression. It should be easy to fix.

So thanks for reporting this. If you need a patch for it, let me know, otherwise it will appear in the next snapshot release.

[nickbattle]

This is now fixed in the development branch.

Interpreter started
> create x := new TestSetPost()
> p x
= TestSetPost{#1, data:={1, 2, 3}}
Executed in 0.003 secs. 
> p x.removeFromSet(1)
= ()
Executed in 0.012 secs. 
> p x
= TestSetPost{#1, data:={2, 3}}
Executed in 0.003 secs. 
>