## Schorr-Waite algorithm

Schorr-Waite's graph marking algorithm

**Authors:** Mário Pereira

**Topics:** Ghost code / Graph Algorithms

**Tools:** Why3

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

Schorr-Waite algorithm

The Schorr-Waite algorithm is the first mountain that any formalism for pointer aliasing should climb. -- Richard Bornat, 2000

Author: Mário Pereira (UBI, then Université Paris Sud)

The code, specification, and invariants below follow those of the following two proofs:

- Thierry Hubert and Claude Marché, using Caduceus and Coq

A case study of C source code verification: the Schorr-Waite algorithm. SEFM 2005. http://www.lri.fr/~marche/hubert05sefm.ps

- Rustan Leino, using Dafny

Dafny: An Automatic Program Verifier for Functional Correctness. LPAR-16. http://research.microsoft.com/en-us/um/people/leino/papers/krml203.pdf

module SchorrWaite use import seq.Seq use import map.Map use import ref.Ref use import int.Int use import list.List use import list.Length use import list.Append use import set.Fset as S

Why3 has no support for arbitrary pointers, so we introduce a small component-as-array memory model

the type of pointers and the null pointer

type loc constant null: loc

each (non-null) location holds four fields: two Boolean marks m and c and two pointers left and right

val m: ref (map loc bool) val c: ref (map loc bool) val left: ref (map loc loc) val right: ref (map loc loc) val get_left (p: loc) : loc requires { p <> null } ensures { result = !left[p] } val set_left (p: loc) (v: loc) : unit requires { p <> null } writes { left } ensures { !left = set (old !left) p v } val get_right (p: loc) : loc requires { p <> null } ensures { result = !right[p] } val set_right (p: loc) (v: loc) : unit requires { p <> null } writes { right } ensures { !right = set (old !right) p v } val get_m (p: loc) : bool requires { p <> null } ensures { result = !m[p] } val set_m (p: loc) (v: bool) : unit requires { p <> null } writes { m } ensures { !m = set (old !m) p v } val get_c (p: loc) : bool requires { p <> null } ensures { result = !c[p] } val set_c (p: loc) (v: bool) : unit requires { p <> null } writes { c } ensures { !c = set (old !c) p v }

for the purpose of the proof, we add a fifth, ghost, field, which records the path from the root (when relevant)

val ghost path_from_root : ref (map loc (list loc)) val get_path_from_root (p : loc) : list loc ensures { result = !path_from_root[p] } val set_path_from_root (p: loc) (l : list loc) : unit requires { p <> null } writes { path_from_root } ensures { !path_from_root = set (old !path_from_root) p l }

Stack of nodes, from the root to the current location, in reverse order (i.e. the current location is the first element in the stack)

type stacknodes = Seq.seq loc predicate not_in_stack (n: loc) (s: stacknodes) = forall i: int. 0 <= i < Seq.length s -> n <> Seq.get s i let tl_stackNodes (stack: stacknodes) : stacknodes requires { Seq.length stack > 0 } ensures { result = stack[1 .. ] } ensures { forall n. not_in_stack n stack -> not_in_stack n result } = stack[1 .. ]

two lemmas about stacks

let lemma cons_not_in (s: stacknodes) (n t: loc) requires { not_in_stack n (cons t s) } ensures { not_in_stack n s } = assert { forall i: int. 0 <= i < Seq.length s -> Seq.get s i = Seq.get (cons t s) (i+1) } let lemma tl_cons (s1 s2: stacknodes) (p: loc) requires { Seq.length s2 > 0 } requires { s1 = s2[1 ..] } requires { p = Seq.get s2 0 } ensures { s2 = cons p s1 } = assert { Seq.(==) s2 (cons p s1) } function last (s: stacknodes) : loc = Seq.get s (Seq.length s - 1) predicate distinct (s: stacknodes) = forall i j. 0 <= i < Seq.length s -> 0 <= j < Seq.length s -> i <> j -> Seq.get s i <> Seq.get s j

Paths

predicate edge (x y : loc) (left right : map loc loc) = x <> null /\ (left[x] = y \/ right[x] = y) inductive path (left right : map loc loc) (x y : loc) (p : list loc) = | path_nil : forall x : loc, l r : map loc loc. path l r x x Nil | path_cons : forall x y z : loc, l r : (map loc loc), p : list loc. edge x z l r -> path l r z y p -> path l r x y (Cons x p) let rec lemma trans_path (x y z : loc) (l r : map loc loc) (p1 p2 : list loc) variant { length p1 } requires { path l r x y p1 } requires { path l r y z p2 } ensures { path l r x z (p1 ++ p2) } = match p1 with | Cons _ (Cons b _ as p') -> trans_path b y z l r p' p2 | _ -> () end lemma path_edge : forall x y : loc, left right : map loc loc. edge x y left right -> path left right x y (Cons x Nil) lemma path_edge_cons: forall n x y : loc, left right : map loc loc, pth : list loc. path left right n x pth -> edge x y left right -> path left right n y (pth ++ (Cons x Nil)) predicate reachable (left right: map loc loc) (x y : loc) = exists p : list loc. path left right x y p

Schorr-Waite algorithm

let schorr_waite (root: loc) (ghost graph : set loc) : unit requires { root <> null /\ S.mem root graph } (* graph is closed under left and right *) requires { forall n : loc. S.mem n graph -> n <> null /\ S.mem !left[n] graph /\ S.mem !right[n] graph } (* graph starts with nothing marked *) requires { forall x : loc. S.mem x graph -> not !m[x] } (* the structure of the graph is not changed *) ensures { forall n : loc. S.mem n graph -> (old !left)[n] = !left[n] /\ (old !right)[n] = !right[n] } (* all the non-null vertices reachable from root are marked at the end of the algorithm, and only these *) ensures { forall n : loc. S.mem n graph -> !m[n] -> reachable (old !left) (old !right) root n } ensures { !m[root] } ensures { forall n : loc. S.mem n graph -> !m[n] -> (forall ch : loc. edge n ch !left !right -> ch <> null -> !m[ch]) } = 'Init: let t = ref root in let p = ref null in let ghost stackNodes = ref Seq.empty in let ghost pth = ref Nil in ghost set_path_from_root !t !pth; let ghost unmarked_nodes = ref graph in let ghost c_false_nodes = ref graph in while !p <> null || (!t <> null && not get_m !t) do invariant { forall n. mem n graph -> not_in_stack n !stackNodes \/ exists i : int. Seq.get !stackNodes i = n } invariant { not_in_stack null !stackNodes } invariant { Seq.length !stackNodes = 0 <-> !p = null } invariant { S.mem !t graph } invariant { !p <> null -> S.mem !p graph } invariant { Seq.length !stackNodes <> 0 -> Seq.get !stackNodes 0 = !p } invariant { forall n : loc. S.mem n graph -> not !m[n] -> S.mem n !unmarked_nodes } invariant { forall n : loc. S.mem n graph -> not !c[n] -> S.mem n !c_false_nodes } invariant { forall i. 0 <= i < Seq.length !stackNodes -> S.mem (Seq.get !stackNodes i) graph } invariant { forall i. 0 <= i < Seq.length !stackNodes - 1 -> let p1 = Seq.get !stackNodes i in let p2 = Seq.get !stackNodes (i+1) in (!c[p2] -> (at !left 'Init)[p2] = !left[p2] /\ (at !right 'Init)[p2] = p1) /\ (not !c[p2] -> (at !left 'Init)[p2] = p1 /\ (at !right 'Init)[p2] = !right[p2]) } invariant { !path_from_root[root] = Nil } invariant { forall n : loc. S.mem n graph -> not_in_stack n !stackNodes -> !left[n] = (at !left 'Init)[n] /\ !right[n] = (at !right 'Init)[n] } (* something like Leino's line 74; this is useful to prove that * the stack is empty iff p = null *) invariant { Seq.length !stackNodes <> 0 -> let first = last !stackNodes in if !c[first] then !right[first] = null else !left[first] = null } invariant { Seq.length !stackNodes <> 0 -> last !stackNodes = root } (* something like lines 75-76 from Leino's paper *) invariant { forall k : int. 0 <= k < Seq.length !stackNodes - 1 -> if !c[Seq.get !stackNodes k] then !right[Seq.get !stackNodes k] = Seq.get !stackNodes (k+1) else !left [Seq.get !stackNodes k] = Seq.get !stackNodes (k+1) } (* all nodes in the stack are marked * (I4a in Hubert and Marché and something alike line 57 in Leino) *) invariant { forall i. 0 <= i < Seq.length !stackNodes -> !m[Seq.get !stackNodes i] } (* stack has no duplicates ---> line 55 from Leino's paper *) invariant { distinct !stackNodes } (* something like Leino's line 68 *) invariant { forall i. 0 <= i < Seq.length !stackNodes -> let n = Seq.get !stackNodes i in if !c[n] then !left[n] = (at !left 'Init)[n] else !right[n] = (at !right 'Init)[n] } (* lines 80-81 from Leino's paper *) invariant { Seq.length !stackNodes <> 0 -> if !c[!p] then (at !right 'Init)[!p] = !t else (at !left 'Init)[!p] = !t } (* lines 78-79 from Leino's paper *) invariant { forall k : int. 0 < k < Seq.length !stackNodes -> let n = Seq.get !stackNodes k in if !c[n] then Seq.get !stackNodes (k - 1) = (at !right 'Init)[n] else Seq.get !stackNodes (k - 1) = (at !left 'Init)[n] } (* line 70 from Leino's paper *) invariant { !p <> null -> path (at !left 'Init) (at !right 'Init) root !p !pth } (* line 72 from Leino's paper *) invariant { forall n : loc. S.mem n graph -> !m[n] -> reachable (at !left 'Init) (at !right 'Init) root n } invariant { !p = null -> !t = root } (* line 70 from Leino's paper *) invariant { forall n : loc, pth : list loc. S.mem n graph -> !m[n] -> pth = !path_from_root[n] -> path (at !left 'Init) (at !right 'Init) root n pth } (* lines 61-62 from Leinos' paper *) invariant { forall n : loc. S.mem n graph -> n <> null -> !m[n] -> not_in_stack n !stackNodes -> (!left[n] <> null -> !m[!left[n]]) /\ (!right[n] <> null -> !m[!right[n]]) } (* something like Leino's lines 57-59 *) invariant { forall i. 0 <= i < Seq.length !stackNodes -> let n = Seq.get !stackNodes i in !c[n] -> (!left[n] <> null -> !m[!left[n]]) /\ (!right[n] <> null -> !m[!right[n]]) } (* termination proved using lexicographic order over a triple *) variant { S.cardinal !unmarked_nodes, S.cardinal !c_false_nodes, Seq.length !stackNodes } if !t = null || get_m !t then begin if get_c !p then begin (* pop *) let q = !t in t := !p; ghost stackNodes := tl_stackNodes !stackNodes; p := !right[!p]; set_right !t q; ghost pth := get_path_from_root !p; end else begin (* swing *) let q = !t in t := get_right !p; set_right !p (get_left !p); set_left !p q; ghost c_false_nodes := S.remove !p !c_false_nodes; set_c !p true; end end else begin (* push *) let q = !p in p := !t; ghost stackNodes := Seq.cons !p !stackNodes; t := get_left !t; set_left !p q; set_m !p true; ghost if !p <> root then pth := !pth ++ (Cons q Nil) else pth := Nil; ghost set_path_from_root !p !pth; assert { !p = Seq.get !stackNodes 0 }; assert { path (at !left 'Init) (at !right 'Init) root !p !pth }; set_c !p false; ghost c_false_nodes := S.add !p !c_false_nodes; ghost unmarked_nodes := S.remove !p !unmarked_nodes end done end

download ZIP archive

# Why3 Proof Results for Project "schorr_waite"

## Theory "schorr_waite.SchorrWaite": fully verified in 38.84 s

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

VC for tl_stackNodes | --- | --- | --- | --- | --- | ||||

split_goal_wp | |||||||||

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

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

VC for cons_not_in | --- | --- | --- | --- | --- | ||||

inline_goal | |||||||||

1. VC for cons_not_in | --- | --- | --- | --- | --- | ||||

split_goal_wp | |||||||||

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

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

VC for tl_cons | 0.04 | --- | --- | --- | --- | ||||

VC for trans_path | --- | --- | --- | --- | --- | ||||

split_goal_wp | |||||||||

1. variant decrease | 0.00 | --- | --- | --- | --- | ||||

2. precondition | 0.04 | --- | --- | --- | --- | ||||

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

4. postcondition | 0.46 | 0.07 | 0.51 | --- | --- | ||||

5. postcondition | 0.66 | --- | --- | --- | --- | ||||

6. postcondition | 0.05 | --- | --- | --- | --- | ||||

path_edge | --- | --- | --- | 0.05 | --- | ||||

path_edge_cons | --- | --- | --- | 0.03 | --- | ||||

VC for schorr_waite | --- | --- | --- | --- | --- | ||||

split_goal_wp | |||||||||

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

2. loop invariant init | --- | --- | --- | 0.03 | --- | ||||

3. loop invariant init | --- | --- | --- | 0.03 | --- | ||||

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

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

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

7. loop invariant init | --- | --- | --- | 0.02 | --- | ||||

8. loop invariant init | --- | --- | --- | 0.02 | --- | ||||

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

10. loop invariant init | --- | --- | --- | 0.02 | --- | ||||

11. loop invariant init | --- | --- | --- | 0.01 | --- | ||||

12. loop invariant init | 0.01 | --- | --- | 0.02 | --- | ||||

13. loop invariant init | --- | --- | --- | 0.02 | --- | ||||

14. loop invariant init | --- | --- | --- | 0.02 | --- | ||||

15. loop invariant init | --- | --- | --- | 0.02 | --- | ||||

16. loop invariant init | --- | --- | --- | 0.03 | --- | ||||

17. loop invariant init | --- | --- | --- | 0.02 | --- | ||||

18. loop invariant init | --- | --- | --- | 0.03 | --- | ||||

19. loop invariant init | --- | --- | --- | 0.03 | --- | ||||

20. loop invariant init | --- | --- | --- | 0.03 | --- | ||||

21. loop invariant init | --- | --- | --- | 0.03 | --- | ||||

22. loop invariant init | --- | --- | --- | 0.02 | --- | ||||

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

24. precondition | --- | --- | --- | 0.04 | --- | ||||

25. precondition | --- | --- | --- | 0.04 | --- | ||||

26. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

27. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

28. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

29. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

30. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

31. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

32. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

33. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

34. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

35. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

36. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

37. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

38. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

39. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

40. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

41. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

42. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

43. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

44. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

45. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

46. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

47. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

48. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

49. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

50. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

51. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

52. loop variant decrease | --- | --- | --- | 0.04 | --- | ||||

53. precondition | --- | --- | --- | 0.04 | --- | ||||

54. precondition | --- | --- | --- | 0.04 | --- | ||||

55. precondition | --- | --- | --- | 0.04 | --- | ||||

56. precondition | --- | --- | --- | 0.04 | --- | ||||

57. precondition | --- | --- | --- | 0.03 | --- | ||||

58. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

59. loop invariant preservation | --- | --- | --- | 0.04 | 0.03 | ||||

60. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

61. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

62. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

63. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

64. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

65. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

66. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

67. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

68. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

69. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

70. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

71. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

72. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

73. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

74. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

75. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

76. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

77. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

78. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

79. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

80. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

81. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

82. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

83. loop invariant preservation | --- | --- | --- | 0.05 | 0.06 | ||||

84. loop variant decrease | --- | --- | --- | 0.04 | --- | ||||

85. precondition | 0.03 | --- | --- | --- | --- | ||||

86. precondition | 0.04 | --- | --- | --- | --- | ||||

87. precondition | --- | --- | --- | 0.04 | --- | ||||

88. precondition | --- | --- | --- | 0.03 | --- | ||||

89. loop invariant preservation | --- | --- | --- | 0.08 | --- | ||||

90. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

91. loop invariant preservation | --- | --- | --- | 0.14 | --- | ||||

92. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

93. loop invariant preservation | --- | --- | --- | 0.07 | --- | ||||

94. loop invariant preservation | --- | --- | --- | 0.07 | --- | ||||

95. loop invariant preservation | --- | --- | --- | 0.08 | --- | ||||

96. loop invariant preservation | --- | --- | --- | 0.08 | --- | ||||

97. loop invariant preservation | --- | --- | --- | 0.16 | --- | ||||

98. loop invariant preservation | --- | --- | --- | --- | --- | ||||

inline_goal | |||||||||

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

split_goal_wp | |||||||||

1. loop invariant preservation | --- | --- | --- | 0.98 | --- | ||||

2. loop invariant preservation | --- | --- | --- | 1.04 | --- | ||||

3. loop invariant preservation | --- | --- | --- | 1.00 | --- | ||||

4. loop invariant preservation | --- | --- | --- | 0.95 | --- | ||||

99. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

100. loop invariant preservation | --- | --- | --- | --- | --- | ||||

split_goal_wp | |||||||||

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

introduce_premises | |||||||||

1. loop invariant preservation | --- | --- | --- | 0.66 | --- | ||||

2. loop invariant preservation | --- | --- | --- | 0.93 | --- | ||||

101. loop invariant preservation | --- | --- | --- | 0.32 | --- | ||||

102. loop invariant preservation | --- | --- | --- | 0.43 | --- | ||||

103. loop invariant preservation | --- | --- | --- | 0.27 | --- | ||||

104. loop invariant preservation | --- | --- | --- | 0.16 | --- | ||||

105. loop invariant preservation | --- | --- | --- | 0.18 | --- | ||||

106. loop invariant preservation | --- | --- | --- | 0.23 | --- | ||||

107. loop invariant preservation | --- | --- | --- | 0.10 | --- | ||||

108. loop invariant preservation | --- | --- | --- | 0.22 | --- | ||||

109. loop invariant preservation | --- | --- | --- | 0.08 | --- | ||||

110. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

111. loop invariant preservation | --- | --- | --- | 0.07 | --- | ||||

112. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

113. loop invariant preservation | --- | --- | --- | --- | --- | ||||

introduce_premises | |||||||||

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

inline_goal | |||||||||

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

split_goal_wp | |||||||||

1. VC for schorr_waite | --- | --- | --- | 0.70 | --- | ||||

2. VC for schorr_waite | --- | --- | --- | 0.70 | --- | ||||

114. loop invariant preservation | --- | --- | --- | 0.25 | --- | ||||

115. loop variant decrease | --- | --- | --- | 0.09 | --- | ||||

116. precondition | --- | --- | --- | 0.04 | --- | ||||

117. precondition | --- | --- | --- | 0.03 | --- | ||||

118. precondition | --- | --- | --- | 0.03 | --- | ||||

119. precondition | --- | --- | --- | 0.04 | --- | ||||

120. precondition | --- | --- | --- | 0.04 | --- | ||||

121. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

122. loop invariant preservation | --- | --- | --- | 0.04 | 0.03 | ||||

123. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

124. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

125. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

126. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

127. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

128. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

129. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

130. loop invariant preservation | 0.04 | --- | --- | 0.17 | --- | ||||

131. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

132. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

133. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

134. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

135. loop invariant preservation | --- | --- | --- | 0.18 | --- | ||||

136. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

137. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

138. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

139. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

140. loop invariant preservation | 0.02 | --- | --- | 0.04 | --- | ||||

141. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

142. loop invariant preservation | --- | --- | --- | 0.13 | --- | ||||

143. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

144. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

145. loop invariant preservation | --- | --- | --- | --- | --- | ||||

introduce_premises | |||||||||

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

split_goal_wp | |||||||||

1. VC for schorr_waite | --- | --- | --- | 0.02 | --- | ||||

2. VC for schorr_waite | --- | --- | --- | 0.02 | --- | ||||

146. loop invariant preservation | --- | --- | --- | 0.60 | --- | ||||

147. loop variant decrease | --- | --- | --- | 0.04 | --- | ||||

148. precondition | --- | --- | --- | 0.04 | --- | ||||

149. precondition | --- | --- | --- | 0.06 | --- | ||||

150. precondition | --- | --- | --- | 0.05 | --- | ||||

151. precondition | --- | --- | --- | 0.04 | --- | ||||

152. assertion | --- | --- | 0.04 | --- | --- | ||||

153. assertion | --- | --- | --- | 0.08 | --- | ||||

154. precondition | --- | --- | --- | 0.06 | --- | ||||

155. loop invariant preservation | --- | --- | --- | 0.10 | --- | ||||

156. loop invariant preservation | --- | --- | --- | 0.15 | --- | ||||

157. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

158. loop invariant preservation | --- | --- | --- | 0.18 | --- | ||||

159. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

160. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

161. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

162. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

163. loop invariant preservation | --- | --- | --- | 0.09 | --- | ||||

164. loop invariant preservation | 4.12 | --- | --- | 0.42 | --- | ||||

165. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

166. loop invariant preservation | --- | --- | --- | 0.10 | --- | ||||

167. loop invariant preservation | --- | --- | --- | 0.43 | --- | ||||

168. loop invariant preservation | --- | --- | --- | 0.27 | --- | ||||

169. loop invariant preservation | 0.55 | --- | --- | 0.13 | --- | ||||

170. loop invariant preservation | --- | --- | --- | 0.09 | --- | ||||

171. loop invariant preservation | --- | --- | --- | 0.16 | --- | ||||

172. loop invariant preservation | --- | --- | --- | 0.34 | --- | ||||

173. loop invariant preservation | --- | --- | --- | 0.16 | --- | ||||

174. loop invariant preservation | 0.60 | --- | --- | 0.15 | --- | ||||

175. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

176. loop invariant preservation | --- | --- | --- | 0.15 | --- | ||||

177. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

178. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

179. loop invariant preservation | --- | --- | --- | --- | --- | ||||

split_goal_wp | |||||||||

1. loop invariant preservation | --- | --- | --- | 0.08 | --- | ||||

2. loop invariant preservation | --- | --- | --- | 0.08 | --- | ||||

180. loop invariant preservation | --- | --- | --- | 0.19 | --- | ||||

181. loop variant decrease | --- | --- | --- | 0.04 | --- | ||||

182. precondition | --- | --- | --- | 0.05 | --- | ||||

183. assertion | --- | --- | 0.05 | --- | --- | ||||

184. assertion | --- | --- | --- | 0.06 | --- | ||||

185. precondition | --- | --- | --- | 0.06 | --- | ||||

186. loop invariant preservation | --- | --- | --- | 0.11 | --- | ||||

187. loop invariant preservation | --- | --- | --- | 0.10 | --- | ||||

188. loop invariant preservation | --- | --- | --- | 0.07 | --- | ||||

189. loop invariant preservation | --- | --- | --- | 0.10 | --- | ||||

190. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

191. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

192. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

193. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

194. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

195. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

196. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

197. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

198. loop invariant preservation | --- | --- | --- | 0.14 | --- | ||||

199. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

200. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

201. loop invariant preservation | --- | --- | --- | 0.15 | --- | ||||

202. loop invariant preservation | --- | --- | --- | 0.15 | --- | ||||

203. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

204. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

205. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

206. loop invariant preservation | --- | --- | --- | 0.13 | --- | ||||

207. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

208. loop invariant preservation | --- | --- | --- | 0.08 | --- | ||||

209. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

210. loop invariant preservation | --- | --- | --- | 0.14 | --- | ||||

211. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

212. loop variant decrease | --- | --- | --- | 0.04 | --- | ||||

213. precondition | 0.04 | --- | --- | --- | --- | ||||

214. precondition | 0.04 | --- | --- | --- | --- | ||||

215. precondition | --- | --- | --- | 0.08 | --- | ||||

216. precondition | --- | --- | --- | 0.07 | --- | ||||

217. loop invariant preservation | --- | --- | --- | 0.07 | --- | ||||

218. loop invariant preservation | --- | --- | --- | 0.07 | --- | ||||

219. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

220. loop invariant preservation | --- | --- | --- | 0.08 | --- | ||||

221. loop invariant preservation | --- | --- | --- | 0.07 | --- | ||||

222. loop invariant preservation | --- | --- | --- | 0.08 | --- | ||||

223. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

224. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

225. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

226. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

227. loop invariant preservation | --- | --- | --- | 0.08 | --- | ||||

228. loop invariant preservation | --- | --- | --- | --- | --- | ||||

split_goal_wp | |||||||||

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

introduce_premises | |||||||||

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

inline_goal | |||||||||

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

2. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

229. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

230. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

231. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

232. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

233. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

234. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

235. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

236. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

237. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

238. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

239. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

240. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

241. loop invariant preservation | --- | --- | --- | --- | --- | ||||

split_goal_wp | |||||||||

1. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

2. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

242. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

243. loop variant decrease | --- | --- | --- | 0.04 | --- | ||||

244. precondition | --- | --- | --- | 0.04 | --- | ||||

245. precondition | --- | --- | --- | 0.04 | --- | ||||

246. precondition | --- | --- | --- | 0.04 | --- | ||||

247. precondition | --- | --- | --- | 0.04 | --- | ||||

248. precondition | --- | --- | --- | 0.04 | --- | ||||

249. loop invariant preservation | --- | --- | --- | 0.07 | --- | ||||

250. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

251. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

252. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

253. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

254. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

255. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

256. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

257. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

258. loop invariant preservation | 0.09 | --- | --- | 0.08 | --- | ||||

259. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

260. loop invariant preservation | --- | --- | --- | 0.07 | --- | ||||

261. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

262. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

263. loop invariant preservation | --- | --- | --- | 0.08 | --- | ||||

264. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

265. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

266. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

267. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

268. loop invariant preservation | 0.04 | --- | --- | --- | --- | ||||

269. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

270. loop invariant preservation | --- | --- | --- | 0.09 | --- | ||||

271. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

272. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

273. loop invariant preservation | --- | --- | --- | 0.07 | --- | ||||

274. loop invariant preservation | --- | --- | --- | --- | --- | ||||

inline_goal | |||||||||

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

simplify_trivial_quantification | |||||||||

1. VC for schorr_waite | --- | --- | --- | 0.02 | --- | ||||

275. loop variant decrease | --- | --- | --- | 0.06 | --- | ||||

276. precondition | 0.03 | --- | --- | --- | --- | ||||

277. precondition | 0.04 | --- | --- | --- | --- | ||||

278. precondition | --- | --- | --- | 0.03 | --- | ||||

279. precondition | --- | --- | --- | 0.04 | --- | ||||

280. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

281. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

282. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

283. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

284. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

285. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

286. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

287. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

288. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

289. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

290. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

291. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

292. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

293. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

294. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

295. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

296. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

297. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

298. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

299. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

300. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

301. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

302. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

303. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

304. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

305. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

306. loop variant decrease | --- | --- | --- | 0.04 | --- | ||||

307. precondition | --- | --- | --- | 0.03 | --- | ||||

308. precondition | --- | --- | --- | 0.03 | --- | ||||

309. precondition | --- | --- | --- | 0.03 | --- | ||||

310. precondition | --- | --- | --- | 0.03 | --- | ||||

311. precondition | --- | --- | --- | 0.04 | --- | ||||

312. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

313. loop invariant preservation | --- | --- | --- | 0.04 | 0.00 | ||||

314. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

315. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

316. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

317. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

318. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

319. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

320. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

321. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

322. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

323. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

324. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

325. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

326. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

327. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

328. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

329. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

330. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

331. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

332. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

333. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

334. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

335. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

336. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

337. loop invariant preservation | --- | --- | --- | 0.04 | 0.00 | ||||

338. loop variant decrease | --- | --- | --- | 0.04 | --- | ||||

339. precondition | --- | --- | --- | 0.04 | --- | ||||

340. precondition | --- | --- | --- | 0.04 | --- | ||||

341. precondition | --- | --- | --- | 0.04 | --- | ||||

342. precondition | --- | --- | --- | 0.04 | --- | ||||

343. assertion | --- | --- | 0.05 | --- | --- | ||||

344. assertion | --- | --- | --- | 0.04 | --- | ||||

345. precondition | --- | --- | --- | 0.04 | --- | ||||

346. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

347. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

348. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

349. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

350. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

351. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

352. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

353. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

354. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

355. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

356. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

357. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

358. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

359. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

360. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

361. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

362. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

363. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

364. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

365. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

366. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

367. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

368. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

369. loop invariant preservation | --- | --- | --- | 0.10 | --- | ||||

370. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

371. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

372. loop variant decrease | --- | --- | --- | 0.10 | --- | ||||

373. precondition | --- | --- | --- | 0.04 | --- | ||||

374. assertion | --- | --- | 0.05 | --- | --- | ||||

375. assertion | --- | --- | --- | 0.04 | --- | ||||

376. precondition | --- | --- | --- | 0.04 | --- | ||||

377. loop invariant preservation | --- | --- | --- | 0.07 | --- | ||||

378. loop invariant preservation | --- | --- | --- | 0.07 | --- | ||||

379. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

380. loop invariant preservation | --- | --- | --- | 0.07 | --- | ||||

381. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

382. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

383. loop invariant preservation | --- | --- | --- | 0.08 | --- | ||||

384. loop invariant preservation | --- | --- | --- | 0.09 | --- | ||||

385. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

386. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

387. loop invariant preservation | --- | --- | --- | 0.02 | --- | ||||

388. loop invariant preservation | --- | --- | --- | --- | --- | ||||

introduce_premises | |||||||||

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

split_goal_wp | |||||||||

1. VC for schorr_waite | --- | --- | --- | 0.05 | --- | ||||

2. VC for schorr_waite | --- | --- | --- | 0.05 | --- | ||||

389. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

390. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

391. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

392. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

393. loop invariant preservation | 0.11 | --- | --- | 0.04 | --- | ||||

394. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

395. loop invariant preservation | --- | --- | --- | 0.06 | --- | ||||

396. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

397. loop invariant preservation | --- | --- | --- | 0.03 | --- | ||||

398. loop invariant preservation | --- | --- | --- | 0.08 | --- | ||||

399. loop invariant preservation | --- | --- | --- | 0.04 | --- | ||||

400. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

401. loop invariant preservation | --- | --- | --- | --- | --- | ||||

inline_goal | |||||||||

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

introduce_premises | |||||||||

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

split_goal_wp | |||||||||

1. VC for schorr_waite | --- | --- | --- | 0.04 | --- | ||||

2. VC for schorr_waite | --- | --- | 0.04 | --- | --- | ||||

402. loop invariant preservation | --- | --- | --- | 0.05 | --- | ||||

403. loop variant decrease | --- | --- | --- | 0.07 | --- | ||||

404. postcondition | --- | --- | --- | --- | --- | ||||

split_goal_wp | |||||||||

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

2. postcondition | --- | --- | --- | 0.03 | --- | ||||

405. postcondition | --- | --- | --- | 0.04 | --- | ||||

406. postcondition | --- | --- | --- | 0.03 | --- | ||||

407. postcondition | --- | --- | --- | 0.03 | --- | ||||

408. postcondition | --- | --- | --- | --- | --- | ||||

split_goal_wp | |||||||||

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

2. postcondition | --- | --- | --- | 0.06 | --- | ||||

409. postcondition | --- | --- | --- | 0.03 | --- | ||||

410. postcondition | --- | --- | --- | 0.03 | --- | ||||

411. postcondition | --- | --- | --- | 0.06 | --- |