"Polymorphic contracts" in VeriFast Java frontend

[bobru...@gmail.com]

Hey everyone,

I'm doing an assignment on static verification of java programs and stumbled across VeriFast's "polymorphic contracts", as mentioned on page 32 (page 438 in the journal) in the VeriFast for Java tutorial [1]. I would like to know how they work exactly.

I have looked at both papers referenced in the tutorial [2, 3], but as far as I can tell neither explains the use of polymorphic contracts. [2] does explain static/dynamic contracts, but then you still have to write two contracts. Or does VeriFast apply  the dynamic-to-static conversion mentioned in Parkinson and Bierman's work (paragrah 4 of [2])?

My question is, can someone tell me where in one of the two papers the idea is discussed more concretely, or otherwise explain me in general terms what it does? I would be immensely grateful for any pointers that can be given.

Kind regards,

Bob Rubbens

[1]: VeriFast for Java: A Tutorial. By Jan Smans, Bart Jacobs, and Frank Piessens. In Dave Clarke, Tobias Wrigstad, and James Noble (Eds.), Aliasing in Object-Oriented Programming, LNCS 7850, Springer, 2013.

[2]: Separation Logic, Abstraction and Inheritance. Matthew J. Parkinson, Gavin M. Bierman

[3]: Verification of Object-Oriented Programs With Invariants. Mike Barnett, Rob DeLine, Manuel Fahndrich, Rustan Leino, Wolfram Schulte

[Bart Jacobs]

Hi Bob,

If an instance method's contract includes instance predicate assertions that are implicitly applied to 'this', then these instance predicate assertions are interpreted differently for statically-bound calls (i.e. 'super' calls) and for dynamically-bound calls (i.e. non-'super' calls). For statically-bound calls, p(args), where p is an instance predicate, is interpreted as this.p(C.class)(args), where C is the class that declares the instance method; for dynamically-bound calls, p(args) is interpreted as this.p(this.getClass())(args).

For example:

class Cell {
    //@ predicate Cell(int value);

    int getValue();
    //@ requires Cell(?value);
    //@ ensures Cell(value) &*& result == value;

}

The contract of getValue() is interpreted as

    //@ requires this.Cell(Cell.class)(?value);
    //@ ensures this.Cell(Cell.class)(value) &*& result == value;

for calls of the form super.getValue() (which may of course appear only in subclasses of class Cell), and as

    //@ requires this.Cell(this.getClass())(?value);
    //@ ensures this.Cell(this.getClass())(value) &*& result == value;

for other calls.

Best regards,
Bart

[Bob Rubbens]

Thank you very much! This clarifies it for me.

Kind regards,

Bob Rubbens