wcet_hull.mlw 848 Bytes
Newer Older
1
module M
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
2

3
(* WCET example
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
4 5 6 7 8 9

   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.
*)

10
  use import int.Int
11
  use import module ref.Ref
12
  use import module array.Array
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
13

Andrei Paskevich's avatar
Andrei Paskevich committed
14
  function n : int
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
15 16
  axiom N_non_negative : n >= 0

17 18 19 20
  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
Andrei Paskevich's avatar
Andrei Paskevich committed
21
      invariant { 0 <= !j <= i <= n /\ i = !j + !t }
22
      while !j > 0 && b[!j-1] > a[i] do
Andrei Paskevich's avatar
Andrei Paskevich committed
23
        invariant { 0 <= !j <= i /\ i = !j + !t } variant { !j }
24 25 26
        j := !j - 1;
        t := !t + 1
      done;
27
      b[!j] <- a[i];
28
      j := !j + 1
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
29
    done;
30
    assert { 0 <= !t <= n }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
31

32
end
33

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
34
(*
35
Local Variables:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
36
compile-command: "unset LANG; make -C ../.. examples/programs/wcet_hull.gui"
37
End:
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
38
*)