Формальная проверка с помощью «KeY» в Java не может доказать цикл сброса массива

В настоящее время я пытаюсь немного понять официальную проверку с помощью KeY инструмент для Java-программ.

Вот мой код Java с ключевыми аннотациями:

public class Test {
    public int[] a;

    /*@ public normal_behavior
    @ ensures (\forall int x; 0<=x && x<a.length; a[x]==1);
    @*/
    public void fillArray() {
        int i = 0;
        while(i < a.length) {
            a[i] = 1;
            i++;
        }
    }
}

К моему удивлению, KeY не смог доказать, что текущая программа действительна в соответствии с ее спецификацией. KeY не достигает цели 54. В окне текущей цели отображается:

 self.a.<created> = TRUE,
 wellFormed(heap),
 self.<created> = TRUE,
 Test::exactInstance(self) = TRUE,
 measuredByEmpty
==>
 self.a = null,
 self = null,
 {exc:=null || i:=0}
   \<{
         try {
             method-frame(source=fillArray()@Test, this=self)
             : {
                 while (i<this.a.length) {
                   this.a[i] = 1;
                   i++;
                 }
               }
         }
         catch (java.lang.Throwable e) {
             exc = e;
         }
     }\> (\forall int x; (x <= -1 | x >= self.a.length | self.a[x] = 1) & self.<inv> & exc = null)

Я действительно не понимаю: в чем основная причина невозможности доказать спецификацию?


java formal-verification jml key-formal-verification
person Agnius Vasiliauskas    schedule 02.03.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Самая основная причина сбоя заключалась в том, что если программа проверки обнаружила неограниченный цикл в методе, то она не могла следовать спецификации метода без инвариант цикла спецификация.

Таким образом, для каждой неограниченной петли мы должны указать инвариант петли. Инвариант цикла – это правило, которое выполняется для каждой итерации цикла. Каждая петля может иметь свое собственное инвариантное правило. Таким образом, код Java со спецификацией должен быть исправлен на:

public class Test{

  public int[] a;

  /*@ public normal_behavior
  @ ensures (\forall int x; 0<=x && x<a.length; a[x]==1); // method post-condition
  @ diverges true; // not necessary terminates
  @*/
  public void fillArray() {
    int i = 0;

    /*@ loop_invariant
    @ 0 <= i && i <= a.length &&  // i ∈ [0, a.length]
    @ (\forall int x; 0<=x && x<i; a[x]==1); // x ∈ [0, i) | a[x] = 1
    @ assignable a[*]; // Valid array location
    @*/
    while(i < a.length) {
      a[i] = 1;
      i++;
    }
  }

}

Самое сложное в размышлениях о том, как указать метод, будет найти инвариант цикла. Но в то же время - самое интересное. Ради причины я повторю инвариант этого цикла:

i ∈ [0, a.length]
x ∈ [0, i) | а [х] = 1

И это условие никогда не меняется в цикле в ЛЮБОЙ итерации. Вот почему это инвариант.

Кстати, если формальная спецификация составлена ​​правильно, мы можем отказаться от TDD и модульное тестирование за окном. Кого волнуют результаты во время выполнения, если можно математически доказать правильность программы в соответствии с ее спецификацией?

Если спецификация хороша, а семантика кода доказана, то ничего не может пойти не так при выполнении программы — это точно. Из-за этого формальная проверка является очень многообещающей областью.

person Agnius Vasiliauskas    schedule 03.03.2019
comment
Дополнительное замечание: придумать подходящий инвариант цикла может быть довольно обременительно, особенно если программа не обязательно верна. KeY также предлагает возможность выполнения Loop Expansion, то есть повторного выполнения цикла, как вы это знаете из конкретного выполнения. Однако для этого вам нужна верхняя граница размера вашего массива (как упоминалось Агниусом, для циклов unbounded вы должны указать инвариант). Добавить требует a.length ‹= 10; (или другое число) и отметьте Expand for Loop Treatment в опциях стратегии KeyY. Таким образом, вы можете сначала выполнить некоторую проверку перед проверкой программы. - person dsteinhoefel; 06.03.2019