random_access_list: cosmetic changes

parent f0b03465
......@@ -74,7 +74,6 @@ module RandomAccessList
| Cons _ r -> if i > 0 then nth_flatten (i-1) r
end
let rec get (i: int) (l: ral 'a) : 'a
requires { 0 <= i < length (elements l) }
variant { i, l }
......@@ -86,22 +85,20 @@ module RandomAccessList
if mod i 2 = 0 then x0 else x1
end
let rec tail (l: ral 'a) : ral 'a
let rec tail (l: ral 'a) : ral 'a
requires { elements l <> Nil }
variant { l }
ensures {let m = elements l in
match nth 0 m with
| None -> false
| Some x -> m = Cons x (elements result)
end }
variant { l }
ensures { match elements l with
| Nil -> false
| Cons _ l -> elements result = l
end }
= match l with
| Empty -> absurd
| One _ l1 -> Zero l1
| Zero l1 -> let (_, x1) = get 0 l1 in One x1 (tail l1)
end
let rec set (y: 'a) (i: int) (l: ral 'a) : ral 'a
let rec set (i: int) (y: 'a) (l: ral 'a) : ral 'a
requires { 0 <= i < length (elements l) }
variant { i, l}
ensures { nth i (elements result) = Some y}
......@@ -115,13 +112,13 @@ module RandomAccessList
= match l with
| Empty -> absurd
| One x l1 -> if i = 0 then One y l1 else
match set y (i-1) (Zero l1) with
match set (i-1) y (Zero l1) with
| Empty | One _ _ -> absurd
| Zero l1 -> One x l1
end
| Zero l1 ->
let (x0, x1) = get (div i 2) l1 in
let l1' = set (if mod i 2 = 0 then (y,x1) else (x0,y)) (div i 2) l1 in
let l1' = set (div i 2) (if mod i 2 = 0 then (y,x1) else (x0,y)) l1 in
assert { forall j. 0 <= j < length (elements l) -> j <> i ->
match nth (div j 2) (elements l1) with
| None -> false
......@@ -171,6 +168,8 @@ module RAL
end
(** Model using sequences instead of lists *)
module RandomAccessListWithSeq
use import int.Int
......@@ -213,7 +212,7 @@ module RandomAccessListWithSeq
| One y l1 -> Zero (add (x, y) l1)
end
let rec get (i: int) (l: ral 'a) : 'a
let rec get (i: int) (l: ral 'a) : 'a
requires { 0 <= i < length (elements l) }
variant { i, l }
ensures { (elements l)[i] = result }
......@@ -225,29 +224,30 @@ module RandomAccessListWithSeq
end
let rec tail (l: ral 'a) : ral 'a
requires { not ((elements l) == empty) }
variant { l }
ensures { (elements l) == cons (elements l)[0] (elements result) }
requires { 0 < length (elements l) }
variant { l }
ensures { elements result == (elements l)[1 .. ] }
= match l with
| Empty -> absurd
| One _ l1 -> Zero l1
| Zero l1 -> let (_, x1) = get 0 l1 in One x1 (tail l1)
end
let rec set (y: 'a) (i: int) (l: ral 'a) : ral 'a
let rec set (i: int) (y: 'a) (l: ral 'a) : ral 'a
requires { 0 <= i < length (elements l) }
variant { i, l}
ensures { elements result == set (elements l) i y}
= match l with
| Empty -> absurd
| One x l1 -> if i = 0 then One y l1 else
match set y (i-1) (Zero l1) with
| Empty | One _ _ -> absurd
| Zero l1 -> One x l1
end
| Zero l1 -> let (x0, x1) = get (div i 2) l1 in
Zero
(set (if mod i 2 = 0 then (y,x1) else (x0,y)) (div i 2) l1)
| One x l1 ->
if i = 0 then One y l1 else
match set (i-1) y (Zero l1) with
| Empty | One _ _ -> absurd
| Zero l1 -> One x l1
end
| Zero l1 ->
let (x0, x1) = get (div i 2) l1 in
Zero (set (div i 2) (if mod i 2 = 0 then (y,x1) else (x0,y)) l1)
end
end
......@@ -7,8 +7,8 @@
<prover id="4" name="Z3" version="4.3.1" timelimit="10" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.3" timelimit="1" memlimit="1000"/>
<prover id="8" name="Alt-Ergo" version="0.95.2" timelimit="15" memlimit="1000"/>
<file name="../random_access_list.mlw" expanded="true">
<theory name="RandomAccessList" sum="10f317f24c1421f793cea88f1312650d" expanded="true">
<file name="../random_access_list.mlw">
<theory name="RandomAccessList" sum="d27743d57c1d4ea4700ca93cff755188">
<goal name="WP_parameter length_flatten" expl="VC for length_flatten">
<transf name="split_goal_wp">
<goal name="WP_parameter length_flatten.1" expl="1. variant decrease">
......@@ -51,7 +51,26 @@
<proof prover="0"><result status="valid" time="0.34" steps="410"/></proof>
</goal>
<goal name="WP_parameter tail" expl="VC for tail">
<proof prover="8"><result status="valid" time="0.12" steps="271"/></proof>
<transf name="split_goal_wp">
<goal name="WP_parameter tail.1" expl="1. unreachable point">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="WP_parameter tail.2" expl="2. postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="34"/></proof>
</goal>
<goal name="WP_parameter tail.3" expl="3. precondition">
<proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
</goal>
<goal name="WP_parameter tail.4" expl="4. variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter tail.5" expl="5. precondition">
<proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter tail.6" expl="6. postcondition">
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter set" expl="VC for set">
<transf name="split_goal_wp">
......@@ -59,7 +78,7 @@
<proof prover="8" timelimit="5"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter set.2" expl="2. postcondition">
<proof prover="8" timelimit="5"><result status="valid" time="0.02" steps="22"/></proof>
<proof prover="8" timelimit="10"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter set.3" expl="3. postcondition">
<proof prover="8" timelimit="5"><result status="valid" time="0.02" steps="46"/></proof>
......@@ -86,7 +105,7 @@
<proof prover="8" timelimit="5"><result status="valid" time="0.03" steps="38"/></proof>
</goal>
<goal name="WP_parameter set.11" expl="11. postcondition">
<proof prover="8" timelimit="5"><result status="valid" time="0.04" steps="99"/></proof>
<proof prover="8" timelimit="10"><result status="valid" time="0.02" steps="99"/></proof>
</goal>
<goal name="WP_parameter set.12" expl="12. postcondition">
<proof prover="8" timelimit="5"><result status="valid" time="0.03" steps="60"/></proof>
......@@ -117,10 +136,10 @@
</transf>
</goal>
<goal name="WP_parameter set.18" expl="18. postcondition">
<proof prover="8" timelimit="10"><result status="valid" time="0.87" steps="511"/></proof>
<proof prover="8" timelimit="5"><result status="valid" time="0.87" steps="511"/></proof>
</goal>
<goal name="WP_parameter set.19" expl="19. postcondition">
<proof prover="8" timelimit="10"><result status="valid" time="0.02" steps="17"/></proof>
<proof prover="8" timelimit="5"><result status="valid" time="0.04" steps="17"/></proof>
</goal>
<goal name="WP_parameter set.20" expl="20. postcondition">
<proof prover="8" timelimit="10"><result status="valid" time="0.03" steps="94"/></proof>
......@@ -145,7 +164,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
</theory>
<theory name="RandomAccessListWithSeq" sum="0a2ddaba4620ea7f427c7e1c523e87b5" expanded="true">
<theory name="RandomAccessListWithSeq" sum="98a44fae0089720a7e399a74aaafb1d9">
<goal name="WP_parameter size" expl="VC for size">
<transf name="split_goal_wp">
<goal name="WP_parameter size.1" expl="1. postcondition">
......@@ -212,22 +231,22 @@
<goal name="WP_parameter tail" expl="VC for tail">
<transf name="split_goal_wp">
<goal name="WP_parameter tail.1" expl="1. unreachable point">
<proof prover="8"><result status="valid" time="0.03" steps="8"/></proof>
<proof prover="8"><result status="valid" time="0.03" steps="6"/></proof>
</goal>
<goal name="WP_parameter tail.2" expl="2. postcondition">
<proof prover="8"><result status="valid" time="0.05" steps="75"/></proof>
<proof prover="8"><result status="valid" time="0.04" steps="68"/></proof>
</goal>
<goal name="WP_parameter tail.3" expl="3. precondition">
<proof prover="8"><result status="valid" time="0.02" steps="26"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
<goal name="WP_parameter tail.4" expl="4. variant decrease">
<proof prover="8"><result status="valid" time="0.03" steps="34"/></proof>
<proof prover="8"><result status="valid" time="0.03" steps="25"/></proof>
</goal>
<goal name="WP_parameter tail.5" expl="5. precondition">
<proof prover="8"><result status="valid" time="0.02" steps="7"/></proof>
<proof prover="8"><result status="valid" time="0.02" steps="5"/></proof>
</goal>
<goal name="WP_parameter tail.6" expl="6. postcondition">
<proof prover="8"><result status="valid" time="6.13" steps="521"/></proof>
<proof prover="8"><result status="valid" time="4.78" steps="526"/></proof>
</goal>
</transf>
</goal>
......@@ -264,7 +283,7 @@
<proof prover="8"><result status="valid" time="0.02" steps="6"/></proof>
</goal>
<goal name="WP_parameter set.11" expl="11. postcondition">
<proof prover="8"><result status="valid" time="2.39" steps="610"/></proof>
<proof prover="8"><result status="valid" time="1.71" steps="610"/></proof>
</goal>
</transf>
</goal>
......
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