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

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

0 голосов
/ 02 марта 2019

В настоящее время я пытаюсь понять формальную проверку с помощью инструмента 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 , он не может доказать, что текущая программа действительна в соответствии с ее спецификацией. Ключ завершается неудачно при достижении цели 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)

Я не понимаю, что является основной причиной неудачного подтверждения спецификации?

1 Ответ

0 голосов
/ 03 марта 2019

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

Таким образомдля каждого неограниченного цикла мы должны указать инвариант цикла.Инвариант цикла - это некое правило, которое сохраняет значение для каждой итерации цикла .Каждый цикл может иметь свое собственное инвариантное правило.Поэтому код 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) |a [x] = 1

И это условие никогда не меняется в цикле в ANY итерации.Вот почему это инвариант .

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

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

...