Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
bab273bb
Commit
bab273bb
authored
Nov 15, 2010
by
Jean-Christophe Filliâtre
Browse files
WCET example
parent
bab3063f
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
40 additions
and
0 deletions
+40
-0
examples/programs/wcet_hull.mlw
examples/programs/wcet_hull.mlw
+40
-0
No files found.
examples/programs/wcet_hull.mlw
0 → 100644
View file @
bab273bb
(* 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:
*)
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment