random_access_list: trivial encapsulation

in anticipation of future module refinement
parent 72e24dba
......@@ -83,3 +83,42 @@ module RandomAccessList
end
end
(** A straightforward encapsulation with a list ghost model
(in anticipation of module refinement) *)
module RAL
use import int.Int
use import RandomAccessList as R
use import list.List
use import list.Length
use import option.Option
use import list.Nth
type t 'a = { r: ral 'a; ghost l: list 'a }
invariant { self.l = elements self.r }
let empty () : t 'a
ensures { result.l = Nil }
=
{ r = Empty; l = Nil }
let size (t: t 'a) : int
ensures { result = length t.l }
=
size t.r
let cons (x: 'a) (s: t 'a) : t 'a
ensures { result.l = Cons x s.l }
=
{ r = add x s.r; l = Cons x s.l }
let get (i: int) (s: t 'a) : 'a
requires { 0 <= i < length s.l }
ensures { Some result = nth i s.l }
=
get i s.r
end
......@@ -4,6 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="6" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.95.1" timelimit="6" memlimit="1000"/>
<prover id="5" name="Coq" version="8.4pl2" timelimit="6" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.3" timelimit="1" memlimit="1000"/>
<file name="../random_access_list.mlw" expanded="true">
......@@ -41,5 +42,19 @@
<proof prover="0"><result status="valid" time="0.34" steps="410"/></proof>
</goal>
</theory>
<theory name="RAL" sum="ef67f0d6811c1a4189d9e2bd83248eb7" expanded="true">
<goal name="WP_parameter empty" expl="VC for empty" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="WP_parameter size" expl="VC for size" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="1"/></proof>
</goal>
<goal name="WP_parameter cons" expl="VC for cons" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter get" expl="VC for get" expanded="true">
<proof prover="2"><result status="valid" time="0.01" steps="7"/></proof>
</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