Commit 9e9decde authored by Léon Gondelman's avatar Léon Gondelman

examples: random-access lists (minor fix)

parent 3b3244c9
......@@ -233,30 +233,31 @@ module RandomAccessListWithSeq
| Zero l1 -> let (_, x1) = lookup 0 l1 in One x1 (tail l1)
end
function aux (i: int) (f: 'a -> 'a) : ('a,'a) -> ('a, 'a) =
\ z. let (x,y) = z in if mod i 2 = 0 then (f x, y) else (x, f y)
function setf (s: seq 'a) (i:int) (f: 'a -> 'a) : seq 'a =
set s i (f s[i])
let rec fupdate_aux (f: 'a -> 'a) (i: int) (l: ral 'a) : ral 'a
function aux (i: int) (f: 'a -> 'a) : ('a,'a) -> ('a, 'a) =
\ z. let (x,y) = z in if mod i 2 = 0 then (f x, y) else (x, f y)
let rec fupdate (f: 'a -> 'a) (i: int) (l: ral 'a) : ral 'a
requires { 0 <= i < length (elements l) }
variant { i, l}
ensures { elements result == setf (elements l) i f}
= match l with
| Empty -> absurd
| One x l1 -> if i = 0 then One (f x) l1 else
cons x (fupdate_aux f (i-1) (Zero l1))
| Zero l1 -> Zero (fupdate_aux (aux i f) (div i 2) l1)
cons x (fupdate f (i-1) (Zero l1))
| Zero l1 -> Zero (fupdate (aux i f) (div i 2) l1)
end
function f (y: 'a) : 'a -> 'a = \ _. y
let fupdate (i:int) (y: 'a) (l: ral 'a) : ral 'a
let update (i:int) (y: 'a) (l: ral 'a) : ral 'a
requires { 0 <= i < length (elements l) }
ensures { elements result == set (elements l) i y}
= fupdate_aux (f y) i l
= fupdate (f y) i l
end
......@@ -164,7 +164,7 @@
<proof prover="0"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
</theory>
<theory name="RandomAccessListWithSeq" sum="fcb68ecfcb876f1501923453e0387c2d">
<theory name="RandomAccessListWithSeq" sum="270fa516a403a2453f40c174ff5ee8d1" expanded="true">
<goal name="WP_parameter size" expl="VC for size">
<transf name="split_goal_wp">
<goal name="WP_parameter size.1" expl="1. postcondition">
......@@ -225,36 +225,11 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter fupdate_aux" expl="VC for fupdate_aux">
<transf name="split_goal_wp">
<goal name="WP_parameter fupdate_aux.1" expl="1. unreachable point">
<proof prover="8" timelimit="5"><result status="valid" time="0.02" steps="7"/></proof>
</goal>
<goal name="WP_parameter fupdate_aux.2" expl="2. postcondition">
<proof prover="8" timelimit="5"><result status="valid" time="0.05" steps="99"/></proof>
</goal>
<goal name="WP_parameter fupdate_aux.3" expl="3. variant decrease">
<proof prover="8" timelimit="5"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
<goal name="WP_parameter fupdate_aux.4" expl="4. precondition">
<proof prover="8" timelimit="5"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="WP_parameter fupdate_aux.5" expl="5. postcondition">
<proof prover="8" timelimit="5"><result status="valid" time="0.08" steps="115"/></proof>
</goal>
<goal name="WP_parameter fupdate_aux.6" expl="6. variant decrease">
<proof prover="8" timelimit="5"><result status="valid" time="0.04" steps="29"/></proof>
</goal>
<goal name="WP_parameter fupdate_aux.7" expl="7. precondition">
<proof prover="8" timelimit="5"><result status="valid" time="0.06" steps="31"/></proof>
</goal>
<goal name="WP_parameter fupdate_aux.8" expl="8. postcondition">
<proof prover="8" timelimit="5"><result status="valid" time="5.33" steps="559"/></proof>
</goal>
</transf>
<goal name="WP_parameter fupdate" expl="VC for fupdate" expanded="true">
<proof prover="0"><result status="valid" time="3.77" steps="1222"/></proof>
</goal>
<goal name="WP_parameter fupdate" expl="VC for fupdate">
<proof prover="0"><result status="valid" time="0.03" steps="16"/></proof>
<goal name="WP_parameter update" expl="VC for update">
<proof prover="8" timelimit="5"><result status="valid" time="0.02" steps="16"/></proof>
</goal>
</theory>
</file>
......
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