Commit ba6fd292 authored by Andrei Paskevich's avatar Andrei Paskevich

repair algo63, algo64, and alg065

parent 8da1605f
This source diff could not be displayed because it is too large. You can view the blob instead.
...@@ -21,12 +21,12 @@ module Algo64 ...@@ -21,12 +21,12 @@ module Algo64
(* Algorithm 63 *) (* Algorithm 63 *)
val partition (a:array int) (m:int) (n:int) (i:ref int) (j:ref int) : unit val partition (a:array int) (m n:int) (i j:ref int) : unit
requires { 0 <= m < n < length a } requires { 0 <= m < n < length a }
writes {a,i,j} writes { a, i, j}
ensures { m <= !j < !i <= n } ensures { m <= !j < !i <= n }
ensures { permut_sub (old a) a m (n+1) } ensures { permut_sub (old a) a m (n+1) }
ensures { ensures {
exists x:int. exists x:int.
(forall r:int. m <= r <= !j -> a[r] <= x) /\ (forall r:int. m <= r <= !j -> a[r] <= x) /\
(forall r:int. !j < r < !i -> a[r] = x) /\ (forall r:int. !j < r < !i -> a[r] = x) /\
...@@ -34,19 +34,37 @@ module Algo64 ...@@ -34,19 +34,37 @@ module Algo64
(* Algorithm 64 *) (* Algorithm 64 *)
let rec quicksort (a:array int) (m:int) (n:int) : unit variant { n-m } = let rec quicksort (a:array int) (m n:int) : unit
requires { 0 <= m <= n < length a } requires { 0 <= m <= n < length a }
variant { n - m }
ensures { permut_sub (old a) a m (n+1) } ensures { permut_sub (old a) a m (n+1) }
ensures { sorted_sub a m (n+1) } ensures { sorted_sub a m (n+1) }
'Init: = if m < n then begin
if m < n then begin
let i = ref 0 in let i = ref 0 in
let j = ref 0 in let j = ref 0 in
partition a m n i j; partition a m n i j;
'L1: quicksort a m !j; 'L1: quicksort a m !j;
assert { permut_sub (at a 'L1) a m (n+1) }; assert { permut_sub (at a 'L1) a m (n+1) };
assert { forall r:int. !j < r <= n -> a[r] = (at a 'L1)[r] };
assert { forall r:int. m <= r <= !j ->
(exists s:int. m <= s <= !j /\ a[r] = (at a 'L1)[s]) &&
a[r] <= a[!j+1] };
'L2: quicksort a !i n; 'L2: quicksort a !i n;
assert { permut_sub (at a 'L2) a m (n+1) } assert { permut_sub (at a 'L2) a m (n+1) };
assert { forall r:int. m <= r < !i -> a[r] = (at a 'L2)[r] };
assert { forall r:int. !i <= r <= n ->
(exists s:int. !i <= s <= n /\ a[r] = (at a 'L2)[s]) &&
a[r] >= a[!i-1] };
assert {
forall r s:int. m <= r <= s <= n ->
if r <= !j then
if s <= !j then "a" a[r] <= a[s] else
if s < !i then "b" a[r] <= a[s] else
"c" a[r] <= a[s] else
if r < !i then
if s < !i then "d" a[r] <= a[s] else
"e" a[r] <= a[s] else
"f" a[r] <= a[s] }
end end
let qs (a:array int) : unit let qs (a:array int) : unit
......
This diff is collapsed.
...@@ -20,9 +20,9 @@ module Algo65 ...@@ -20,9 +20,9 @@ module Algo65
(* algorithm 63 *) (* algorithm 63 *)
val partition (a:array int) (m:int) (n:int) (i:ref int) (j:ref int) : unit val partition (a:array int) (m n:int) (i j:ref int) : unit
requires { 0 <= m < n < length a } requires { 0 <= m < n < length a }
writes {a,i,j} writes { a, i, j }
ensures { m <= !j < !i <= n } ensures { m <= !j < !i <= n }
ensures { permut_sub (old a) a m (n+1) } ensures { permut_sub (old a) a m (n+1) }
ensures { ensures {
...@@ -33,21 +33,30 @@ module Algo65 ...@@ -33,21 +33,30 @@ module Algo65
(* Algorithm 65 (fixed version) *) (* Algorithm 65 (fixed version) *)
let rec find (a:array int) (m:int) (n:int) (k:int) : unit variant { n-m } = let rec find (a:array int) (m n:int) (k:int) : unit
requires { 0 <= m <= k <= n < length a } requires { 0 <= m <= k <= n < length a }
variant { n - m }
ensures { permut_sub (old a) a m (n+1) } ensures { permut_sub (old a) a m (n+1) }
ensures { forall r:int. m <= r <= k -> a[r] <= a[k] } ensures { forall r:int. m <= r <= k -> a[r] <= a[k] }
ensures { forall r:int. k <= r <= n -> a[k] <= a[r] } ensures { forall r:int. k <= r <= n -> a[k] <= a[r] }
if m < n then begin = if m < n then begin
let i = ref 0 in let i = ref 0 in
let j = ref 0 in let j = ref 0 in
'L1:
partition a m n i j; partition a m n i j;
'L1:
if k <= !j then find a m !j k;
assert { permut_sub (at a 'L1) a m (n+1) }; assert { permut_sub (at a 'L1) a m (n+1) };
assert { forall r:int. !j < r <= n -> a[r] = (at a 'L1)[r] };
assert { forall r:int. m <= r <= !j ->
(exists s:int. m <= s <= !j /\ a[r] = (at a 'L1)[s]) &&
a[r] <= a[!j+1] };
'L2: 'L2:
if k <= !j then find a m !j k; if !i <= k then find a !i n k;
assert { permut_sub (at a 'L2) a m (n+1) }; assert { permut_sub (at a 'L2) a m (n+1) };
if !i <= k then find a !i n k assert { forall r:int. m <= r < !i -> a[r] = (at a 'L2)[r] };
assert { forall r:int. !i <= r <= n ->
(exists s:int. !i <= s <= n /\ a[r] = (at a 'L2)[s]) &&
a[r] >= a[!i-1] }
end end
end end
This diff is collapsed.
This diff is collapsed.
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