contracts and virtual methods

Jul 2, 2014 at 2:54 PM
Hi,

I know Spec# is no longer developed, but I'd like to check if you thought of a mechanism for the frame condition of virtual methods. This is interesrting for our own work on support for inheritance in SPARK 2014.

I've passed the code below to the Spec# checker on rise4fun:
using System;
using Microsoft.Contracts;

class T1 {

    protected int c1;

    public T1 ()
        ensures ((T1)this).isZero();
    {
        c1 = 0;
    }

    [Pure][Delayed]
    public virtual bool isMax ()
        ensures c1 == Int32.MaxValue ==> result == true;
    {
        return c1 == Int32.MaxValue;
    }

    [Pure][Delayed]
    public virtual bool isZero () {
        return c1 == 0;
    }

    public virtual void bump ()
        requires ! isMax();
        modifies this.*;
        ensures c1 == old(c1) + 1;
    {
        // C# and Spec# ignore possible overflows, so insert explicit assertion
        assert c1 < Int32.MaxValue;
        c1 = c1 + 1;
    }
}

class T2 : T1 {

    protected int c2;

    public T2 ()
        ensures ((T2)this).isZero();
    {
        c2 = 0;
    }

    [Pure][Delayed]
    public override bool isMax ()
        ensures c2 == Int32.MaxValue ==> result == true;
    {
        return base.isMax() || c2 == Int32.MaxValue;
    }

    [Pure][Delayed]
    public override bool isZero () {
        return base.isZero() && c2 == 0;
    }

    public override void bump ()
        ensures c2 == old(c2) + 1;
    {
        // This should derive from the precondition of bump
        assert c1 < Int32.MaxValue;
        assert c2 < Int32.MaxValue;
        base.bump();
        // C# and Spec# ignore possible overflows, so insert explicit assertion
        assert c2 < Int32.MaxValue;
        c2 = c2 + 1;
    }
}
and I got the following unproved properties:

c.ssc(8,12): warning CS2663: Method T1(), unsatisfied postcondition: ((T1)this).isZero() c.ssc(41,12): warning CS2663: Method T2(), unsatisfied postcondition: ((T2)this).isZero() c.ssc(59,26): warning CS2663: Method T2.bump(), unsatisfied postcondition: c2 == old(c2) + 1 c.ssc(67,9): warning CS2663: Assertion might not hold: c2 < Int32.MaxValue

I guess the first two are simply that static calls to virtual methods are not well supported. I'm more interested in the last two, which are due to the fact that the modifies clause of T1.bump is currently set to the default this.* (so all fields). The problem is that the modifies clause of T2.bump cannot be redefined, so the modifies clause of T1.bump cannot be simply c1. Is there a solution to that problem in Spec#?

Thanks
Developer
Jul 2, 2014 at 3:32 PM
Hi Yannick,

We do not have a solution to this problem in Spec#. It seems what you need to avoid the last two errors is a way to distinguish the specs that need to be respected by method overrides and the specs that apply only to the current implementation. Then you could use the former to verify dynamically-bound calls and the latter to verify statically-bound calls such as the base-call in T2.bump. Arnd Poetzsch-Heffter and I presented a logic that can do that at ESOP 1999; later work (two papers at POPL 2008) do something similar for separation logic. JML has support for these kinds of contracts ("code contracts" apply to the implementation only).

Cheers,
Peter
Jul 2, 2014 at 4:35 PM
Thanks Peter for the super-fast answer!

I'll have a look at your references ("A Programming Logic for Sequential Java", "Separation logic, abstraction and inheritance" and "Enhancing modular OO verification with separation logic"). We happen to have a design for supporting OO in SPARK that precisely distinguishes contracts for dynamically-bound calls from contracts for statically-bound calls. Good to know this is what you recommend!

I'm curious how you can achieve that in JML. I've written a JML version of the same program, and I have exactly the same problem:
public class T1 {

    //@ public model JMLDataGroup _state;

    public int c1; //@ in _state;

    //@ assignable _state;
    //@ ensures c1 == 0;  // cannot call isZero here, which would not be proved
    public T1 () {
        c1 = 0;
    }

    public /*@ pure */ boolean isMax () {
        return c1 == Integer.MAX_VALUE;
    }

    // cannot add a postcondition to isZero (say, to prove the postcondition of
    // T1's constructor calling isZero), as it would be inherited by
    // overridings.
    public /*@ pure */ boolean isZero () {
        return c1 == 0;
    }

    //@ requires c1 < Integer.MAX_VALUE;
    //@ assignable _state;
    //@ ensures c1 == \old(c1) + 1;
    public void bump () {
        // Java and JML ignore possible overflows, so insert explicit assertion
        //@ assert c1 < Integer.MAX_VALUE;
        c1 = c1 + 1;
    }
}

public class T2 extends T1 {

    public int c2; //@ in _state;

    //@ assignable _state;
    //@ ensures c2 == 0;
    public T2 () {
        c2 = 0;
    }

    public /*@ pure */ boolean isMax () {
        return super.isMax() || c2 == Integer.MAX_VALUE;
    }

    public /*@ pure */ boolean isZero () {
        return super.isZero() && c2 == 0;
    }

    //@ requires c1 < Integer.MAX_VALUE;
    //@ requires c2 < Integer.MAX_VALUE;
    //@ assignable _state;
    //@ ensures c2 == \old(c2) + 1;
    public void bump () {
        // This should derive from the precondition of bump
        //@ assert c2 < Integer.MAX_VALUE;
        super.bump();
        // Java and JML ignore possible overflows, so insert explicit assertion
        //@ assert c2 < Integer.MAX_VALUE;
        c2 = c2 + 1;
    }
}
for which I get the unproved properties (using OpenJML):
T2.java:28: warning: The prover cannot establish an assertion (Assert) in method bump
       //@ assert c2 < Integer.MAX_VALUE;
           ^
T2.java:23: warning: The prover cannot establish an assertion (Postcondition) in method bump
   public void bump () {
               ^
T2.java:22: warning: Associated declaration: T2.java:23: 
   //@ ensures c2 == \old(c2) + 1;
       ^
As T1.bump behavior is inherited by T2.bump, it would be incorrect to set the assignable clause to c1 only in T1.bump, no?
Developer
Jul 2, 2014 at 9:58 PM
Hi Yannick,

I think you could specify T1.bump like this:

/*@ code behavior
@ requires c1 < Integer.MAX_VALUE;
@ assignable c1;
@ behavior
@ requires c1 < Integer.MAX_VALUE;
@ assignable _state;
@ ensures c1 == \old(c1) + 1;
@*/

However, I am not sure whether OpenJML supports code contracts. See. Sec. 16.2 of the JML reference manual.

Cheers,
Peter
Jul 3, 2014 at 9:27 AM
Thanks Peter. Gary Leavens answered me the same thing on jmlspecs-interest mailing-list, but as he noted himself, this is not used by OpenJML for the statically bound call to super.bump() in T2.bump. The reason might be that the JML reference manual only states that code contracts can be used as well as other contracts for statically-bound calls, not instead of them:

"In verification of a method call, you can use a code specification case for a method m given in a class C only if you can prove that the method being called is method m in class C. This applies in particular to super calls, which is the main use for such code contracts. (It would also apply to calls to final methods, calls to methods in final classes, and calls to private or static methods.)"