SMT Prover дает "неизвестно", несмотря на сильные проверенные утверждения

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

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

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] Цель typed_main_assert_false: действительно (114ms) (97)
...

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