Skip to content

GitLab

why3
why3
Commit 90b5f914 authored by Martin Clochard's avatar Martin Clochard
Browse files
Options

new example: alternative Schorr-Waite

parent 99b6e736
Hide whitespace changes
Inline Side-by-side
Showing with 923 additions and 0 deletions
examples/schorr_waite_via_recursion.mlw 0 → 100644
View file @ 90b5f914
(** Schorr-Waite algorithm for general-size records.
Author: Martin Clochard (Université Paris Sud)
Here the proof is carried out by proving an equivalent
recursive program. The recursive program can be justified
to be equivalent to the looping one:
all side-effects/exception throwing are done by running the loop body
(which features a minor modification to exit by exception),
so the recursive programs amounts to execute an arbitrary number
of time the loop body. It is immediately followed by an absurd statement
to enforce the equivalence with the loop which runs its body an
infinite number of times.
Although the added recursive structure can be seen to be computationally
irrelevant, it allows to discharge details about Schorr-Waite
stack management through a recursive procedure proof. The method
basically make explicit the derecursification used to obtain
Schorr-Waite algorithm.
See example verifythis_2016_tree_traversal for details about
the technique, applied to a similar algorithm for trees.
*)
(** Component-as-array memory model, with null pointers
and arbitrary-sized memory blocks. *)
module Memory
use import int.Int
use import option.Option
use import map.Map
(** Memory locations *)
type loc
(** Null pointer *)
constant null : loc
(** Marks used by Schorr-Waite *)
type color =
| White
| Black (option int)
type pmem = map loc (map int loc)
(** Memory blocks have two parts: a marking part containing in particular
Schorr-Waite internal management data, and a sequence of pointers
to other memory blocks. *)
type memory model {
(** Associate block size to location. *)
block_size : map loc int;
(** Pointers to other memory blocks. *)
mutable accessor : pmem;
(** Marks. *)
mutable colors : map loc color;
}
(** Global instance for memory *)
val memo : memory
(** null creation *)
val null () : loc ensures { result = null }
(** null test *)
val is_null (l:loc) : bool ensures { result <-> l = null }
(** Get block size associated to a given location *)
val get_block_size (l:loc) : int
requires { l <> null }
reads { memo }
ensures { result = memo.block_size[l] /\ result >= 0 }
(** Access to a mark *)
val get_color (l:loc) : color
requires { l <> null }
reads { memo }
ensures { result = memo.colors[l] }
(** Set a mark. We also impose the restriction that when a block is
marked black, the given index must be coherent with the block size.
This impose special treatment for 0-sized memory blocks. *)
val set_color (l:loc) (c:color) : unit
requires { l <> null }
requires { match c with
| White -> true
| Black None -> memo.block_size[l] = 0
| Black (Some ind) -> 0 <= ind < memo.block_size[l]
end }
writes { memo.colors }
ensures { memo.colors = old (memo.colors[l <- c]) }
(** Getter/Setter for pointer buffer *)
val get_acc (l:loc) (k:int) : loc
requires { l <> null /\ 0 <= k < memo.block_size[l] }
reads { memo }
ensures { result = memo.accessor[l][k] }
val set_acc (l:loc) (k:int) (d:loc) : unit
requires { l <> null /\ 0 <= k < memo.block_size[l] }
writes { memo.accessor }
ensures { memo.accessor =
old (memo.accessor[l <- memo.accessor[l][k <- d]]) }
(** Take ghost snapshots of memory. *)
val ghost snapshot_acc () : pmem
reads { memo }
ensures { result = memo.accessor }
val ghost snapshot_colors () : map loc color
reads { memo }
ensures { result = memo.colors }
end
(** Define notions about the memory graph *)
module GraphShape
use import int.Int
use import set.Fset
use import map.Map
use import Memory
predicate black (c:color) = c <> White
(** Edges *)
predicate edge (m:memory) (x y:loc) =
x <> null /\ (exists n. 0 <= n < m.block_size[x] /\ m.accessor[x][n] = y)
(** Paths *)
inductive path memory (x y:loc) =
| path_nil : forall m x. path m x x
| path_cons : forall m x y z. edge m x y /\ path m y z -> path m x z
(** DFS invariant. For technical reason, it must refer to different parts
of the memory at different time. The graph structure is given
via the initial memory, but the coloring is given via the current one. *)
predicate well_colored_on (graph gray:set loc) (m:memory) (cl:map loc color) =
subset gray graph /\
(forall x y. mem x graph /\ edge m x y /\ y <> null /\ black cl[x] ->
mem x gray \/ black cl[y]) /\
(forall x. mem x gray -> black cl[x])
(** Unchanged only concerns the graph shape, not the marks *)
predicate unchanged (m1 m2:memory) =
forall x n. x <> null /\ 0 <= n < m1.block_size[x] ->
m2.accessor[x][n] = m1.accessor[x][n]
end
(** Proof of Schorr-Waite algorithm *)
module SchorrWaite
use import int.Int
use import option.Option
use import set.Fset
use import map.Map
use import map.Const
use import ref.Ref
use import Memory
use import GraphShape
let black (l: loc) : bool
requires { l <> null }
reads { memo }
ensures { result <-> black memo.colors[l] }
= match get_color l with White -> false | _ -> true end
exception Stop
let schorr_waite (root: loc) (ghost graph: set loc) : unit
(** Root belong to graph (note: for simplicity, the graph set
may (and likely does) contain the null pointer. *)
requires { mem root graph }
(** Graph is closed by following edges *)
requires { forall l n.
mem l graph /\ l <> null /\ 0 <= n < memo.block_size[l] ->
mem memo.accessor[l][n] graph }
writes { memo.accessor, memo.colors }
(** The graph starts fully unmarked. *)
requires { forall x. mem x graph -> not black memo.colors[x] }
(** The graph structure is left unchanged. *)
ensures { unchanged (old memo) memo }
(** Every non-null location reachable from the root is marked black. *)
ensures { forall x. path (old memo) root x /\ x <> null ->
black memo.colors[x] }
(** Every other location is left with its previous color. *)
ensures { forall x. not path (old memo) root x /\ x <> null ->
memo.colors[x] = (old memo).colors[x] }
=
'I:
let t = ref root in
let p = ref (null ()) in
(** Schorr-Waite loop body. *)
let body () : unit
(** Loop body specification: mindlessly repeat the underlying code. *)
requires { !p <> null /\ (!t = null \/ black memo.colors[!t]) ->
match memo.colors[!p] with
| Black (Some m) -> 0 <= m < memo.block_size[!p]
| _ -> false
end }
ensures { old (!p <> null \/ (!t <> null /\ not black memo.colors[!t])) }
ensures { old (!t <> null /\ not black memo.colors[!t] /\
memo.block_size[!t] = 0) ->
memo.colors = old memo.colors[!t <- Black None] /\
!t = old !t /\ !p = old (!p) /\ memo.accessor = old memo.accessor
}
ensures { old (!t <> null /\ not black memo.colors[!t] /\
memo.block_size[!t] > 0) ->
memo.colors = old memo.colors[!t <- Black (Some 0)] /\
!t = old memo.accessor[!t][0] /\ !p = old (!t) /\
memo.accessor = old memo.accessor[!t <- memo.accessor[!t][0 <- !p]] }
ensures { old (!t = null \/ black memo.colors[!t]) ->
match old (memo.colors[!p]) with
| Black (Some m) ->
let n = m + 1 in
if n = old (memo.block_size[!p])
then
!t = old (!p) /\ !p = (old memo.accessor[!p])[m] /\
memo.colors = old (memo.colors) /\
memo.accessor =
(old memo.accessor)[old !p <-
(old memo.accessor[!p])[m <- old !t]]
else !p = old !p /\ !t = (old memo.accessor[!p])[n] /\
memo.colors = (old memo.colors)[old !p <- Black (Some n)] /\
let pi = (old memo.accessor[!p])[m] in
memo.accessor =
(old memo.accessor)[old !p <-
(old memo.accessor[!p])[n <- pi][m <- old !t]]
| _ -> false
end }
raises { Stop -> old(!p = null /\ (!t = null \/ black memo.colors[!t])) /\
memo.colors = old memo.colors /\ memo.accessor = old memo.accessor }
= (** Minor modification to the loop: it exits by exception. *)
if is_null !p && (is_null !t || black !t) then raise Stop;
if is_null !t || black !t then begin
match get_color !p with
| Black (Some m) ->
let s = get_block_size !p in
let n = m + 1 in
if n = s then begin (* Pop *)
let q = !t in
t := !p;
p := get_acc !p m;
set_acc !t m q
end else begin (* Swing *)
let q = !t in
t := get_acc !p n;
set_acc !p n (get_acc !p m);
set_acc !p m q;
set_color !p (Black (Some n))
end
| _ -> absurd
end
end else
let s = get_block_size !t in
if s = 0 then (* Mark & continue *) set_color !t (Black None)
else begin (* Mark & Push *)
let q = !p in
p := !t;
t := get_acc !t 0;
set_acc !p 0 q;
set_color !p (Black (Some 0))
end
in
let rec aux (ghost gray:set loc) : unit
(* DFS invariant *)
requires { well_colored_on graph gray (at memo 'I) memo.colors }
requires { mem !t graph }
(* Non-marked nodes have unchanged structure with
respect to the initial one. *)
requires { forall x n.
x <> null /\ not black memo.colors[x] /\ 0 <= n < memo.block_size[x] ->
memo.accessor[x][n] = (at memo.accessor 'I)[x][n] }
(* 'stack frames' are maintained correctly *)
ensures { !t = old !t /\ !p = old !p }
(* Pointer buffer is left unchanged *)
ensures { unchanged (old memo) memo }
(* Maintain DFS invariant *)
ensures { well_colored_on graph gray (at memo 'I) memo.colors }
(* The top node get marked *)
ensures { black memo.colors[!t] \/ !t = null }
(* May not mark unreachable node, neither change marked node. *)
ensures { forall x.
x <> null -> not path (at memo 'I) !t x \/ black (old memo.colors)[x] ->
memo.colors[x] = (old memo.colors)[x] }
(* Never 'exit' the loop during the recursive calls *)
raises { Stop -> false }
(* Terminates because there is a limited number of 'grayable' nodes. *)
variant { cardinal graph - cardinal gray }
= 'J:
if is_null !t || black !t then () else begin
let s = get_block_size !t in
let ghost g2 = add !t gray in
assert { path (at memo 'I) !t !t };
body (); (* Either push or mark & continue. *)
if s <> 0 then begin
for i = 0 to s - 2 do (* Over all sub-blocs... *)
(* DFS invariant. *)
invariant { well_colored_on graph g2 (at memo 'I) memo.colors }
(* Current stack frame invariants *)
invariant { !p = at !t 'J }
invariant { !t = (at memo.accessor 'I)[!p][i] }
invariant { memo.colors[!p] = Black (Some i) }
invariant { forall j. 0 <= j < s /\ j <> i ->
memo.accessor[!p][j] = (at memo.accessor 'J)[!p][j] }
invariant { memo.accessor[!p][i] = at !p 'J }
(* Outside structure is unchanged. *)
invariant { forall l n.
l <> null /\ l <> !p /\ 0 <= n < memo.block_size[l] ->
memo.accessor[l][n] = (at memo.accessor 'J)[l][n] }
(* All nodes under !p & before i are either null or marked black. *)
invariant { forall j. 0 <= j < i ->
let l = memo.accessor[!p][j] in l = null \/ black memo.colors[l] }
(* Unreachable/pre-marked blocks do not change. *)
invariant { forall l. l <> null ->
not path (at memo 'I) !p l \/ black (at memo.colors 'J)[l] ->
memo.colors[l] = (at memo.colors 'J)[l] }
'K:
aux g2; (* Explore sub-bloc. *)
body (); (* Swing to next sub-bloc. *)
assert { !t = (at memo.accessor 'K)[!p][i+1]
= (at memo.accessor 'J)[!p][i+1] }
done;
aux g2; (* Explore last sub-bloc. *)
body (); (* Pop. *)
end
end in
try aux (ghost empty); (* Explore main bloc *)
body (); (* Exit *)
absurd; (* Done. *)
with Stop ->
(* Need induction to recover path-based specification. *)
assert { forall x y m. m = at memo 'I /\ x <> null /\ y <> null /\
mem x graph /\ black memo.colors[x] ->
("induction" path m x y) -> black memo.colors[y] }
end
end
\ No newline at end of file
examples/schorr_waite_via_recursion/why3session.xml 0 → 100644
View file @ 90b5f914
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../schorr_waite_via_recursion.mlw" expanded="true">
<theory name="Memory" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="GraphShape" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="SchorrWaite" sum="5cdd637225548b2bcec592ea4db1065e" expanded="true">
<goal name="WP_parameter black" expl="VC for black">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="WP_parameter schorr_waite" expl="VC for schorr_waite">
<transf name="split_goal_wp">
<goal name="WP_parameter schorr_waite.1" expl="1. exceptional postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.2" expl="2. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.3" expl="3. exceptional postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.4" expl="4. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.5" expl="5. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.6" expl="6. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.7" expl="7. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.8" expl="8. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.9" expl="9. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.10" expl="10. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.11" expl="11. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.12" expl="12. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.13" expl="13. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.14" expl="14. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.15" expl="15. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.16" expl="16. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.17" expl="17. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.18" expl="18. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.19" expl="19. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.20" expl="20. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.21" expl="21. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.22" expl="22. unreachable point">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.23" expl="23. unreachable point">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.24" expl="24. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.25" expl="25. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.26" expl="26. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.27" expl="27. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.28" expl="28. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.29" expl="29. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.30" expl="30. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.31" expl="31. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.32" expl="32. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.33" expl="33. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.34" expl="34. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.35" expl="35. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.36" expl="36. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.37" expl="37. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.38" expl="38. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.39" expl="39. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.40" expl="40. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.41" expl="41. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.42" expl="42. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.43" expl="43. unreachable point">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.44" expl="44. unreachable point">
<proof prover="0"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.45" expl="45. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.46" expl="46. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.47" expl="47. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.48" expl="48. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.49" expl="49. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.50" expl="50. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.51" expl="51. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="14"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.52" expl="52. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.53" expl="53. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.54" expl="54. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="20"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.55" expl="55. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="20"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.56" expl="56. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.57" expl="57. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.58" expl="58. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.59" expl="59. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.60" expl="60. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.61" expl="61. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.62" expl="62. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="13"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.63" expl="63. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.64" expl="64. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.65" expl="65. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.66" expl="66. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.67" expl="67. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="39"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.68" expl="68. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.69" expl="69. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.70" expl="70. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.71" expl="71. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.72" expl="72. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.73" expl="73. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.74" expl="74. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.75" expl="75. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.76" expl="76. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.77" expl="77. postcondition">
<proof prover="0"><result status="valid" time="0.06" steps="57"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.78" expl="78. unreachable point">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.79" expl="79. unreachable point">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.80" expl="80. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.81" expl="81. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.82" expl="82. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.83" expl="83. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.84" expl="84. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.85" expl="85. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.86" expl="86. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.87" expl="87. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.88" expl="88. postcondition">
<proof prover="0"><result status="valid" time="0.03" steps="41"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.89" expl="89. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="24"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.90" expl="90. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.91" expl="91. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.92" expl="92. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.93" expl="93. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="20"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.94" expl="94. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="20"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.95" expl="95. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.96" expl="96. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.97" expl="97. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.98" expl="98. postcondition">
<proof prover="0"><result status="valid" time="0.07" steps="59"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.99" expl="99. unreachable point">
<proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.100" expl="100. unreachable point">
<proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.101" expl="101. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.102" expl="102. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.103" expl="103. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.104" expl="104. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.105" expl="105. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.106" expl="106. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.107" expl="107. postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.108" expl="108. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.109" expl="109. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter schorr_waite.110" expl="110. precondition">