## 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 import int.Int type key type keym

the logic model of a key

function keym key: keym predicate eq (x y: key) = keym x = keym y val eq (x y: key) : bool ensures { result <-> eq x y } predicate neq (x y: key) = keym x <> keym y let neq (x y: key) : bool ensures { result <-> neq x y } = not (eq x y) 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 constant dummy: key constant dummym: keym = keym dummy end module LinearProbing clone import HashedTypeWithDummy use import int.Int use import int.ComputerDivision use import option.Option use import list.Mem use import map.Map use map.Const use import ref.Ref use import array.Array function bucket (k: key) (n: int) : int = mod (hash k) n lemma bucket_bounds: forall n: int. 0 < n -> forall k: key. 0 <= bucket k n < n

j lies between l and r, cyclically

predicate between (l j r: int) = l <= j < r || r < l <= j || j < r < l

number of dummy values in array `a`

between `l`

and `u`

namespace NumOfDummy use int.NumOf function numof (a: array key) (l u: int) : int = NumOf.numof (\ 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 <= self.size < length self.data } invariant { let n = Array.length self.data in self.size + numofd self.data 0 n = n } invariant { valid self.data self.view self.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 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 'L: let j = find a x in assert { eq a[j] dummy }; a[j] <- x; assert { numofd a 0 (j+1) = numofd (at a '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.size, h.data, h.data.elts, h.view, h.loc } ensures { h.view = Map.set (old h.view) (keym x) True } = abstract 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 'L: h.size <- h.size + 1; h.data[i] <- x; assert { numofd h.data 0 (i+1) = numofd (at h.data '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 'L: h.data[j] <- dummy; assert { numofd h.data 0 (j+1) = numofd (at h.data '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 in 0.01 s

Obligations | Alt-Ergo (0.99.1) |

1. VC for neq | 0.01 |

## Theory "linear_probing.LinearProbing": fully verified in 0.02 s

Obligations | Alt-Ergo (0.99.1) | CVC3 (2.4.1) | CVC4 (1.4) | Z3 (4.3.2) | ||||

bucket_bounds | 0.02 | --- | --- | --- | ||||

2. VC for numof_eq | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. variant decrease | 0.01 | --- | --- | --- | ||||

2. precondition | 0.02 | --- | --- | --- | ||||

3. precondition | 0.02 | --- | --- | --- | ||||

4. postcondition | --- | --- | --- | 0.06 | ||||

5. postcondition | --- | --- | --- | 0.04 | ||||

3. VC for dummy_const | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. variant decrease | 0.02 | --- | --- | --- | ||||

2. precondition | 0.02 | --- | --- | --- | ||||

3. precondition | 0.01 | --- | --- | --- | ||||

4. postcondition | --- | --- | --- | 0.01 | ||||

5. postcondition | 0.01 | --- | --- | --- | ||||

4. VC for numof_update | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. assertion | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. VC for numof_update | 0.06 | --- | --- | --- | ||||

2. VC for numof_update | --- | --- | 0.04 | --- | ||||

2. assertion | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. VC for numof_update | 0.05 | --- | --- | --- | ||||

2. VC for numof_update | --- | --- | 0.06 | --- | ||||

3. postcondition | --- | --- | --- | 0.36 | ||||

5. VC for create | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. array creation size | 0.02 | --- | --- | --- | ||||

2. type invariant | 0.02 | --- | --- | --- | ||||

3. type invariant | --- | --- | --- | 0.02 | ||||

4. type invariant | 0.02 | --- | --- | --- | ||||

5. postcondition | 0.02 | --- | --- | --- | ||||

6. VC for clear | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. precondition | 0.01 | --- | --- | --- | ||||

2. type invariant | 0.02 | --- | --- | --- | ||||

3. type invariant | --- | --- | --- | 0.02 | ||||

4. type invariant | 0.04 | --- | --- | --- | ||||

5. type invariant | 0.02 | --- | --- | --- | ||||

6. postcondition | 0.02 | --- | --- | --- | ||||

7. postcondition | 0.02 | --- | --- | --- | ||||

7. VC for find | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. index in array bounds | 0.03 | --- | --- | --- | ||||

2. postcondition | 0.02 | --- | --- | --- | ||||

3. postcondition | 0.04 | --- | --- | --- | ||||

4. postcondition | 0.02 | --- | --- | --- | ||||

5. index in array bounds | 0.01 | --- | --- | --- | ||||

6. postcondition | 0.01 | --- | --- | --- | ||||

7. postcondition | 0.02 | --- | --- | --- | ||||

8. postcondition | 0.02 | --- | --- | --- | ||||

9. variant decrease | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. VC for find | 0.04 | --- | --- | --- | ||||

2. VC for find | --- | --- | --- | 0.50 | ||||

10. precondition | 0.02 | --- | --- | --- | ||||

11. precondition | 0.02 | --- | --- | --- | ||||

12. precondition | 0.06 | --- | --- | --- | ||||

13. precondition | --- | --- | --- | 0.01 | ||||

14. postcondition | 0.01 | --- | --- | --- | ||||

15. postcondition | 0.03 | --- | --- | --- | ||||

16. postcondition | 0.02 | --- | --- | --- | ||||

17. precondition | 0.02 | --- | --- | --- | ||||

18. precondition | 0.03 | --- | --- | --- | ||||

19. precondition | 0.02 | --- | --- | --- | ||||

20. precondition | --- | --- | --- | 0.09 | ||||

21. postcondition | 0.03 | --- | --- | --- | ||||

22. postcondition | 0.01 | --- | --- | --- | ||||

23. postcondition | 0.03 | --- | --- | --- | ||||

8. VC for mem | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. precondition | 0.03 | --- | --- | --- | ||||

2. precondition | 0.02 | --- | --- | --- | ||||

3. index in array bounds | 0.02 | --- | --- | --- | ||||

4. postcondition | --- | 0.29 | --- | --- | ||||

9. VC for resize | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. array creation size | 0.02 | --- | --- | --- | ||||

2. type invariant | 0.02 | --- | --- | --- | ||||

3. type invariant | 0.03 | --- | --- | --- | ||||

4. type invariant | 0.02 | --- | --- | --- | ||||

5. type invariant | 0.01 | --- | --- | --- | ||||

6. postcondition | 0.02 | --- | --- | --- | ||||

7. loop invariant init | 0.04 | --- | --- | --- | ||||

8. loop invariant init | 0.03 | --- | --- | --- | ||||

9. loop invariant init | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. loop invariant init | 0.04 | --- | --- | --- | ||||

2. loop invariant init | 0.02 | --- | --- | --- | ||||

3. loop invariant init | --- | --- | --- | 0.02 | ||||

4. loop invariant init | 0.02 | --- | --- | --- | ||||

5. loop invariant init | --- | --- | --- | 0.02 | ||||

6. loop invariant init | 0.02 | --- | --- | --- | ||||

10. index in array bounds | 0.03 | --- | --- | --- | ||||

11. type invariant | 0.03 | --- | --- | --- | ||||

12. precondition | 0.02 | --- | --- | --- | ||||

13. precondition | 0.03 | --- | --- | --- | ||||

14. assertion | --- | --- | --- | 0.14 | ||||

15. index in array bounds | 0.03 | --- | --- | --- | ||||

16. assertion | --- | --- | --- | 0.10 | ||||

17. loop invariant preservation | --- | --- | --- | 0.22 | ||||

18. loop invariant preservation | --- | 0.09 | --- | --- | ||||

19. loop invariant preservation | --- | 0.26 | --- | --- | ||||

20. loop invariant preservation | --- | --- | --- | 0.02 | ||||

21. loop invariant preservation | 0.03 | --- | --- | --- | ||||

22. loop invariant preservation | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. loop invariant preservation | --- | --- | --- | 0.02 | ||||

2. loop invariant preservation | --- | --- | --- | 0.02 | ||||

3. loop invariant preservation | --- | --- | --- | 0.02 | ||||

4. loop invariant preservation | --- | --- | --- | 0.17 | ||||

5. loop invariant preservation | --- | --- | --- | 0.16 | ||||

6. loop invariant preservation | --- | --- | --- | 0.06 | ||||

23. type invariant | 0.02 | --- | --- | --- | ||||

24. type invariant | 0.02 | --- | --- | --- | ||||

25. type invariant | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. type invariant | --- | --- | --- | --- | ||||

inline_goal | ||||||||

1. type invariant | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. VC for resize | 0.02 | --- | 0.03 | 0.01 | ||||

2. VC for resize | --- | --- | 0.08 | --- | ||||

3. VC for resize | --- | --- | 0.08 | --- | ||||

4. VC for resize | --- | --- | --- | 0.03 | ||||

5. VC for resize | --- | --- | --- | 0.02 | ||||

6. VC for resize | --- | --- | --- | 0.03 | ||||

7. VC for resize | 0.49 | --- | 0.10 | --- | ||||

8. VC for resize | --- | --- | 0.27 | --- | ||||

26. type invariant | 0.03 | --- | --- | --- | ||||

27. postcondition | 0.02 | --- | --- | --- | ||||

10. VC for add | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. VC for add | 0.01 | --- | --- | --- | ||||

2. VC for add | 0.02 | --- | --- | --- | ||||

3. precondition | 0.03 | --- | --- | 0.02 | ||||

4. precondition | 0.02 | --- | --- | --- | ||||

5. index in array bounds | 0.02 | --- | --- | --- | ||||

6. index in array bounds | 0.02 | --- | --- | --- | ||||

7. assertion | --- | --- | --- | 0.20 | ||||

8. type invariant | 0.02 | --- | --- | --- | ||||

9. type invariant | --- | --- | --- | 0.09 | ||||

10. type invariant | --- | --- | --- | --- | ||||

inline_goal | ||||||||

1. type invariant | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. VC for add | 0.04 | --- | --- | --- | ||||

2. VC for add | --- | --- | 1.08 | 0.65 | ||||

3. VC for add | --- | --- | --- | 0.69 | ||||

4. VC for add | --- | --- | --- | 0.28 | ||||

5. VC for add | --- | --- | --- | 0.21 | ||||

6. VC for add | --- | --- | --- | 0.54 | ||||

7. VC for add | --- | --- | 0.84 | --- | ||||

8. VC for add | --- | --- | --- | 0.94 | ||||

11. type invariant | 0.02 | --- | --- | --- | ||||

12. postcondition | 0.04 | --- | --- | --- | ||||

13. type invariant | 0.02 | --- | --- | --- | ||||

14. type invariant | --- | --- | --- | 0.09 | ||||

15. type invariant | --- | --- | --- | 0.26 | ||||

16. postcondition | 0.04 | --- | --- | --- | ||||

11. VC for copy | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. type invariant | --- | --- | --- | 0.02 | ||||

2. type invariant | --- | --- | --- | --- | ||||

3. type invariant | --- | --- | --- | 1.49 | ||||

12. VC for find_dummy | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. index in array bounds | 0.02 | --- | --- | --- | ||||

2. postcondition | 0.02 | --- | --- | --- | ||||

3. postcondition | 0.02 | --- | --- | --- | ||||

4. postcondition | 0.03 | --- | --- | --- | ||||

5. postcondition | 0.01 | --- | --- | --- | ||||

6. variant decrease | 0.08 | --- | --- | --- | ||||

7. precondition | 0.01 | --- | --- | --- | ||||

8. precondition | 0.03 | --- | --- | --- | ||||

9. precondition | 0.04 | --- | --- | --- | ||||

10. precondition | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. VC for find_dummy | 0.40 | --- | --- | --- | ||||

2. VC for find_dummy | --- | 0.05 | --- | 0.03 | ||||

11. precondition | 0.02 | --- | --- | --- | ||||

12. postcondition | 0.02 | --- | --- | --- | ||||

13. postcondition | 0.02 | --- | --- | --- | ||||

14. postcondition | 0.02 | --- | --- | --- | ||||

15. postcondition | 0.03 | --- | --- | --- | ||||

13. VC for delete | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. index in array bounds | 0.02 | --- | --- | 0.01 | ||||

2. variant decrease | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. VC for delete | 0.02 | --- | --- | --- | ||||

2. VC for delete | 0.07 | --- | --- | --- | ||||

3. precondition | 0.02 | --- | --- | 0.01 | ||||

4. precondition | 0.03 | --- | --- | 0.01 | ||||

5. precondition | 0.02 | --- | --- | 0.01 | ||||

6. precondition | 0.03 | --- | --- | --- | ||||

7. precondition | --- | --- | --- | 0.02 | ||||

8. precondition | 0.04 | --- | --- | --- | ||||

9. precondition | 0.06 | --- | --- | --- | ||||

10. precondition | --- | --- | --- | --- | ||||

inline_goal | ||||||||

1. precondition | 0.36 | --- | --- | --- | ||||

11. precondition | 0.02 | --- | --- | --- | ||||

12. precondition | 0.02 | --- | --- | 0.01 | ||||

13. precondition | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. precondition | --- | --- | --- | 0.02 | ||||

2. precondition | --- | --- | --- | 0.02 | ||||

3. precondition | 0.01 | --- | --- | --- | ||||

4. precondition | 0.14 | --- | --- | --- | ||||

5. precondition | --- | --- | --- | 0.02 | ||||

14. postcondition | 0.10 | --- | --- | --- | ||||

15. postcondition | 0.02 | --- | --- | --- | ||||

16. precondition | 0.06 | --- | --- | --- | ||||

17. precondition | 0.03 | --- | --- | 0.01 | ||||

18. index in array bounds | 0.02 | --- | --- | 0.02 | ||||

19. precondition | 0.04 | --- | --- | --- | ||||

20. precondition | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. precondition | --- | --- | 0.05 | --- | ||||

21. precondition | 0.06 | --- | --- | --- | ||||

22. precondition | 0.05 | --- | --- | --- | ||||

23. precondition | 0.04 | --- | --- | --- | ||||

24. index in array bounds | 0.03 | --- | --- | 0.02 | ||||

25. precondition | 0.06 | --- | --- | --- | ||||

26. precondition | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. precondition | --- | --- | 0.07 | --- | ||||

27. precondition | --- | --- | --- | 0.09 | ||||

28. variant decrease | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. VC for delete | 0.12 | --- | --- | --- | ||||

2. VC for delete | --- | --- | --- | 0.18 | ||||

29. precondition | 0.03 | --- | --- | 0.01 | ||||

30. precondition | 0.02 | --- | --- | 0.01 | ||||

31. precondition | 0.02 | --- | --- | 0.01 | ||||

32. precondition | 0.04 | --- | --- | --- | ||||

33. precondition | 0.07 | --- | --- | --- | ||||

34. precondition | 0.08 | --- | --- | --- | ||||

35. precondition | 0.06 | --- | --- | --- | ||||

36. precondition | --- | 0.20 | 0.51 | --- | ||||

37. precondition | 0.03 | --- | --- | --- | ||||

38. precondition | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. precondition | --- | --- | 0.47 | --- | ||||

2. precondition | --- | --- | 0.57 | --- | ||||

39. precondition | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. precondition | --- | 0.10 | --- | --- | ||||

2. precondition | --- | --- | --- | 0.73 | ||||

3. precondition | --- | 0.18 | --- | --- | ||||

4. precondition | --- | 1.60 | --- | --- | ||||

5. precondition | --- | 1.51 | --- | 1.14 | ||||

40. postcondition | 0.03 | --- | --- | --- | ||||

41. postcondition | 0.10 | --- | --- | --- | ||||

42. postcondition | --- | --- | --- | --- | ||||

inline_goal | ||||||||

1. postcondition | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. VC for delete | 0.03 | --- | --- | --- | ||||

2. VC for delete | 0.06 | --- | --- | --- | ||||

3. VC for delete | 0.06 | --- | --- | --- | ||||

4. VC for delete | 0.04 | --- | --- | --- | ||||

5. VC for delete | 0.04 | --- | --- | --- | ||||

6. VC for delete | 0.06 | --- | --- | --- | ||||

7. VC for delete | 0.18 | --- | --- | --- | ||||

8. VC for delete | --- | --- | --- | 0.14 | ||||

14. VC for remove | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. precondition | 0.02 | --- | --- | --- | ||||

2. precondition | 0.01 | --- | --- | --- | ||||

3. index in array bounds | 0.02 | --- | --- | --- | ||||

4. index in array bounds | 0.02 | --- | --- | --- | ||||

5. assertion | --- | 23.32 | --- | 16.68 | ||||

6. type invariant | 0.03 | --- | --- | --- | ||||

7. precondition | 0.02 | --- | --- | --- | ||||

8. precondition | 0.04 | --- | --- | --- | ||||

9. precondition | 0.04 | --- | --- | --- | ||||

10. precondition | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. VC for remove | --- | --- | --- | 0.26 | ||||

2. VC for remove | --- | --- | 0.07 | --- | ||||

11. precondition | 0.13 | --- | --- | --- | ||||

12. precondition | 0.03 | --- | --- | --- | ||||

13. precondition | 0.02 | --- | --- | --- | ||||

14. precondition | 0.04 | --- | --- | --- | ||||

15. precondition | 0.03 | --- | --- | --- | ||||

16. precondition | 0.02 | --- | --- | --- | ||||

17. precondition | 0.03 | --- | --- | --- | ||||

18. precondition | 0.02 | --- | --- | --- | ||||

19. precondition | 0.04 | --- | --- | --- | ||||

20. precondition | 0.02 | --- | --- | --- | ||||

21. precondition | --- | --- | 0.89 | 0.44 | ||||

22. precondition | 2.54 | --- | --- | 0.70 | ||||

23. type invariant | --- | --- | --- | 0.12 | ||||

24. type invariant | --- | --- | --- | 0.17 | ||||

25. type invariant | --- | --- | --- | --- | ||||

split_goal_wp | ||||||||

1. type invariant | 0.02 | --- | --- | --- | ||||

26. type invariant | 0.02 | --- | --- | 0.01 | ||||

27. postcondition | 0.03 | --- | --- | 0.00 | ||||

28. postcondition | --- | --- | --- | 2.00 |