Cannot prove basic functions relying only on Implementations/Inlining

Question

I have this class Course. I can prove the passed(int i) method when I use the contract for getBar(), not without it. Besides the contract of getBar() is also proven. Why can't I prove passed with inlining? I tried both Key 2.8 and Key 2.7.

public class Course {

    /*@ spec_public @*/ private int bar;
    /*@ spec_public @*/ private int time =100;
    public  boolean strict= true;

    /*@ public  normal_behaviour
      @ requires this!=null;
      @ ensures  \result==bar;
      @ assignable \nothing;
      @*/
    public int getBar() {
        return this.bar;
    }
    /*@ public normal_behaviour
      @ ensures  \result==(getBar()<=i);
      @*/
    public boolean passed(int i) {
        return this.getBar()<= i;
    }
}

score 1 · Accepted Answer · answered Mar 10 '21 at 15:01

The KeY verification engine can be used to verify JML annotated Java programs. (Mostly automatically, but interactive theorem proving is possible).

It works modularly. This means that every method is considered individually. Your method passed calls getBar, but getBar may actually be overriden in a subclass of Course – one which may be added later. KeY verifies programs using the "open program" paradigm which means that any extension (addition of classes) of the program cannot invalidate existing proofs.

Therefore: Inlining is not possible for this invocation since the method may be overridden.

Solutions:

Make the class final. (No overriding then)
Make the method getBar final (Again, no overriding)
Make the method getBar private (Again, no overriding)
In the GUI use the Options > Taclet Options options to set the option methodExpansion to noRestriction. (Change from "open program" to "closed program" and allow method expansion everywhere.)

Cannot prove basic functions relying only on Implementations/Inlining

1 Answers1