Java interfaces support

[Bob Rubbens]

Hello everyone,

I have a question about Java interface support in Verifast. I have the following program (sorry, it is a bit lengthy) where I try to share state between interfaces. It works, but it requires a lot of boilerplate lemmas to convert between state3 and state5. Also, it requires another predicate Xstate to keep around as a starting point, which seems less favourable.

I would like to have one lemma that can be used for both Increment3 and Increment 5, but I'm not sure if that is possible (or, if it were possible, what the semantics of such a feature would be). Am I missing a way to structure this more efficiently or is this just the way interface support works in verifast?

interface Increment3 {
    //@ predicate state3(int val);

    void increment3();
    //@ requires state3(?x);
    //@ ensures state3(x + 3);
}

interface Increment5 {
    //@ predicate state5(int val);

    void increment5();
    //@ requires state5(?x);
    //@ ensures state5(x + 5);
}

class X implements Increment3, Increment5 {
   public int x;
   
   //@ predicate state3(int val) = x |-> val;
   //@ predicate state5(int val) = x |-> val;
   
   //@ predicate Xstate(int val) = x |-> val;

    public X()
    //@ requires true;
    //@ ensures Xstate(0);
    { }

    public void increment3()
    //@ requires state3(?y);
    //@ ensures state3(y + 3);
    {
    //@ open state3(y);
    x += 3;
    //@ close state3(y + 3);
    }
   
    public void increment5()
    //@ requires state5(?y);
    //@ ensures state5(y + 5);
    {
    //@ open state5(y);
    x += 5;
    //@ close state5(y + 5);
    }
   
    /*@
    lemma void Xstate_to_state3()
    requires Xstate(?y);
    ensures state3(y);
    {
        open Xstate(y);
        close state3(y);
    }  
   
    lemma void state3_to_state5()
    requires state3(?y);
    ensures state5(y);
    {
        open state3(y);
        close state5(y);
    }
   
    lemma void state5_to_Xstate()
    requires state5(?y);
    ensures Xstate(y);
    {
        open state5(y);
        close Xstate(y);
    }
      @*/
     
}

class Main {
    public static void main()
    //@ requires true;
    //@ ensures true;
    {
        X x = new X();
        //@ assert x.Xstate(0);
        foo(x);
        //@ assert x.Xstate(8);
    }

    public static void foo(X x)
    //@ requires x.Xstate(?y);
    //@ ensures x.Xstate(y+8);
    {
        //@ x.Xstate_to_state3();
    x.increment3();
    //@ x.state3_to_state5();
    x.increment5();
        //@ x.state5_to_Xstate();
    }
}

Kind regards,

Bob

[Bart Jacobs]

Dear Bob,

Yes, I think this is the best one can do in VeriFast. Note that VeriFast could probably be extended to automatically call the lemma methods in many cases, in the same way that Verifast already has support for calling regular (top-level) lemma functions automatically in many cases. (In fact, if class X is final, these lemmas can be written as toplevel lemma functions and then, one can exploit the existing automation support by replacing keyword 'lemma' by 'lemma_auto'.)

Getting rid of the lemma definitions seems trickier in general. These seem to serve an essential function: they define a way to map class X's abstract state to each interface's abstract state, and back.

If I remember correctly, Matthew Parkinson, in his PhD thesis, reduces the overhead of this by allowing subclasses to add parameters to superclass predicates. This implies a default mapping from subclass abstract states to superclass abstract states. (I think there's also a version, perhaps in the Jstar paper, where he generalizes this to records and projecting to a subset of the record fields.)

We have not (yet?) implemented anything similar in VeriFast.

Best,
Bart

--
You received this message because you are subscribed to the Google Groups "VeriFast" group.
To unsubscribe from this group and stop receiving emails from it, send an email to verifast+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/48caba8b-2c51-44f0-82d8-da7a4bac6689%40googlegroups.com.

[Bob Rubbens]

Thank you for your quick answer. I missed the lemma_auto functionality, that looks very useful. It would be interesting to see if such a default mapping could be defined from a newly defined predicate to both of the interface predicates, but semantics for that seem tricky to me (and not very useful/worth the effort if you can just add and prove the above lemmas).

To unsubscribe from this group and stop receiving emails from it, send an email to veri...@googlegroups.com.