Commit b510ebc9 by Jean-Christophe Filliatre

### make it prettier

parent 83f2b5d5
 ... ... @@ -11,25 +11,25 @@ module PrefixSumRec use import int.ComputerDivision use import int.Power use import array.Array use import array.ArraySum use import array.Array use import array.ArraySum (** Shortcuts *) function go_left (left right:int) : int = let space = right - left in left - div space 2 let space = right - left in left - div space 2 lemma go_left_bounds: forall left right:int. 0 <= left /\ left + 1 < right /\ right - left <= left -> 0 <= go_left left right < left forall left right:int. 0 <= left /\ left + 1 < right /\ right - left <= left -> 0 <= go_left left right < left function go_right (left right:int) : int = let space = right - left in right - div space 2 let space = right - left in right - div space 2 lemma go_right_bounds: forall left right:int. 0 <= left /\ left + 1 < right /\ right - left <= left -> left <= go_right left right < right forall left right:int. 0 <= left /\ left + 1 < right /\ right - left <= left -> left <= go_right left right < right (** Needed for the proof of phase1_frame and phase1_frame2 *) lemma Div_mod_2: ... ... @@ -38,12 +38,16 @@ module PrefixSumRec (** The step must be a power of 2 *) predicate is_power_of_2 (x:int) = exists k:int. (k >= 0 /\ x = power 2 k) (** Needed for proving is_power_of_2_1. Can it be added to the theory Power? *) lemma is_power_of_2_0: forall k:int. k > 0 -> power 2 k = 2 * (power 2 (k-1)) lemma is_power_of_2_1: forall x:int. is_power_of_2 x -> x > 1 -> 2 * (div x 2) = x (** Needed for proving is_power_of_2_1. Can it be added to the theory Power? *) lemma is_power_of_2_0: forall k:int. k > 0 -> power 2 k = 2 * power 2 (k-1) lemma is_power_of_2_1: forall x:int. is_power_of_2 x -> x > 1 -> 2 * div x 2 = x (** Describe the result of the first function. The second function traverse the array in the same way than the first function so it can use the ind uctive . *) (** Describe the result of the first function. The second function traverses the array in the same way than the first function so it can use the inductive. *) inductive phase1 (left:int) (right:int) (a0: array int) (a: array int) = | Leaf : forall left right:int, a0 a : array int. right = left + 1 -> ... ... @@ -69,71 +73,64 @@ module PrefixSumRec a0[i] = a0'[i]) -> phase1 left right a0 a -> phase1 left right a0' a (** 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) } (** First function: modify partially the table and compute some intermediate partial sums *) let rec upsweep (left right: int) (a: array int) = { 0 <= left < right < a.length /\ -1 <= left - (right - left) /\ is_power_of_2 (right - left) } 'Init: let space = right - left in if right > left+1 then begin upsweep (left - div space 2) left a; 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) } end; a[right] <- a[left] + a[right]; assert { right > left+1 -> phase1 (left - div space 2) left (at a 'Init) a }; assert { right > left+1 -> phase1 (right - div space 2) right (at a 'Init) a } { let space = right - left in if right > left+1 then begin upsweep (left - div space 2) left a; 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) } end; a[right] <- a[left] + a[right]; assert { right > left+1 -> phase1 (left - div space 2) left (at a 'Init) a }; assert { right > left+1 -> phase1 (right - div space 2) right (at a 'Init) a } { let space = right - left in phase1 left right (old a) a /\ a[right] = sum (old a) (left-(right-left)+1) (right+1) /\ (forall i: int. i <= left-space -> a[i] = (old a)[i]) /\ (forall i: int. i > right -> a[i] = (old a)[i]) } (** What we really want to prove *) predicate partial_sum (left:int) (right:int) (a0 a : array int) = 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) /\ a[right] = sum a0 0 (left-(right-left) + 1) /\ phase1 left right a0 a } 'Init: let tmp = a[right] in 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]; a[left] <- tmp; assert { a[right] = sum a0 0 (left + 1) }; if right > left+1 then let space = right - left in begin assert { phase1 (go_left left right) left a0 (at a 'Init) }; 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; 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 } end; () { partial_sum left right a0 a /\ (forall i: int. i > right -> a[i] = (old a)[i]) } (** What we really want to prove *) predicate partial_sum (left:int) (right:int) (a0 a : array int) = forall i : int. (left-(right-left)) < i <= right -> a[i] = sum a0 0 i (** Second function: complete the partial using the remaining intial value and the partial sum already computed *) let rec downsweep (left right: int) (ghost a0 : array int) (a : array int) = { 0 <= left < right < a.length /\ -1 <= left - (right - left) /\ is_power_of_2 (right - left) /\ a[right] = sum a0 0 (left-(right-left) + 1) /\ phase1 left right a0 a } 'Init: let tmp = a[right] in 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]; a[left] <- tmp; assert { a[right] = sum a0 0 (left + 1) }; if right > left+1 then let space = right - left in assert { phase1 (go_left left right) left a0 (at a 'Init) }; 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; 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 } { partial_sum left right a0 a /\ (forall i: int. i <= left-(right-left) -> a[i] = (old a)[i]) /\ (forall i: int. i > right -> a[i] = (old a)[i]) } (forall i: int. i > right -> a[i] = (old a)[i]) } let main () :unit = {} let main () = let a = make 8 0 in 'Init: a[0] <- 3; a[1] <- 1; a[2] <- 7; a[3] <- 0; a[4] <- 4; a[5] <- 1; ... ... @@ -151,6 +148,5 @@ module PrefixSumRec assert { a[5] = 15 }; assert { a[6] = 16 }; assert { a[7] = 22 } {} end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!