Невозможно доказать базовые функции, полагаясь только на реализации/встраивание

Question

У меня есть курс этого класса. Я могу доказать переданный (int i) метод, когда использую контракт для getBar(), а не без него. Кроме того, контракт getBar() также доказан. Почему я не могу подтвердить передачу с помощью встраивания? Пробовал и Key 2.8 и 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;
    }
}

Answer 1

Механизм проверки KeyY можно использовать для проверки программ Java с аннотациями JML . (В основном автоматически, но возможно и интерактивное доказательство теорем).

Работает модульно. Это означает, что каждый метод рассматривается индивидуально. Ваш метод passedcall , но на самом деле может быть переопределен в подклассе Course, который может быть добавлен позже. KeY проверяет программы, используя парадигму «открытой программы», что означает, что любое расширение (добавление классов) программы не может сделать существующие доказательства недействительными.

Следовательно: встраивание невозможно для этого вызова, так как метод может быть переопределен.

Решения :

1. Сделай класс. (Тогда без переопределения)
2. Сделать метод final(Опять же, без переопределения)
3. Сделать метод getBar private(Опять же, без переопределения)
4. В графическом интерфейсе используйте Options > Taclet Optionsпараметры, чтобы установить параметр methodExpansionк noRestriction. (Измените «открытую программу» на «закрытую программу» и разрешите расширение метода везде.)