frama-c - Frama-C/WP チュートリアルの例「不一致アルゴリズム」

Question

Frama-C (Neon-20140301) と Alt-Ergo で WP チュートリアルの例を試しています。「不一致アルゴリズム」の例には行き詰まりましたが、「equal」や「find」などの他の同様の例には問題はありません。コードを以下に示します。ポストコンディション P0、P2 は放電されていません。ここで何が間違っているのか誰にも教えてもらえますか?

#include<stdbool.h>

/*@
  @ predicate IsEqual {A,B} (float* a, integer n, float* b) =
  @   \forall integer i; 0 <= i < n ==> \at(a[i], A) == \at(b[i], B);
*/a

/*@ requires n >= 0;
  @ requires \valid(a+(0..n-1));
  @ requires \valid(b+(0..n-1));
  @ 
  @ assigns \nothing;
  @ 
  @ behavior all_equal:
  @   assumes IsEqual{Here,Here}(a, n, b);
  @   ensures P0: \result == n;
  @   
  @ behavior some_not_equal:
  @   assumes !IsEqual{Here,Here}(a, n, b);
  @   ensures P1: 0 <= \result < n;
  @   ensures P2: a[\result] != b[\result];
  @   ensures P3: IsEqual{Here,Here}(a, \result, b);
  @   
  @ complete behaviors;
  @ disjoint behaviors;
*/

bool mismatch (float* a, int n, float* b)
{
  /*@ loop invariant 0 <= i <= n;
    @ loop invariant IsEqual{Here,Here}(a, i, b);
    @ loop assigns i;
    @ loop variant n-i;
   */
  for (int i=0; i<n; i++) {
    if (a[i] != b[i])
      return i;
  }
  return n;
}