Commit 37fa5ab1 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

cursors: experiments in progress

parent b3937b40
......@@ -12,8 +12,10 @@
identical to to_do
*)
module IterableList
use import list.List
module Cursor
use import int.Int
use import seq.Seq
type t
(** the collection *)
......@@ -21,28 +23,26 @@ module IterableList
(** the type of its elements *)
type cursor = private {
mutable ghost done_: list elt; (** already processed *)
mutable ghost to_do: list elt; (** yet to be processed *)
ghost seq: seq elt;
mutable ghost i : int;
}
predicate coherent t cursor
val create (t: t) : cursor
ensures { result.done_ = Nil }
ensures { result.i = 0 }
ensures { coherent t result }
val has_next (t: t) (c: cursor) : bool
val has_next (ghost t: t) (c: cursor) : bool
requires { coherent t c }
ensures { result <-> c.to_do <> Nil }
ensures { result <-> 0 <= c.i < length c.seq }
val next (t: t) (c: cursor) : elt
requires { c.to_do <> Nil }
val next (ghost t: t) (c: cursor) : elt
requires { coherent t c }
requires { 0 <= c.i < length c.seq }
writes { c }
ensures { match old c.to_do with
| Nil -> false
| Cons x l -> result = x /\ c.done_ = Cons x (old c.done_) /\
c.to_do = l end }
ensures { result = c.seq[old c.i] }
ensures { c.i = old c.i + 1 }
ensures { coherent t c }
end
......@@ -50,24 +50,25 @@ end
module TestCursor
use import int.Int
use import list.List
use import list.Length
use import list.Sum
use import int.Sum
use import seq.Seq
use import ref.Refint
clone import IterableList with type elt = int
clone import Cursor with type elt = int
(** sums all the remaining elements in the cursor *)
let sum (t: t) (c: cursor) : int
requires { coherent t c }
ensures { result = old (sum c.to_do) }
requires { c.i = 0 }
ensures { result = sum 0 (length c.seq - 1) (get c.seq) }
=
let s = ref 0 in
'I:
while has_next t c do
invariant { at (sum c.to_do) 'I = !s + sum c.to_do }
invariant { coherent t c }
variant { length c.to_do }
invariant { 0 <= c.i <= length c.seq }
invariant { !s = sum 0 (c.i - 1) (get c.seq) }
variant { length c.seq - c.i }
let x = next t c in
s += x
done;
......@@ -150,7 +151,7 @@ module TestListCursor
end
(** {2 Iteration over a muable collection}
(** {2 Iteration over a mutable collection}
here we choose an array of integers *)
......@@ -244,4 +245,21 @@ module TestArrayCursor
done;
!s
let harness1 () : unit
=
let a = Array.make 42 0 in
let c = create a in
let x = next a c in
assert { x = 0 }
(*
let harness2 () : unit
=
let a = Array.make 42 0 in
let c = create a in
a[1] <- 17;
let x = next a c in
assert { x = 0 }
*)
end
......@@ -5,38 +5,53 @@
<prover id="0" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.3" timelimit="6" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="10" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="10" memlimit="1000"/>
<file name="../cursor.mlw" expanded="true">
<theory name="IterableList" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<theory name="Cursor" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="TestCursor" sum="333c008a98d32cd755d2ab198a3820d0" expanded="true">
<theory name="TestCursor" sum="176c55ab5c9e377bb55c280a95c35887" expanded="true">
<goal name="WP_parameter sum" expl="VC for sum" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter sum.1" expl="1. loop invariant init">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="2"/></proof>
<proof prover="3"><result status="valid" time="0.04" steps="2"/></proof>
</goal>
<goal name="WP_parameter sum.2" expl="2. loop invariant init">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="3"/></proof>
</goal>
<goal name="WP_parameter sum.3" expl="3. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter sum.3" expl="3. loop invariant init" expanded="true">
<proof prover="3"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="WP_parameter sum.4" expl="4. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter sum.5" expl="5. precondition">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter sum.6" expl="6. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.00"/></proof>
<goal name="WP_parameter sum.6" expl="6. precondition">
<proof prover="1"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
<goal name="WP_parameter sum.7" expl="7. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="WP_parameter sum.8" expl="8. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<goal name="WP_parameter sum.8" expl="8. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.02" steps="11"/></proof>
</goal>
<goal name="WP_parameter sum.9" expl="9. postcondition" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<goal name="WP_parameter sum.9" expl="9. loop invariant preservation">
<proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="WP_parameter sum.10" expl="10. loop variant decrease">
<proof prover="1"><result status="valid" time="0.02" steps="11"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter sum.11" expl="11. postcondition" expanded="true">
<proof prover="3"><result status="valid" time="0.02" steps="8"/></proof>
</goal>
</transf>
</goal>
......@@ -126,7 +141,7 @@
</transf>
</goal>
</theory>
<theory name="TestArrayCursor" sum="1818e28aa2ccadd10a21d99b8b296439">
<theory name="TestArrayCursor" sum="1e7488f16d72fe3b07df3520264bcf37" expanded="true">
<goal name="WP_parameter array_sum_array_to_list" expl="VC for array_sum_array_to_list">
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -161,6 +176,29 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter harness1" expl="VC for harness1" expanded="true">
<proof prover="4"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="WP_parameter harness2" expl="VC for harness2" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter harness2.1" expl="1. array creation size">
<proof prover="3"><result status="valid" time="0.03" steps="1"/></proof>
</goal>
<goal name="WP_parameter harness2.2" expl="2. index in array bounds">
<proof prover="3"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="WP_parameter harness2.3" expl="3. precondition" expanded="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter harness2.4" expl="4. precondition" expanded="true">
<proof prover="3"><result status="timeout" time="9.98"/></proof>
<proof prover="4"><result status="timeout" time="11.01"/></proof>
</goal>
<goal name="WP_parameter harness2.5" expl="5. assertion" expanded="true">
<proof prover="4"><result status="valid" time="0.28"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment