Почему WP не может вывести «еще» близко?

Question

Я пытаюсь написать спецификацию для функции, которая принимает 2 указателя на int и присваивает меньшее значение первому указателю, а другое — второму.

Вот код и спецификация:

      /*@
   requires \valid(a) && \valid(b);

   assigns *a, *b;

   ensures *a >  *b ==> *a == \old(*b) && *b == \old(*a);
   ensures *a <= *b ==> *a == \old(*a) && *b == \old(*b);
*/
void order(int * a, int *b) {
  if (*a > *b) {
    int tmp = *a;
    *a = *b;
    *b = *a;
  }
}

И вот вывод frama-c -wp so.c:

      [kernel] Parsing so.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_order_post_2 : Unknown (Qed:4ms) (366ms)
[wp] Proved goals:    3 / 4
  Qed:             2  (0.40ms-2ms-5ms)
  Alt-Ergo:        1  (30ms) (16) (unknown: 1)

WP не может доказать второе пост-условие, можете ли вы объяснить мне, почему?

Answer 1

Оказывается, решение моего вопроса находится в учебнике Алена Бланшара, $3.3.1.1. ( здесь )

В пост-условиях мне не хватает примитивов вокруг *aа также *b. Итак, условия должны гласить:

      ensures \old(*a) < \old(*b) ==> *a == \old(*b) && *b == \old(*a) ;
ensures \old(*a) >= \old(*b) ==> *a == \old(*a) && *b == \old(*b) ;

Без \old, левые части импликаций относятся к значениям после выполнения функции.