why3/plugins/cfg/examples/max_array.mlcfg

module MaxArray

  use int.Int

  use array.Array

  let cfg compute_max (a:array int) : (max: int, ghost ind:int)
    requires { length a > 0 }
    ensures  { 0 <= ind < length a }
    ensures  { forall i. 0 <= i < length a -> a[ind] >= a[i] }
  =
  (* simulation of the C code: (from ACSL Manual, section 2.4.2 Loop invariants)

   i = 0;
   goto L;
   do {
      if (t[i] > m) { L: m = t[i]; }
      /*@ invariant
        @  0 <= i < n && m == \max(0,i,\lambda integer k; t[k]);
        @*/
      i++;
      }
    while (i < n);
    return m;

  *)
  var i m: int;
  ghost var ind: int;
  {
    i <- 0;
    goto L
  }
  L {
    m <- a[i];
    ind <- i;
    goto L1
  }
  L1 {
    invariant i_bounds   { 0 <= i < length a };
    invariant ind_bounds { 0 <= ind < length a };
    invariant m_and_ind  { m = a[ind] };
    invariant m_is_max   { forall j. 0 <= j <= i -> m >= a[j] };
                           (* (yes, j <= i, not j < i !) *)
    i <- i + 1;
    switch (i < length a)
    | True  -> goto L2
    | False -> return (m, ind)
    end
  }
  L2 {
    switch (a[i] > m)
    | True  -> goto L
    | False -> goto L1
    end
  }
end