random_access_list: with sequences instead of lists

parent 6c0dd217
......@@ -125,3 +125,57 @@ module RAL
end
module RandomAccessListWithSeq
use import int.Int
use import int.ComputerDivision
use import seq.Seq
type ral 'a =
| Empty
| Zero (ral ('a, 'a))
| One 'a (ral ('a, 'a))
function flatten (s: seq ('a, 'a)) : seq 'a
= create (2 * length s)
(\ i: int. let (x0, x1) = s[div i 2] in
if mod i 2 = 0 then x0 else x1)
function elements (l: ral 'a) : seq 'a
= match l with
| Empty -> empty
| Zero l1 -> flatten (elements l1)
| One x l1 -> cons x (flatten (elements l1))
end
let rec size (l: ral 'a) : int
variant { l }
ensures { result = length (elements l) }
=
match l with
| Empty -> 0
| Zero l1 -> 2 * size l1
| One _ l1 -> 1 + 2 * size l1
end
let rec add (x: 'a) (l: ral 'a) : ral 'a
variant { l }
ensures { elements result == cons x (elements l) }
= match l with
| Empty -> One x Empty
| Zero l1 -> One x l1
| One y l1 -> Zero (add (x, y) l1)
end
let rec get (i: int) (l: ral 'a) : 'a
requires { 0 <= i < length (elements l) }
variant { i, l }
ensures { (elements l)[i] = result }
= match l with
| Empty -> absurd
| One x l1 -> if i = 0 then x else get (i-1) (Zero l1)
| Zero l1 -> let (x0, x1) = get (div i 2) l1 in
if mod i 2 = 0 then x0 else x1
end
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="3" name="Z3" version="4.3.2" timelimit="6" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.3" timelimit="1" memlimit="1000"/>
<file name="../random_access_list.mlw" expanded="true">
<theory name="RandomAccessList" sum="d952bd09a31c38ca601c47b7856a5416" expanded="true">
......@@ -64,5 +65,16 @@
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
</theory>
<theory name="RandomAccessListWithSeq" sum="2b4baed53359c844adc5f3be28250dd8" expanded="true">
<goal name="WP_parameter size" expl="VC for size" expanded="true">
<proof prover="0"><result status="valid" time="0.08" steps="78"/></proof>
</goal>
<goal name="WP_parameter add" expl="VC for add" expanded="true">
<proof prover="3"><result status="valid" time="1.34"/></proof>
</goal>
<goal name="WP_parameter get" expl="VC for get" expanded="true">
<proof prover="0"><result status="valid" time="1.62" steps="406"/></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