module M

(* WCET example

   This double loop program is actually O(n).
   We show it by introducing a variable t which counts the number of times
   the body of the inner loop is executed.
*)

  use import int.Int
  use import module ref.Ref
  use import module array.Array

  function n : int
  axiom N_non_negative : n >= 0

  let hull (a: array int) (b: array int) =
    let j = ref 0 in
    let t = ref 0 in (* WCET *)
    for i = 0 to n-1 do
      invariant { 0 <= !j <= i <= n /\ i = !j + !t }
      while !j > 0 && b[!j-1] > a[i] do
        invariant { 0 <= !j <= i /\ i = !j + !t } variant { !j }
        j := !j - 1;
        t := !t + 1
      done;
      b[!j] <- a[i];
      j := !j + 1
    done;
    assert { 0 <= !t <= n }

end

(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/wcet_hull.gui"
End:
*)