Commit 65769564 authored by Andrei Paskevich's avatar Andrei Paskevich

examples: minor syntax adjustments

parent ebe465a7
......@@ -30,14 +30,14 @@ module Algo63
val random (m n: int) : int ensures { m <= result <= n }
let partition_ (a: array int) (m n: int) (i j: ref int) (ghost ghx: ref int) =
let partition_ (a: array int) (m n: int) (i j: ref int) (ghost ghx: ref int)
requires { 0 <= m < n < length a }
ensures { m <= !j < !i <= n }
ensures { permut_sub (old a) a m (n+1) }
ensures { forall r:int. m <= r <= !j -> a[r] <= !ghx }
ensures { forall r:int. !j < r < !i -> a[r] = !ghx }
ensures { forall r:int. !i <= r <= n -> a[r] >= !ghx }
'Init:
=
let f = random m n in
let x = a[f] in
ghx := x;
......@@ -45,12 +45,12 @@ module Algo63
j := n;
let rec up_down () variant { 1 + !j - !i } =
requires { m <= !j <= n /\ m <= !i <= n }
requires { permut_sub (at a 'Init) a m (n+1) }
requires { permut_sub (old a) a m (n+1) }
requires { forall r:int. m <= r < !i -> a[r] <= x }
requires { forall r:int. !j < r <= n -> a[r] >= x }
requires { a[f] = x }
ensures { m <= !j <= !i <= n }
ensures { permut_sub (at a 'Init) a m (n+1) }
ensures { permut_sub (old a) a m (n+1) }
ensures { !i = n \/ a[!i] > x }
ensures { !j = m \/ a[!j] < x }
ensures { a[f] = x }
......
......@@ -24,7 +24,7 @@ module Algo64
val partition (a: array int) (m n: int) (i j: ref int) (ghost x: ref int) :
unit
requires { 0 <= m < n < length a }
writes { a, i, j}
writes { a, i, j }
ensures { m <= !j < !i <= n }
ensures { permut_sub (old a) a m (n+1) }
ensures { forall r:int. m <= r <= !j -> a[r] <= !x }
......@@ -49,10 +49,12 @@ module Algo64
let j = ref 0 in
let ghost x = ref 42 in
partition a m n i j x;
'L1: quicksort a m !j;
assert { qs_partition (at a 'L1) a m n !i !j !x };
'L2: quicksort a !i n;
assert { qs_partition (at a 'L2) a m n !i !j !x }
label L1 in
quicksort a m !j;
assert { qs_partition (a at L1) a m n !i !j !x };
label L2 in
quicksort a !i n;
assert { qs_partition (a at L2) a m n !i !j !x }
end
let qs (a:array int) : unit
......
......@@ -43,19 +43,19 @@ module Algo65
let j = ref 0 in
let ghost x = ref 42 in
partition a m n i j x;
'L1:
label L1 in
if k <= !j then find a m !j k;
assert { permut_sub (at a 'L1) a m (n+1) };
assert { forall r:int. !j < r <= n -> a[r] = (at a 'L1)[r] };
assert { permut_sub (a at L1) a m (n+1) };
assert { forall r:int. !j < r <= n -> a[r] = (a at L1)[r] };
assert { forall r:int. m <= r <= !j ->
(exists s:int. m <= s <= !j /\ a[r] = (at a 'L1)[s]) &&
(exists s:int. m <= s <= !j /\ a[r] = (a at L1)[s]) &&
a[r] <= a[!j+1] };
'L2:
label L2 in
if !i <= k then find a !i n k;
assert { permut_sub (at a 'L2) a m (n+1) };
assert { forall r:int. m <= r < !i -> a[r] = (at a 'L2)[r] };
assert { permut_sub (a at L2) a m (n+1) };
assert { forall r:int. m <= r < !i -> a[r] = (a at L2)[r] };
assert { forall r:int. !i <= r <= n ->
(exists s:int. !i <= s <= n /\ a[r] = (at a 'L2)[s]) &&
(exists s:int. !i <= s <= n /\ a[r] = (a at L2)[s]) &&
a[r] >= a[!i-1] }
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