## Hash tables with linear probing

**Authors:** Jean-Christophe Filliâtre / Martin Clochard

**Topics:** Array Data Structure / Data Structures

**Tools:** Why3

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

Hash tables using linear probing

Authors: Jean-Christophe Filliâtre (CNRS) Martin Clochard (École Normale Supérieure)

module HashedTypeWithDummy use int.Int type key type keym

the logic model of a key

function keym key: keym val predicate eq (x y: key) ensures { result <-> keym x = keym y } let predicate neq (x y: key) ensures { result <-> keym x <> keym y } = not (eq x y) val function hash key : int axiom hash_nonneg: forall k: key. 0 <= hash k axiom hash_eq: forall x y: key. eq x y -> hash x = hash y val constant dummy: key constant dummym: keym = keym dummy end module LinearProbing clone HashedTypeWithDummy with axiom . use int.Int use int.ComputerDivision use option.Option use list.Mem use map.Map use map.Const use ref.Ref use array.Array let function bucket (k: key) (n: int) : int requires { 0 < n } ensures { 0 <= result < n } = mod (hash k) n predicate between (l j r: int) = l <= j < r || r < l <= j || j < r < l

`j`

lies between `l`

and `r`

, cyclically

scope NumOfDummy use int.NumOf

number of dummy values in array `a`

between `l`

and `u`

function numof (a: array key) (l u: int) : int = NumOf.numof (fun i -> eq a[i] dummy) l u let rec lemma numof_eq (a1 a2: array key) (l u: int) : unit requires { 0 <= l <= u <= length a1 = length a2 } requires { forall i: int. l <= i < u -> eq a2[i] a1[i] } ensures { numof a2 l u = numof a1 l u } variant { u-l } = if l < u then numof_eq a1 a2 (l+1) u let rec lemma dummy_const (a: array key) (n: int) requires { 0 <= n } requires { forall i: int. 0 <= i < n -> a[i] = dummy } variant { n } ensures { numof a 0 n = n } = if n > 0 then dummy_const a (n-1) end function numofd (a: array key) (l u: int) : int = NumOfDummy.numof a l u let ghost numof_update (a1 a2: array key) (l i u: int) requires { 0 <= l <= i < u <= Array.length a1 = Array.length a2 } requires { forall j: int. l <= j < u -> j<>i -> a1[j] = a2[j] } requires { eq a1[i] dummy && neq a2[i] dummy } ensures { numofd a1 l u = 1 + numofd a2 l u } = assert { numofd a1 l u = numofd a1 l i + numofd a1 i u = numofd a1 l i + numofd a1 i (i+1) + numofd a1 (i+1) u }; assert { numofd a2 l u = numofd a2 l i + numofd a2 i u = numofd a2 l i + numofd a2 i (i+1) + numofd a2 (i+1) u } predicate valid (data: array key) (view: map keym bool) (loc : map keym int) = (* dummy not in the model *) not (Map.get view dummym) /\ (* any value in the array is in the model *) (forall i: int. 0 <= i < Array.length data -> let x = data[i] in neq x dummy -> Map.get view (keym x) /\ Map.get loc (keym x) = i) /\ (* any value in the model is in the array *) (let n = Array.length data in forall x: key. Map.get view (keym x) -> let i = Map.get loc (keym x) in 0 <= i < n && eq data[i] x && forall j: int. 0 <= j < n -> between (bucket x n) j i -> neq data[j] x /\ neq data[j] dummy) (* TODO ^^^^^^^^^^^^^^^^^^ is actually provable *) type t = { mutable size: int; (* total number of elements *) mutable data: array key; (* buckets *) ghost mutable view: map keym bool; (* pure model *) ghost mutable loc : map keym int; (* index where it is stored *) } (* at least one empty slot *) invariant { 0 <= size < length data } invariant { let n = Array.length data in size + numofd data 0 n = n } invariant { valid data view loc } let create (n: int) : t requires { 0 < n } ensures { forall x: key. not (Map.get result.view (keym x)) } = { size = 0; data = Array.make n dummy; view = Const.const false; loc = Const.const 0; } let clear (h: t) : unit writes { h.size, h.data.elts, h.view } ensures { h.size = 0 } ensures { forall x: key. not (Map.get h.view (keym x)) } = h.size <- 0; Array.fill h.data 0 (Array.length h.data) dummy; h.view <- Const.const false let function next (n i: int) : int = let i = i+1 in if i = n then 0 else i let find (a: array key) (x: key) : int requires { neq x dummy } requires { let n = Array.length a in 0 < n /\ numofd a 0 n > 0 } ensures { 0 <= result < Array.length a } ensures { eq a[result] dummy || eq a[result] x } ensures { forall j: int. 0 <= j < Array.length a -> between (bucket x (Array.length a)) j result -> neq a[j] x /\ neq a[j] dummy } = let n = Array.length a in let b = bucket x n in let rec find (i: int) : int requires { 0 <= i < n } requires { numofd a 0 n > 0 } requires { forall j: int. 0 <= j < n -> between b j i -> neq a[j] x /\ neq a[j] dummy } requires { if i >= b then numofd a b i = 0 else numofd a b n = numofd a 0 i = 0 } variant { if i >= b then n - i + b else b - i } ensures { 0 <= result < n } ensures { eq a[result] dummy || eq a[result] x } ensures { forall j: int. 0 <= j < n -> between b j result -> neq a[j] x /\ neq a[j] dummy } = if eq a[i] dummy || eq a[i] x then i else find (next n i) in find b let mem (h: t) (x: key) : bool requires { neq x dummy } ensures { result <-> Map.get h.view (keym x) } = neq h.data[find h.data x] dummy let resize (h: t) : unit writes { h.data, h.loc } ensures { Array.length h.data = 2 * old (Array.length h.data) } = let n = Array.length h.data in let n2 = 2 * n in let a = Array.make n2 dummy in let ghost l = ref (Const.const 0) in for i = 0 to n - 1 do invariant { numofd a 0 n2 = numofd h.data 0 i + n2 - i } invariant { forall j: int. 0 <= j < n2 -> neq a[j] dummy -> Map.get h.view (keym a[j]) /\ Map.get !l (keym a[j]) = j } invariant { forall x: key. Map.get h.view (keym x) -> let j = Map.get h.loc (keym x) in if j < i then let j2 = Map.get !l (keym x) in 0 <= j2 < n2 /\ eq a[j2] x /\ forall k: int. 0 <= k < n2 -> between (bucket x n2) k j2 -> neq a[k] x /\ neq a[k] dummy else forall j2: int. 0 <= j2 < n2 -> neq a[j2] x } let x = h.data[i] in if neq x dummy then begin label L in let j = find a x in assert { eq a[j] dummy }; a[j] <- x; assert { numofd a 0 (j+1) = numofd (a at L) 0 (j+1) - 1 }; l := Map.set !l (keym x) j end done; h.loc <- !l; h.data <- a let add (h: t) (x: key) : unit requires { neq x dummy } writes { h } ensures { h.view = Map.set (old h.view) (keym x) True } = begin ensures { h.size + 1 < Array.length h.data } if 2 * (h.size + 1) >= Array.length h.data then resize h end; let i = find h.data x in if eq h.data[i] dummy then begin label L in h.size <- h.size + 1; h.data[i] <- x; assert { numofd h.data 0 (i+1) = numofd (h.data at L) 0 (i+1) - 1 } end; ghost (h.view <- Map.set h.view (keym x) True); ghost (h.loc <- Map.set h.loc (keym x) i) let copy (h: t) : t ensures { result.view = h.view } = { size = h.size; data = Array.copy h.data; view = h.view; loc = h.loc; } let rec ghost find_dummy (a: array key) (s: int) (i: int) : int requires { 0 <= s < Array.length a } requires { 0 <= i < Array.length a } requires { i <> s } requires { if i >= s then numofd a i (Array.length a) + numofd a 0 s >= 1 else numofd a i s >= 1} requires { forall k: int. 0 <= k < Array.length a -> between s k i -> k<>s -> neq a[k] dummy } variant { if i >= s then Array.length a - i + s else s - i} ensures { 0 <= result < Array.length a } ensures { result <> s } ensures { eq a[result] dummy } ensures { forall k: int. 0 <= k < Array.length a -> between s k result -> k<>s -> neq a[k] dummy } = let n = Array.length a in if eq a[i] dummy then i else find_dummy a s (next n i) (* j is the hole just created by remove (see below) and this function restores the data structure invariant for elements to the right of j if needed, starting at index i *) let rec delete (a: array key) (ghost loc: ref (map keym int)) (ghost view: map keym bool) (ghost f0: int) (j i: int) : unit requires { 0 <= f0 < Array.length a } requires { 0 <= j < Array.length a } requires { 0 <= i < Array.length a } requires { j <> f0 } requires { eq a[j] dummy } requires { eq a[f0] dummy } requires { between j i f0 } requires { forall k: int. 0 <= k < Array.length a -> between i k f0 -> k<>i -> neq a[k] dummy } requires { not (Map.get view dummym) } requires { forall k: int. 0 <= k < Array.length a -> let x = a[k] in neq x dummy -> Map.get view (keym x) /\ Map.get !loc (keym x) = k } (* any value in the model is in the array *) requires { let n = Array.length a in forall x: key. Map.get view (keym x) -> let k = Map.get !loc (keym x) in 0 <= k < n && eq a[k] x && forall l: int. 0 <= l < n -> between (bucket x n) l k -> neq a[l] x /\ (neq a[l] dummy \/ l = j /\ between j i k) } variant { if i >= f0 then Array.length a - i + f0 else f0 - i } ensures { numofd a 0 (Array.length a) = numofd (old a) 0 (Array.length a) } ensures { valid a view !loc } = let n = Array.length a in let i = next n i in let xi = a[i] in if neq xi dummy then begin let r = bucket xi n in if j < r && r <= i || i < j && j < r || r <= i && i < j then (* the hash index r lies cyclically between j and i *) delete a loc view f0 j i else begin let ghost a1 = Array.copy a in ghost NumOfDummy.numof_eq a a1 0 n; (* the hole j lies cyclically between hash index r and i *) a[j] <- xi; ghost numof_update a1 a 0 j n; let ghost a2 = Array.copy a in ghost NumOfDummy.numof_eq a a2 0 n; ghost loc := Map.set !loc (keym xi) j; a[i] <- dummy; ghost numof_update a a2 0 i n; delete a loc view f0 i i end end let remove (h: t) (x: key) : unit requires { neq x dummy } ensures { h.view = Map.set (old h.view) (keym x) False } = let n = Array.length h.data in let j = find h.data x in if neq h.data[j] dummy then begin label L in h.data[j] <- dummy; assert { numofd h.data 0 (j+1) = numofd (h.data at L) 0 (j+1) + 1 }; ghost (h.view <- Map.set h.view (keym x) False); let l = ref h.loc in let f0 = find_dummy h.data j (next n j) in delete h.data l h.view f0 j j; ghost (h.loc <- !l); h.size <- h.size - 1; end end

download ZIP archive

# Why3 Proof Results for Project "linear_probing"

## Theory "linear_probing.HashedTypeWithDummy": fully verified

Obligations | Alt-Ergo 2.0.0 |

VC for neq | 0.00 |

## Theory "linear_probing.LinearProbing": fully verified

Obligations | Alt-Ergo 2.0.0 | Alt-Ergo 2.3.3 | CVC3 2.4.1 | CVC4 1.4 | CVC4 1.5 | CVC4 1.7 | Z3 4.5.0 | Z3 4.6.0 | Z3 4.8.6 | ||||||||

VC for bucket | 0.01 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

VC for numof_eq | --- | --- | --- | 4.55 | --- | --- | --- | --- | --- | ||||||||

VC for dummy_const | 0.22 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

VC for numof_update | 0.92 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

VC for t | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

exists 0 | |||||||||||||||||

t'vc.0 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

exists (make 1 dummy) | |||||||||||||||||

t'vc.0.0 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

exists (fun (_:keym1) -> False) | |||||||||||||||||

t'vc.0.0.0 | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

exists (fun (_:keym1) -> 0) | |||||||||||||||||

t'vc.0.0.0.0 | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | ||||||||

VC for create | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

VC for clear | 0.07 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

VC for find | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

split_goal_right | |||||||||||||||||

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

index in array bounds | 0.00 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

variant decrease | --- | --- | --- | --- | --- | --- | 0.12 | --- | --- | ||||||||

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

precondition | 0.00 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

precondition | 0.04 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

precondition | 0.32 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

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

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

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

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

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

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

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

postcondition | 0.00 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

VC for mem | --- | --- | --- | 2.08 | --- | --- | --- | --- | --- | ||||||||

VC for resize | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

split_goal_right | |||||||||||||||||

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

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

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

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

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

precondition | 0.00 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

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

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

assertion | --- | --- | --- | --- | --- | --- | 0.41 | --- | --- | ||||||||

loop invariant preservation | --- | --- | --- | --- | --- | --- | 0.52 | --- | --- | ||||||||

loop invariant preservation | Timeout (5s) | Timeout (1s) | --- | --- | --- | Timeout (1s) | 9.83 | --- | Timeout (1s) | ||||||||

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

split_goal_right | |||||||||||||||||

loop invariant preservation | --- | --- | 0.58 | --- | --- | --- | --- | --- | --- | ||||||||

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

remove real,tuple0,unit,ref,map,list,option,zero,one,(>),(>=),abs,div,mod,const,is_nil,mem,is_none,(!),hash,([]'),([<-]'),next,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,numof'def,Numof_bounds,Numof_append,Numof_left_no_add,Numof_left_add,Empty,Full,numof_increasing,numof_strictly_increasing,numof_change_any,numof_change_some,numof_change_equiv,is_nil'spec,is_none'spec,neq'spec,hash_nonneg,hash_eq,array'invariant,([<-])'spec,make_spec,bucket'spec,bucket'def,numof_eq,dummy_const | |||||||||||||||||

loop invariant preservation | --- | --- | --- | --- | --- | --- | --- | 0.02 | --- | ||||||||

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

remove real,tuple0,unit,ref,map,list,option,zero,one,(>),(>=),abs,div,mod,const,is_nil,mem,is_none,(!),hash,([]'),([<-]'),next,Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,numof'def,Numof_bounds,Numof_append,Numof_left_no_add,Numof_left_add,Empty,Full,numof_increasing,numof_strictly_increasing,numof_change_any,numof_change_some,numof_change_equiv,is_nil'spec,is_none'spec,neq'spec,hash_nonneg,hash_eq,array'invariant,([<-])'spec,make_spec,bucket'spec,bucket'def,numof_eq,dummy_const | |||||||||||||||||

loop invariant preservation | --- | --- | --- | --- | --- | --- | --- | 0.02 | --- | ||||||||

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

remove zero,one,(-),(>),(<=),(>=),abs,get,set,([]'),([<-]'),const,(!),is_nil,mem,is_none,([]),numof,numofd,next,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,numof'def,Numof_bounds,Numof_append,Numof_left_no_add,Numof_left_add,Empty,Full,numof_increasing,numof_strictly_increasing,numof_change_any,numof_change_some,numof_change_equiv,is_nil'spec,is_none'spec,eq'spec,hash_nonneg,hash_eq,array'invariant,([<-])'spec,make_spec,bucket'spec,bucket'def,numof_eq,dummy_const | |||||||||||||||||

loop invariant preservation | --- | --- | --- | --- | --- | --- | 0.02 | --- | --- | ||||||||

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

remove zero,one,(-),(>),(<=),(>=),abs,get,set,([]'),([<-]'),const,(!),is_nil,mem,is_none,neq,dummym,between,numof,numofd,next,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,Abs_le,Abs_pos,Div_bound,Mod_bound,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Rounds_toward_zero,Div_1,Mod_1,Div_inf,Mod_inf,Div_mult,Mod_mult,numof'def,Numof_bounds,Numof_append,Numof_left_no_add,Numof_left_add,Empty,Full,numof_increasing,numof_strictly_increasing,numof_change_any,numof_change_some,numof_change_equiv,is_nil'spec,is_none'spec,neq'spec,array'invariant,([<-])'spec,make_spec,bucket'spec,numof_eq,dummy_const | |||||||||||||||||

loop invariant preservation | --- | --- | 0.13 | --- | --- | --- | --- | --- | --- | ||||||||

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

loop invariant preservation | 0.02 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

loop invariant preservation | --- | --- | --- | --- | --- | --- | 0.02 | --- | --- | ||||||||

loop invariant preservation | --- | --- | --- | --- | --- | --- | 0.10 | --- | --- | ||||||||

type invariant | --- | --- | --- | --- | 0.04 | --- | --- | --- | --- | ||||||||

type invariant | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | ||||||||

type invariant | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

split_goal_right | |||||||||||||||||

type invariant | --- | --- | 0.06 | --- | --- | --- | --- | --- | --- | ||||||||

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

out of loop bounds | 0.01 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

VC for add | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

split_goal_right | |||||||||||||||||

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

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

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

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

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

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

assertion | --- | --- | --- | --- | --- | --- | 0.18 | --- | --- | ||||||||

type invariant | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | ||||||||

type invariant | --- | --- | --- | --- | --- | --- | --- | 0.19 | --- | ||||||||

type invariant | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

split_goal_right | |||||||||||||||||

type invariant | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

unfold valid | |||||||||||||||||

VC for add | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

split_goal_right | |||||||||||||||||

VC for add | --- | --- | --- | --- | 0.08 | --- | --- | --- | --- | ||||||||

VC for add | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

inline_all | |||||||||||||||||

VC for add | --- | --- | --- | --- | 0.16 | --- | --- | --- | --- | ||||||||

VC for add | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

VC for add | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

subst_all | |||||||||||||||||

VC for add | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

case (i=i1) | |||||||||||||||||

true case | 0.03 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

inline_all | |||||||||||||||||

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

VC for add | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

VC for add | --- | --- | --- | --- | --- | --- | --- | 0.96 | --- | ||||||||

VC for add | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

VC for add | --- | --- | --- | --- | --- | --- | --- | 1.12 | --- | ||||||||

VC for add | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

inline_all | |||||||||||||||||

VC for add | --- | --- | --- | --- | --- | --- | --- | 0.56 | --- | ||||||||

VC for add | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

inline_all | |||||||||||||||||

VC for add | --- | --- | --- | --- | --- | --- | --- | 0.19 | --- | ||||||||

VC for add | --- | --- | --- | --- | 0.20 | --- | --- | --- | --- | ||||||||

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

type invariant | --- | --- | --- | --- | 0.05 | --- | --- | --- | --- | ||||||||

type invariant | --- | --- | --- | --- | 0.06 | --- | --- | --- | --- | ||||||||

type invariant | --- | --- | --- | --- | 0.11 | --- | --- | --- | --- | ||||||||

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

VC for copy | --- | --- | --- | 2.37 | --- | --- | --- | --- | --- | ||||||||

VC for find_dummy | 1.02 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

VC for delete | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

split_goal_right | |||||||||||||||||

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

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

variant decrease | 0.03 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

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

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

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

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

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

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

precondition | 0.10 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

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

precondition | 4.84 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

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

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

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

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

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

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

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

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

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

index in array bounds | 0.06 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

precondition | 0.08 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

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

variant decrease | 0.22 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

precondition | 0.08 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

precondition | 0.08 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

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

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

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

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

precondition | --- | --- | --- | --- | --- | --- | 0.27 | --- | --- | ||||||||

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

precondition | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

split_goal_right | |||||||||||||||||

precondition | --- | --- | 0.61 | --- | --- | --- | --- | --- | --- | ||||||||

precondition | --- | --- | 0.90 | --- | --- | --- | --- | --- | --- | ||||||||

precondition | --- | --- | --- | --- | 0.15 | --- | --- | --- | --- | ||||||||

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

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

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

postcondition | --- | --- | --- | 0.13 | --- | --- | 0.15 | --- | --- | ||||||||

VC for remove | --- | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

split_goal_right | |||||||||||||||||

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

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

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

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

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

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

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

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

precondition | --- | --- | --- | --- | --- | --- | 0.28 | --- | --- | ||||||||

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

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

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

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

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

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

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

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

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

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

precondition | --- | --- | --- | --- | 0.15 | --- | --- | --- | --- | ||||||||

precondition | 6.62 | --- | --- | --- | --- | --- | --- | --- | --- | ||||||||

type invariant | --- | --- | --- | --- | 0.56 | --- | --- | --- | --- | ||||||||

type invariant | --- | --- | --- | --- | --- | --- | --- | 0.32 | --- | ||||||||

type invariant | --- | --- | --- | --- | --- | --- | 0.02 | --- | --- | ||||||||

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

postcondition | --- | --- | --- | 0.16 | --- | --- | 0.46 | --- | --- |