## VerifyThis 2018: le rouge et le noir

solution to VerifyThis 2018 challenge 2

**Authors:** Raphaël Rieu-Helft

**Topics:** Array Data Structure / Algorithms / Mathematics

**Tools:** Why3

**References:** VerifyThis @ ETAPS 2018 / Project Euler

see also the index (by topic, by tool, by reference, by year)

# VerifyThis @ ETAPS 2018 competition Challenge 2: Le rouge et le noir

Author: Raphaël Rieu-Helft (LRI, Université Paris Sud)

module ColoredTiles use int.Int use set.Fset use seq.Seq type color = Red | Black type coloring = seq color predicate tworedneighbors (c: coloring) (i:int) = ((c[i-2] = Red /\ c[i-1] = Red /\ 2 <= i) \/ (c[i-1] = Red /\ c[i+1] = Red /\ 1 <= i <= length c - 2) \/ (c[i+1] = Red /\ c[i+2] = Red /\ i <= length c - 3)) predicate valid (c:coloring) = forall i. 0 <= i < length c -> c[i] = Red -> tworedneighbors c i function black (_n:int) : color = Black function red (_n:int) : color = Red function colorings0 : fset coloring = add (create 0 black) Fset.empty function colorings1 : fset coloring = add (create 1 black) Fset.empty function colorings2 : fset coloring = add (create 2 black) Fset.empty function colorings3: fset coloring = add (create 3 red) (add (create 3 black) Fset.empty) lemma valid_contr: forall c i. valid c -> 0 <= i < length c -> not (tworedneighbors c i) -> c[i] = Black lemma colo_0 : forall c: coloring. length c = 0 -> (valid c <-> mem c colorings0 by Seq.(==) c (create 0 black)) lemma colo_1 : forall c: coloring. length c = 1 -> (valid c <-> mem c colorings1 by c[0] = Black so Seq.(==) c (create 1 black)) lemma colo_2 : forall c: coloring. length c = 2 -> (valid c <-> mem c colorings2 by c[0] = Black = c[1] so Seq.(==) c (create 2 black) so c = create 2 black) lemma colo_3 : forall c: coloring. length c = 3 -> (valid c <-> mem c colorings3 by if c[0] = Black then (c[0]=c[1]=c[2]=Black so c == create 3 black so c = create 3 black) else (c[0]=c[1]=c[2]=Red so c == create 3 red so c = create 3 red)) let lemma valid_split_fb (c:coloring) (k: int) requires { 3 <= k < length c } requires { forall i. 0 <= i < k -> c[i] = Red } requires { valid c[k+1 ..] } ensures { valid c } = let c' = c[k+1 ..] in assert { forall i. k+1 <= i < length c -> c[i] = Red -> (tworedneighbors c i by c'[i - (k+1)] = Red so [@case_split] tworedneighbors c' (i - (k+1))) } let lemma valid_restrict (c: coloring) (k: int) requires { valid c } requires { 0 <= k < length c } requires { c[k] = Black } ensures { valid c[k+1 ..] } = () (*1st black tile starting at i *) let rec function first_black_tile (c:coloring) : int ensures { 0 <= result <= length c } ensures { forall j. 0 <= j < result <= length c -> c[j] = Red } ensures { result < length c -> c[result] = Black } ensures { valid c -> result = 0 \/ 3 <= result } variant { length c } = if Seq.length c = 0 then 0 else match c[0] with | Black -> 0 | Red -> assert { valid c -> c[1]=Red /\ c[2] = Red }; let r = first_black_tile c[1 ..] in assert { forall j. 1 <= j < 1+r -> c[j] = Red by c[1 ..][j-1] = Red }; 1+r end let rec function addleft (nr:int) (c:coloring) : coloring variant { nr } ensures { nr >= 0 -> Seq.length result = Seq.length c + nr + 1 } = if nr <= 0 then cons Black c else cons Red (addleft (nr-1) c) (* add nr red tiles and a black tile to the left of each coloring *) function mapaddleft (s:fset coloring) (nr:int) : fset coloring = map (addleft nr) s lemma addleft_fb: forall c nr. 0 <= nr -> first_black_tile (addleft nr c) = nr lemma mapaddleft_fb: forall s c nr. 0 <= nr -> mem c (mapaddleft s nr) -> first_black_tile c = nr predicate reciprocal (f: 'a -> 'b) (g: 'b -> 'a) = forall y. g (f y) = y let lemma bij_image (u: fset 'a) (f: 'a -> 'b) (g: 'b -> 'a) requires { reciprocal f g } ensures { subset u (map g (map f u)) } = assert { forall x. mem x u -> mem (f x) (map f u) -> mem (g (f x)) (map g (map f u)) -> mem x (map g (map f u)) } let lemma bij_cardinal (u: fset 'a) (f: 'a -> 'b) (g: 'b -> 'a) requires { reciprocal f g } ensures { cardinal (map f u) = cardinal u } = assert { cardinal (map f u) <= cardinal u }; assert { cardinal (map g (map f u)) <= cardinal (map f u) }; assert { cardinal u <= cardinal (map g (map f u)) } function rmleft (nr:int) (c:coloring) : coloring = c[nr+1 ..] use seq.FreeMonoid lemma ext: forall c1 c2: coloring. Seq.(==) c1 c2 -> c1 = c2 lemma app_eq: forall c1 c2 c3 c4: coloring. c1 = c2 -> c3 = c4 -> c1 ++ c3 = c2 ++ c4 let rec lemma addleft_result (c:coloring) (nr:int) requires { 0 <= nr } ensures { addleft nr c = (Seq.create nr red) ++ (cons Black c) } variant { nr } = if nr = 0 then assert { addleft nr c = (Seq.create nr red) ++ (cons Black c) } else begin let cnr = create nr red in let cnrm = create (nr - 1) red in addleft_result c (nr-1); assert { addleft (nr-1) c = cnrm ++ cons Black c }; assert { cons Red cnrm = cnr by Seq.(==) (cons Red cnrm) cnr }; assert { addleft nr c = cnr ++ cons Black c by addleft nr c = cons Red (addleft (nr-1) c) = cons Red (cnrm ++ cons Black c) = (cons Red cnrm) ++ cons Black c = cnr ++ cons Black c } end let lemma addleft_bijective (nr:int) requires { 0 <= nr } ensures { reciprocal (addleft nr) (rmleft nr) } = assert { forall c i. 0 <= i < length c -> (rmleft nr (addleft nr c))[i] = c[i] }; assert { forall c. Seq.(==) (rmleft nr (addleft nr c)) c } let lemma mapaddleft_card (s: fset coloring) (nr: int) requires { 0 <= nr } ensures { cardinal (mapaddleft s nr) = cardinal s } = addleft_bijective nr; bij_cardinal s (addleft nr) (rmleft nr) let lemma addleft_valid (c:coloring) (nr:int) requires { nr = 0 \/ 3 <= nr } requires { valid c } ensures { valid (addleft nr c) } = addleft_result c nr; if nr = 0 then assert { valid (addleft 0 c) } else valid_split_fb (addleft nr c) nr let lemma mapaddleft_valid (s: fset coloring) (nr: int) requires { forall c. mem c s -> valid c } requires { nr = 0 \/ 3 <= nr } ensures { forall c. mem c (mapaddleft s nr) -> valid c } = assert { forall c. mem c (mapaddleft s nr) -> valid c by mem c (map (addleft nr) s) so (exists y. mem y s /\ c = addleft nr y) } let lemma mapaddleft_length (s: fset coloring) (nr: int) (l1 l2: int) requires { forall c. mem c s -> Seq.length c = l1 } requires { 0 <= nr } requires { l2 = l1 + nr + 1 } ensures { forall c. mem c (mapaddleft s nr) -> Seq.length c = l2 } = () let rec ghost disjoint_union (s1 s2: fset coloring) : fset coloring requires { forall x. mem x s1 -> not mem x s2 } ensures { result = union s1 s2 } ensures { cardinal result = cardinal s1 + cardinal s2 } variant { cardinal s1 } = if is_empty s1 then begin assert { union s1 s2 = s2 by (forall x. mem x (union s1 s2) -> mem x s1 \/ mem x s2 -> mem x s2) so subset (union s1 s2) s2 }; s2 end else let x = pick s1 in let s1' = remove x s1 in let s2' = add x s2 in let u = disjoint_union s1' s2' in assert { u = union s1 s2 by u = union s1' s2' so (forall y. (mem y s2' <-> (mem y s2 \/ y = x))) so (forall y. ((mem y s1' \/ y = x) <-> mem y s1)) so (forall y. mem y u <-> mem y s1' \/ mem y s2' <-> mem y s1' \/ mem y s2 \/ y = x <-> mem y s1 \/ mem y s2 <-> mem y (union s1 s2)) so (forall y. mem y u <-> mem y (union s1 s2)) so Fset.(==) u (union s1 s2)}; u use array.Array let enum () : (count: array int, ghost sets: array (fset coloring)) ensures { Array.length count = 51 = Array.length sets /\ (forall i. 0 <= i <= 50 -> (forall c: coloring. Seq.length c = i -> (valid c <-> mem c (sets[i])))) /\ (forall i. 0 <= i < 50 -> count[i] = cardinal (sets[i])) } = let count = Array.make 51 0 in let ghost sets : array (fset coloring) = Array.make 51 Fset.empty in count[0] <- 1; sets[0] <- colorings0; assert { forall c. ((Seq.length c = 0 /\ valid c) <-> mem c (sets[0])) }; count[1] <- 1; sets[1] <- colorings1; assert { forall i c. (i=0 \/ i=1) -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) }; count[2] <- 1; sets[2] <- colorings2; assert { forall i c. (i=0 \/ i=1 \/ i=2) -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) }; count[3] <- 2; sets[3] <- colorings3; assert { sets[3] = colorings3 }; assert { forall i c. (i=0 \/ i=1 \/ i=2 \/ i = 3) -> ((Seq.length c = i /\ valid c) <-> mem c (sets[i])) }; assert { cardinal colorings3 = 2 }; for n = 4 to 50 do invariant { forall c i. 0 <= i < n -> Seq.length c = i -> valid c -> mem c (sets[i]) } invariant { forall c i. 0 <= i < n -> mem c (sets[i]) -> (Seq.length c = i /\ valid c) } invariant { forall i. 0 <= i < n -> count[i] = cardinal (sets[i]) } label StartLoop in (* colorings with first_black_tile = 0 *) count[n] <- count[n-1]; mapaddleft_valid (sets[n-1]) 0; sets[n] <- mapaddleft (sets[n-1]) 0; assert { forall i. 0 <= i < n -> sets[i] = sets[i] at StartLoop }; assert { forall i. 0 <= i < n -> count[i] = count[i] at StartLoop }; assert { forall c. Seq.length c = n -> valid c -> first_black_tile c < 3 -> mem c sets[n] by first_black_tile c = 0 so valid c[1 ..] so mem c[1 ..] (sets[n-1]) so addleft 0 c[1 ..] = c so mem c (mapaddleft sets[n-1] 0) }; for k = 3 to n-1 do invariant { forall c i. 0 <= i < n -> Seq.length c = i -> valid c -> mem c (sets[i]) } invariant { forall c i. 0 <= i < n -> mem c (sets[i]) -> (Seq.length c = i /\ valid c) } invariant { forall i. 0 <= i < n -> count[i] = cardinal (sets[i]) } invariant { forall c. (mem c (sets[n]) <-> (Seq.length c = n /\ valid c /\ first_black_tile c < k)) } invariant { count[n] = cardinal (sets[n]) } label InnerLoop in (* colorings with first_black_tile = k *) count[n] <- count [n] + count [n-k-1]; mapaddleft_length (sets[n-k-1]) k (n-k-1) n; mapaddleft_valid (sets[n-k-1]) k; mapaddleft_card (sets[n-k-1]) k; let ghost ns = mapaddleft sets[n-k-1] k in assert { forall c. mem c ns -> first_black_tile c = k }; assert { forall c. Seq.length c = n -> valid c -> first_black_tile c = k -> mem c ns by valid c[k+1 ..] so mem c[k+1 ..] (sets[n-k-1]) so let c' = addleft k c[k+1 ..] in ((forall i. 0 <= i < n -> Seq.get c i = Seq.get c' i) by c[k+1 ..] = c'[k+1 ..]) so Seq.(==) c' c so c' = c so mem c (mapaddleft sets[n-k-1] k) }; sets[n] <- disjoint_union (sets[n]) ns; assert { forall i. 0 <= i < n -> sets[i] = sets[i] at InnerLoop }; assert { forall i. 0 <= i < n -> count[i] = count[i] at InnerLoop }; done; (* coloring with first_black_tile = n *) label LastAdd in let ghost r = Seq.create n red in let ghost sr = Fset.singleton r in assert { forall c. mem c sets[n] -> first_black_tile c < n }; assert { first_black_tile r = n }; assert { valid r /\ Seq.length r = n }; count[n] <- count[n]+1; sets[n] <- disjoint_union (sets[n]) sr; assert { forall c. mem c sets[n] -> valid c /\ Seq.length c = n by [@case_split] mem c (sets[n] at LastAdd) \/ mem c sr }; assert { forall c. Seq.length c = n -> first_black_tile c = n -> mem c sets[n] by (forall k. 0 <= k < n -> Seq.get c k = Red) so c == r so c = r }; assert { forall i. 0 <= i < n -> sets[i] = sets[i] at LastAdd }; assert { forall i. 0 <= i < n -> count[i] = count[i] at LastAdd }; done; count, sets end

download ZIP archive

# Why3 Proof Results for Project "verifythis_2018_le_rouge_et_le_noir_1"

## Theory "verifythis_2018_le_rouge_et_le_noir_1.ColoredTiles": fully verified

Obligations | Alt-Ergo 2.3.3 | CVC5 1.0.5 | Z3 4.12.2 | ||||||||

valid_contr | 0.01 | --- | --- | ||||||||

colo_0 | --- | --- | --- | ||||||||

split_vc | |||||||||||

colo_0.0 | 0.01 | --- | --- | ||||||||

colo_0.1 | 0.01 | --- | --- | ||||||||

colo_0.2 | --- | 0.08 | --- | ||||||||

colo_1 | --- | --- | --- | ||||||||

split_vc | |||||||||||

colo_1.0 | 0.01 | --- | --- | ||||||||

colo_1.1 | 0.01 | --- | --- | ||||||||

colo_1.2 | 0.02 | --- | --- | ||||||||

colo_1.3 | --- | 0.08 | --- | ||||||||

colo_2 | --- | --- | --- | ||||||||

split_vc | |||||||||||

colo_2.0 | 0.01 | --- | --- | ||||||||

colo_2.1 | 0.01 | --- | --- | ||||||||

colo_2.2 | 0.02 | --- | --- | ||||||||

colo_2.3 | 0.01 | --- | --- | ||||||||

colo_2.4 | 0.11 | --- | --- | ||||||||

colo_2.5 | --- | 0.09 | --- | ||||||||

colo_3 | --- | --- | --- | ||||||||

split_vc | |||||||||||

colo_3.0 | 0.01 | --- | --- | ||||||||

colo_3.1 | 0.01 | --- | --- | ||||||||

colo_3.2 | 0.01 | --- | --- | ||||||||

colo_3.3 | 0.01 | --- | --- | ||||||||

colo_3.4 | 0.01 | --- | --- | ||||||||

colo_3.5 | 0.01 | --- | --- | ||||||||

colo_3.6 | 0.12 | --- | --- | ||||||||

colo_3.7 | 0.01 | --- | --- | ||||||||

colo_3.8 | 0.17 | --- | --- | ||||||||

colo_3.9 | 0.02 | --- | --- | ||||||||

colo_3.10 | 0.30 | --- | --- | ||||||||

colo_3.11 | --- | 0.48 | --- | ||||||||

VC for valid_split_fb | --- | --- | --- | ||||||||

split_vc | |||||||||||

precondition | 0.01 | --- | --- | ||||||||

assertion | --- | --- | --- | ||||||||

split_vc | |||||||||||

assertion | 0.02 | --- | --- | ||||||||

VC for valid_split_fb | 0.02 | --- | --- | ||||||||

VC for valid_split_fb | 0.08 | --- | --- | ||||||||

postcondition | 0.12 | --- | --- | ||||||||

VC for valid_restrict | --- | --- | --- | ||||||||

split_vc | |||||||||||

postcondition | --- | --- | --- | ||||||||

split_all_full | |||||||||||

postcondition | 0.48 | --- | --- | ||||||||

VC for first_black_tile | --- | --- | --- | ||||||||

split_vc | |||||||||||

assertion | 0.02 | --- | --- | ||||||||

precondition | 0.01 | --- | --- | ||||||||

variant decrease | 0.01 | --- | --- | ||||||||

assertion | --- | --- | --- | ||||||||

split_vc | |||||||||||

assertion | 0.02 | --- | --- | ||||||||

VC for first_black_tile | 0.04 | --- | --- | ||||||||

postcondition | 0.02 | --- | --- | ||||||||

postcondition | 0.02 | --- | --- | ||||||||

postcondition | 0.04 | --- | --- | ||||||||

postcondition | 0.03 | --- | --- | ||||||||

VC for addleft | --- | --- | --- | ||||||||

split_vc | |||||||||||

variant decrease | 0.01 | --- | --- | ||||||||

postcondition | 0.01 | --- | --- | ||||||||

addleft_fb | --- | --- | --- | ||||||||

introduce_premises | |||||||||||

addleft_fb.0 | --- | --- | --- | ||||||||

induction nr | |||||||||||

base case | 0.02 | --- | --- | ||||||||

recursive case | --- | --- | --- | ||||||||

split_all_full | |||||||||||

recursive case | --- | --- | 0.05 | ||||||||

mapaddleft_fb | 0.02 | --- | --- | ||||||||

VC for bij_image | --- | --- | --- | ||||||||

split_vc | |||||||||||

assertion | 0.01 | --- | --- | ||||||||

postcondition | 0.02 | --- | --- | ||||||||

VC for bij_cardinal | --- | --- | --- | ||||||||

split_vc | |||||||||||

assertion | 0.01 | --- | --- | ||||||||

assertion | 0.01 | --- | --- | ||||||||

assertion | 0.02 | --- | --- | ||||||||

postcondition | 0.01 | --- | --- | ||||||||

ext | 0.01 | --- | --- | ||||||||

app_eq | 0.01 | --- | --- | ||||||||

VC for addleft_result | --- | --- | --- | ||||||||

split_vc | |||||||||||

assertion | 0.06 | --- | --- | ||||||||

precondition | 0.01 | --- | --- | ||||||||

precondition | 0.01 | --- | --- | ||||||||

variant decrease | 0.01 | --- | --- | ||||||||

precondition | 0.01 | --- | --- | ||||||||

assertion | --- | 0.10 | --- | ||||||||

assertion | --- | --- | --- | ||||||||

split_vc | |||||||||||

assertion | 2.00 | --- | --- | ||||||||

VC for addleft_result | 0.02 | --- | --- | ||||||||

assertion | 0.04 | --- | --- | ||||||||

postcondition | --- | 0.05 | --- | ||||||||

VC for addleft_bijective | --- | --- | --- | ||||||||

split_vc | |||||||||||

assertion | 0.25 | --- | --- | ||||||||

assertion | 0.07 | --- | --- | ||||||||

postcondition | 0.02 | --- | --- | ||||||||

VC for mapaddleft_card | --- | --- | --- | ||||||||

split_vc | |||||||||||

precondition | 0.01 | --- | --- | ||||||||

precondition | 0.01 | --- | --- | ||||||||

postcondition | 0.01 | --- | --- | ||||||||

VC for addleft_valid | --- | --- | --- | ||||||||

split_vc | |||||||||||

precondition | 0.01 | --- | --- | ||||||||

assertion | --- | 3.24 | --- | ||||||||

precondition | 0.02 | --- | --- | ||||||||

precondition | 0.02 | --- | --- | ||||||||

precondition | 0.12 | --- | --- | ||||||||

postcondition | 0.01 | --- | --- | ||||||||

VC for mapaddleft_valid | 0.06 | --- | --- | ||||||||

VC for mapaddleft_length | 0.03 | --- | --- | ||||||||

VC for disjoint_union | --- | --- | --- | ||||||||

split_vc | |||||||||||

assertion | 0.02 | --- | --- | ||||||||

variant decrease | 0.01 | --- | --- | ||||||||

precondition | 0.02 | --- | --- | ||||||||

assertion | --- | --- | --- | ||||||||

split_vc | |||||||||||

assertion | 0.01 | --- | --- | ||||||||

VC for disjoint_union | 0.02 | --- | --- | ||||||||

VC for disjoint_union | 0.02 | --- | --- | ||||||||

VC for disjoint_union | 0.02 | --- | --- | ||||||||

VC for disjoint_union | 0.01 | --- | --- | ||||||||

VC for disjoint_union | 0.02 | --- | --- | ||||||||

VC for disjoint_union | 0.02 | --- | --- | ||||||||

VC for disjoint_union | 0.01 | --- | --- | ||||||||

VC for disjoint_union | 0.01 | --- | --- | ||||||||

VC for disjoint_union | 0.01 | --- | --- | ||||||||

VC for disjoint_union | 0.01 | --- | --- | ||||||||

VC for disjoint_union | 0.03 | --- | --- | ||||||||

VC for disjoint_union | 0.01 | --- | --- | ||||||||

VC for disjoint_union | 0.01 | --- | --- | ||||||||

VC for disjoint_union | 0.01 | --- | --- | ||||||||

VC for disjoint_union | 0.02 | --- | --- | ||||||||

VC for disjoint_union | 0.02 | --- | --- | ||||||||

postcondition | 0.01 | --- | --- | ||||||||

postcondition | 0.05 | --- | --- | ||||||||

VC for enum | --- | --- | --- | ||||||||

split_vc | |||||||||||

array creation size | 0.01 | --- | --- | ||||||||

array creation size | 0.01 | --- | --- | ||||||||

index in array bounds | 0.01 | --- | --- | ||||||||

index in array bounds | 0.01 | --- | --- | ||||||||

assertion | 0.03 | --- | --- | ||||||||

index in array bounds | 0.01 | --- | --- | ||||||||

index in array bounds | 0.01 | --- | --- | ||||||||

assertion | 0.22 | --- | --- | ||||||||

index in array bounds | 0.01 | --- | --- | ||||||||

index in array bounds | 0.01 | --- | --- | ||||||||

assertion | --- | 0.30 | --- | ||||||||

index in array bounds | 0.02 | --- | --- | ||||||||

index in array bounds | 0.02 | --- | --- | ||||||||

assertion | --- | 0.19 | --- | ||||||||

assertion | --- | --- | --- | ||||||||

case i=3 | |||||||||||

true case (assertion) | --- | --- | --- | ||||||||

rewrite h | |||||||||||

true case (assertion) | --- | --- | --- | ||||||||

rewrite Assert | |||||||||||

true case (assertion) | --- | --- | --- | ||||||||

split_all_full | |||||||||||

VC for enum | --- | --- | --- | ||||||||

introduce_premises | |||||||||||

VC for enum | --- | --- | --- | ||||||||

apply colo_31 | |||||||||||

apply premises | 0.02 | --- | --- | ||||||||

apply premises | 0.02 | --- | --- | ||||||||

VC for enum | 0.10 | --- | --- | ||||||||

VC for enum | --- | --- | --- | ||||||||

introduce_premises | |||||||||||

VC for enum | --- | --- | --- | ||||||||

apply colo_3 | |||||||||||

apply premises | 0.10 | --- | --- | ||||||||

apply premises | --- | --- | --- | ||||||||

apply H | |||||||||||

false case (assertion) | 0.21 | --- | --- | ||||||||

assertion | 0.70 | --- | --- | ||||||||

loop invariant init | 0.04 | --- | --- | ||||||||

loop invariant init | 0.12 | --- | --- | ||||||||

loop invariant init | --- | --- | --- | ||||||||

assert (i=0\/i=1\/i=2\/i=3) | |||||||||||

asserted formula | 0.02 | --- | --- | ||||||||

loop invariant init | --- | --- | --- | ||||||||

revert h | |||||||||||

loop invariant init | --- | --- | --- | ||||||||

split_all_full | |||||||||||

loop invariant init | 0.48 | --- | --- | ||||||||

loop invariant init | 0.46 | --- | --- | ||||||||

loop invariant init | 0.45 | --- | --- | ||||||||

loop invariant init | --- | --- | --- | ||||||||

introduce_premises | |||||||||||

loop invariant init | --- | --- | --- | ||||||||

replace i 3 | |||||||||||

loop invariant init | --- | --- | --- | ||||||||

replace sets[3] colorings3 | |||||||||||

loop invariant init | --- | --- | --- | ||||||||

rewrite Assert | |||||||||||

loop invariant init | 0.04 | --- | --- | ||||||||

equality hypothesis | --- | 0.20 | --- | ||||||||

equality hypothesis | 0.03 | --- | --- | ||||||||

index in array bounds | 0.02 | --- | --- | ||||||||

index in array bounds | 0.02 | --- | --- | ||||||||

index in array bounds | 0.02 | --- | --- | ||||||||

precondition | 0.03 | --- | --- | ||||||||

precondition | 0.02 | --- | --- | ||||||||

index in array bounds | 0.02 | --- | --- | ||||||||

index in array bounds | 0.03 | --- | --- | ||||||||

assertion | 0.07 | --- | --- | ||||||||

assertion | 0.07 | --- | --- | ||||||||

assertion | --- | --- | --- | ||||||||

split_vc | |||||||||||

assertion | 0.05 | --- | --- | ||||||||

VC for enum | 0.05 | --- | --- | ||||||||

VC for enum | 0.31 | --- | --- | ||||||||

VC for enum | 0.05 | --- | --- | ||||||||

VC for enum | 0.14 | --- | --- | ||||||||

VC for enum | 0.05 | --- | --- | ||||||||

loop invariant init | 0.12 | --- | --- | ||||||||

loop invariant init | 0.06 | --- | --- | ||||||||

loop invariant init | 0.12 | --- | --- | ||||||||

loop invariant init | 1.23 | --- | --- | ||||||||

loop invariant init | 0.05 | --- | --- | ||||||||

index in array bounds | 0.03 | --- | --- | ||||||||

index in array bounds | 0.03 | --- | --- | ||||||||

index in array bounds | 0.03 | --- | --- | ||||||||

index in array bounds | 0.03 | --- | --- | ||||||||

precondition | 0.05 | --- | --- | ||||||||

precondition | 0.03 | --- | --- | ||||||||

precondition | 0.03 | --- | --- | ||||||||

index in array bounds | 0.03 | --- | --- | ||||||||

precondition | 0.05 | --- | --- | ||||||||

precondition | 0.03 | --- | --- | ||||||||

index in array bounds | 0.03 | --- | --- | ||||||||

precondition | 0.03 | --- | --- | ||||||||

index in array bounds | 0.04 | --- | --- | ||||||||

assertion | 0.05 | --- | --- | ||||||||

assertion | --- | --- | --- | ||||||||

split_vc | |||||||||||

assertion | 0.06 | --- | --- | ||||||||

VC for enum | 0.36 | --- | --- | ||||||||

VC for enum | 2.72 | --- | --- | ||||||||

VC for enum | --- | --- | --- | ||||||||

case i<k | |||||||||||

true case | 0.11 | --- | --- | ||||||||

false case | --- | --- | --- | ||||||||

case i=k | |||||||||||

false case (true case) | 0.19 | --- | --- | ||||||||

false case | --- | --- | --- | ||||||||

assert (get1 c i = get1 c[k+1 ..] (i-k-1)) | |||||||||||

asserted formula | 0.70 | --- | --- | ||||||||

false case | 0.74 | --- | --- | ||||||||

VC for enum | 0.62 | --- | --- | ||||||||

VC for enum | 0.05 | --- | --- | ||||||||

VC for enum | 0.18 | --- | --- | ||||||||

VC for enum | 0.04 | --- | --- | ||||||||

index in array bounds | 0.03 | --- | --- | ||||||||

precondition | 0.05 | --- | --- | ||||||||

index in array bounds | 0.04 | --- | --- | ||||||||

assertion | 0.08 | --- | --- | ||||||||

assertion | 0.09 | --- | --- | ||||||||

loop invariant preservation | 0.18 | --- | --- | ||||||||

loop invariant preservation | 0.16 | --- | --- | ||||||||

loop invariant preservation | 0.14 | --- | --- | ||||||||

loop invariant preservation | 0.34 | --- | --- | ||||||||

loop invariant preservation | 0.06 | --- | --- | ||||||||

precondition | 0.03 | --- | --- | ||||||||

assertion | 0.04 | --- | --- | ||||||||

assertion | 0.32 | --- | --- | ||||||||

assertion | --- | --- | --- | ||||||||

introduce_premises | |||||||||||

assertion | --- | --- | --- | ||||||||

inline_goal | |||||||||||

assertion | 0.34 | --- | --- | ||||||||

index in array bounds | 0.03 | --- | --- | ||||||||

index in array bounds | 0.03 | --- | --- | ||||||||

index in array bounds | 0.03 | --- | --- | ||||||||

precondition | 0.06 | --- | --- | ||||||||

index in array bounds | 0.04 | --- | --- | ||||||||

assertion | --- | --- | --- | ||||||||

split_vc | |||||||||||

assertion | 0.14 | --- | --- | ||||||||

VC for enum | 0.09 | --- | --- | ||||||||

VC for enum | 0.09 | --- | --- | ||||||||

assertion | --- | --- | --- | ||||||||

split_all_full | |||||||||||

VC for enum | 0.06 | --- | --- | ||||||||

VC for enum | 0.18 | --- | --- | ||||||||

VC for enum | 0.06 | --- | --- | ||||||||

VC for enum | 0.56 | --- | --- | ||||||||

assertion | 0.09 | --- | --- | ||||||||

assertion | 0.09 | --- | --- | ||||||||

loop invariant preservation | 0.43 | --- | --- | ||||||||

loop invariant preservation | 0.28 | --- | --- | ||||||||

loop invariant preservation | 0.29 | --- | --- | ||||||||

out of loop bounds | 0.03 | --- | --- | ||||||||

postcondition | 0.19 | --- | --- | ||||||||

VC for enum | 0.02 | --- | --- |