Commit 83f2b5d5 authored by François Bobot's avatar François Bobot

verifythis_PrefixSumRec: remove some assert, but many remains

parent 04d17bbf
......@@ -69,7 +69,7 @@ module PrefixSumRec
a0[i] = a0'[i]) ->
phase1 left right a0 a -> phase1 left right a0' a
(** First function *)
(** First function: modify partially the table and compute some intermediate partial sum *)
let rec upsweep (left:int) (right:int) (a : array int) : unit =
{ 0 <= left < right < a.length /\ -1 <= left - (right - left) /\ is_power_of_2 (right - left) }
'Init:
......@@ -80,8 +80,8 @@ module PrefixSumRec
upsweep (right - div space 2) right a;
assert { phase1 (left - div space 2) left (at a 'Init) a };
assert { phase1 (right - div space 2) right (at a 'Init) a };
assert { a[left] = sum (at a 'Init) (left-(right-left)+1) (left+1)};
assert { a[right] = sum (at a 'Init) (left+1) (right+1)}
assert { a[left] = sum (at a 'Init) (left-(right-left)+1) (left+1) };
assert { a[right] = sum (at a 'Init) (left+1) (right+1) }
end;
a[right] <- a[left] + a[right];
assert { right > left+1 -> phase1 (left - div space 2) left (at a 'Init) a };
......@@ -99,6 +99,8 @@ module PrefixSumRec
forall i : int. (left-(right-left)) < i <= right -> a[i] = sum a0 0 i
(** BUG of why3ml? a0 can't be set as ghost: vty_value mismatch *)
(** Second function: complete the partial using the remaining intial value and the partial
sum already computed *)
let rec downsweep (left:int) (right:int) ((*ghost*) a0 : array int) (a : array int) : unit =
{ 0 <= left < right < a.length /\ -1 <= left - (right - left) /\
is_power_of_2 (right - left) /\
......@@ -110,7 +112,6 @@ module PrefixSumRec
assert { a[right] = sum a0 0 (left-(right-left) + 1) };
assert { a[left] = sum a0 (left-(right-left)+1) (left+1) };
a[right] <- a[right] + a[left];
assert { a[right] = sum a0 0 (left + 1) };
a[left] <- tmp;
assert { a[right] = sum a0 0 (left + 1) };
if right > left+1 then
......@@ -120,7 +121,6 @@ module PrefixSumRec
assert { phase1 (go_right left right) right a0 (at a 'Init) };
assert { phase1 (go_right left right) right a0 a };
downsweep (left - div space 2) left a0 a;
assert { a[right] = sum a0 0 (left + 1) };
downsweep (right - div space 2) right a0 a;
assert { partial_sum (left - div space 2) left a0 a };
assert { partial_sum (right - div space 2) right a0 a }
......@@ -139,7 +139,7 @@ module PrefixSumRec
a[0] <- 3; a[1] <- 1; a[2] <- 7; a[3] <- 0; a[4] <- 4; a[5] <- 1;
a[6] <- 6; a[7] <- 3;
let a0 = copy a in (** TODO make it as ghost *)
assert { power 2 2 = 4 };
assert { power 2 2 = 4 }; (** for is_power_of_2 existential *)
upsweep 3 7 a;
a[7] <- 0;
downsweep 3 7 a0 a;
......
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