Wiki Agenda Contact Version française

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

ObligationsAlt-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_cons0.04------------
VC for trans_path---------------
split_goal_wp
  1. variant decrease0.00------------
2. precondition0.04------------
3. precondition0.01------------
4. postcondition0.460.070.51------
5. postcondition0.66------------
6. postcondition0.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 init0.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. precondition0.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.040.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.050.06
84. loop variant decrease---------0.04---
85. precondition0.03------------
86. precondition0.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.040.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 preservation0.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 preservation0.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 preservation4.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 preservation0.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 preservation0.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. precondition0.04------------
214. precondition0.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 preservation0.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 preservation0.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. precondition0.03------------
277. precondition0.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.040.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.040.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 preservation0.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---