Commit bab273bb authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

WCET example

parent bab3063f
(* 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 array.ArrayLength as A
type array 'a = A.t int 'a
logic (#) (a : array 'a) (i : int) : 'a = A.get a i
logic n : int
axiom N_non_negative : n >= 0
}
let hull a b =
let j = ref 0 in
let t = ref 0 in (* WCET *)
for i = 0 to n-1 do
invariant { 0 <= !j <= i <= n and i = !j + !t }
while !j > 0 && !b#(!j-1) > a#(i) do
invariant { 0 <= !j <= i and i = !j + !t } variant { !j }
j := !j - 1;
t := !t + 1
done;
b := A.set !b !j (a#i);
j := !j + 1
done;
assert { 0 <= !t <= n }
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/wcet_hull.gui"
End:
*)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment