examples_in_progress/wcet_hull.mlw

   1 module M
   2
   3 (* WCET example
   4
   5    This double loop program is actually O(n).
   6    We show it by introducing a variable t which counts the number of times
   7    the body of the inner loop is executed.
   8 *)
   9
  10   use int.Int
  11   use ref.Ref
  12   use array.Array
  13
  14   val constant n : int
  15     ensures { 0 <= result }
  16
  17   let hull (a: array int) (b: array int) =
  18     let j = ref 0 in
  19     let t = ref 0 in (* WCET *)
  20     for i = 0 to n-1 do
  21       invariant { 0 <= !j <= i <= n /\ i = !j + !t }
  22       while !j > 0 && b[!j-1] > a[i] do
  23         invariant { 0 <= !j <= i /\ i = !j + !t } variant { !j }
  24         j := !j - 1;
  25         t := !t + 1
  26       done;
  27       b[!j] <- a[i];
  28       j := !j + 1
  29     done;
  30     assert { 0 <= !t <= n }
  31
  32 end