Доказывающий выходы SMT «неизвестно», несмотря на сильные доказанными утверждения

Question

Предположим, мы имеем следующий C аннотированный код:

#define L 3 
int a[L] = {0}; 
/*@ requires \valid(a+(0..(L - 1))); 
    ensures \forall int j; 0 <= j < L ==> (a[j] == j); */ 
int main() { 
     int i = 0; 
     /*@ loop assigns i, a[0..(i-1)]; 
      loop invariant inv1: 0 <= i <= L; 
      loop invariant inv2: 
         \forall int k; 0 <= k < i ==> a[k] == k; 
     */ 
     while (i < L) { 
      a[i] = i; 
      i++; 
     } 
     /*@ assert final_progress: 
       \forall int k; 0 < k < L ==> a[k] == a[k-1] + 1; 
      assert final_c: 
       a[2] == a[1] - 1; */ 
     return 0; 
} 

Почему Alt-Ergo/Z3 дает «неизвестно» или тайм-ауты для final_c утверждения, несмотря на то, что final_progress заявление было доказано? Мне бы очень хотелось увидеть «Недействительно» для таких явно (с точки зрения пользователя) недопустимых утверждений.

$ frama-c -wp -wp-rte -wp-prover z3 test2.c 
.. 
[wp] [z3] Goal typed_main_assert_final_c : Unknown (455ms) 

$ frama-c -wp -wp-rte -wp-prover alt-ergo test2.c 
.. 
[wp] [Alt-Ergo] Goal typed_main_assert_final_c : Timeout 

Answer 1

В БК плагин не поддерживает маркировки свойства (предварительные условия, постусловия, пользовательские утверждения) недействительными. Как указано в разделе 2.2 WP plugin manual статус является одним из:

1. — Нет доказательств попытки.

2. — Недвижимость не подтверждена.

   Этот статус означает, что доказательства не удалось найти. Возможно, это связано с тем, что свойство действительно недействительно.

3. — Недвижимость действительна, но имеет зависимости.

   Вы увидите, что этот статус применяется к свойству, если плагин WP способен доказать свойство, предполагающее, что одно или несколько свойств полностью действительны.

4. — Собственность и все ее зависимости полностью действительны.

Хотя WP плагин не поддерживает маркировки свойства как недействительный, вы можете использовать трюк отстаивания \false в конце функции:

#define L 3 
int a[L] = {0}; 
/*@ requires \valid(a+(0..(L - 1))); 
    ensures \forall int j; 0 <= j < L ==> (a[j] == j); */ 
int main() 
{ 
    int i = 0; 
    /*@ loop assigns i, a[0..(i-1)]; 
     loop invariant inv1: 0 <= i <= L; 
     loop invariant inv2: \forall int k; 0 <= k < i ==> a[k] == k; 
    */ 
    while (i < L) { 
     a[i] = i; 
     i++; 
    } 
    //@ assert final_progress: \forall int k; 0 < k < L ==> a[k] == a[k-1] + 1; 
    //@ assert final_c: a[2] == a[1] - 1; 
    //@ assert false: \false; 
    return 0; 
} 

Запуск WP плагин этого кода приводит :

 
... 
[wp] [Alt-Ergo] Goal typed_main_assert_false : Valid (114ms) (97) 
... 

Если WP плагин отмечает assert \false правомочно (в графическом интерфейсе будет отображаться как действительные, но-имеет-зависимость), то вы знаете, что есть недопустимый Prope RTY.