flexible arrays: more efficient implementation, with O(1) length

parent 24f9c218
......@@ -33,24 +33,23 @@ module FlexibleArray
| Node l _ r -> (size l = size r || size l = size r + 1) && inv l && inv r
end
let empty () : tree 'a
ensures { inv result }
ensures { size result = 0 }
= Empty
let length (t: tree 'a) : int
requires { inv t }
ensures { result = size t }
=
size t
let is_empty (t: tree 'a) : bool
requires { inv t }
ensures { result <-> size t = 0 }
type t 'a = {
length: int;
tree: tree 'a;
} invariant {
length = size tree && inv tree
}
let empty () : t 'a
ensures { result.length = 0 }
= { length = 0; tree = Empty }
let is_empty (t: t 'a) : bool
ensures { result <-> t.length = 0 }
=
match t with Empty -> True | Node _ _ _ -> False end
t.length = 0
let rec function get (t: tree 'a) (i: int) : 'a
let rec function get_aux (t: tree 'a) (i: int) : 'a
requires { 0 <= i < size t }
requires { inv t }
variant { t }
......@@ -58,52 +57,79 @@ module FlexibleArray
| Empty -> absurd
| Node l x r ->
if i = 0 then x
else if mod i 2 = 1 then get l (div i 2) else get r (div i 2 - 1)
else if mod i 2 = 1 then get_aux l (div i 2) else get_aux r (div i 2 - 1)
end
let rec set (t: tree 'a) (i: int) (v: 'a) : tree 'a
let function get (t: t 'a) (i: int) : 'a
requires { 0 <= i < t.length }
= get_aux t.tree i
let rec set_aux (t: tree 'a) (i: int) (v: 'a) : tree 'a
requires { 0 <= i < size t }
requires { inv t }
variant { t }
ensures { inv result }
ensures { size result = size t }
ensures { forall j. 0 <= j < size t -> j <> i -> get result j = get t j }
ensures { get result i = v }
ensures { forall j. 0 <= j < size t -> j <> i ->
get_aux result j = get_aux t j }
ensures { get_aux result i = v }
= match t with
| Empty -> absurd
| Node l x r ->
if i = 0 then Node l v r
else if mod i 2 = 1 then Node (set l (div i 2) v) x r
else Node l x (set r (div i 2 - 1) v)
else if mod i 2 = 1 then Node (set_aux l (div i 2) v) x r
else Node l x (set_aux r (div i 2 - 1) v)
end
let set (t: t 'a) (i: int) (v: 'a) : t 'a
requires { 0 <= i < t.length }
ensures { result.length = t.length }
ensures { forall j. 0 <= j < t.length -> j <> i -> get result j = get t j }
ensures { get result i = v }
= { length = t.length; tree = set_aux t.tree i v }
(* low extension *)
let rec le (v: 'a) (t: tree 'a) : tree 'a
let rec le_aux (v: 'a) (t: tree 'a) : tree 'a
requires { inv t }
variant { t }
ensures { inv result }
ensures { size result = size t + 1 }
ensures { get result 0 = v }
ensures { forall j. 0 <= j < size t -> get result (j + 1) = get t j }
ensures { get_aux result 0 = v }
ensures { forall j. 0 <= j < size t ->
get_aux result (j + 1) = get_aux t j }
= match t with
| Empty -> Node Empty v Empty
| Node l x r -> Node (le x r) v l
| Node l x r -> Node (le_aux x r) v l
end
let rec le (v: 'a) (t: t 'a) : t 'a
ensures { result.length = t.length + 1 }
ensures { get result 0 = v }
ensures { forall j. 0 <= j < t.length -> get result (j + 1) = get t j }
= { length = t.length + 1; tree = le_aux v t.tree }
(* low removal *)
let rec lr (t: tree 'a) : tree 'a
let rec lr_aux (t: tree 'a) : tree 'a
requires { inv t }
requires { size t > 0 }
variant { t }
ensures { inv result }
ensures { size result = size t - 1 }
ensures { forall j. 0 <= j < size result -> get result j = get t (j + 1) }
ensures { forall j. 0 <= j < size result ->
get_aux result j = get_aux t (j + 1) }
= match t with
| Empty -> absurd
| Node Empty _ Empty -> Empty
| Node l _ r -> Node r (get l 0) (lr l)
| Node l _ r -> Node r (get_aux l 0) (lr_aux l)
end
let lr (t: t 'a) : t 'a
requires { t.length > 0 }
ensures { result.length = t.length - 1 }
ensures { forall j. 0 <= j < result.length ->
get result j = get t (j + 1) }
= { length = t.length - 1; tree = lr_aux t.tree }
(* high extension *)
let rec he_aux (s: int) (t: tree 'a) (v: 'a) : tree 'a
requires { inv t }
......@@ -111,22 +137,20 @@ module FlexibleArray
variant { t }
ensures { inv result }
ensures { size result = size t + 1 }
ensures { get result (size t) = v }
ensures { forall j. 0 <= j < size t -> get result j = get t j }
ensures { get_aux result (size t) = v }
ensures { forall j. 0 <= j < size t -> get_aux result j = get_aux t j }
= match t with
| Empty -> Node Empty v Empty
| Node l x r -> if mod s 2 = 1 then Node (he_aux (div s 2) l v) x r
else Node l x (he_aux (div s 2 - 1) r v)
end
let he (t: tree 'a) (v: 'a) : tree 'a
requires { inv t }
ensures { inv result }
ensures { size result = size t + 1 }
ensures { get result (size t) = v }
ensures { forall j. 0 <= j < size t -> get result j = get t j }
let he (t: t 'a) (v: 'a) : t 'a
ensures { result.length = t.length + 1 }
ensures { get result t.length = v }
ensures { forall j. 0 <= j < t.length -> get result j = get t j }
=
he_aux (size t) t v
{ length = t.length + 1; tree = he_aux t.length t.tree v }
(* high removal *)
let rec hr_aux (s: int) (t: tree 'a) : tree 'a
......@@ -135,7 +159,8 @@ module FlexibleArray
variant { t }
ensures { inv result }
ensures { size result = size t - 1 }
ensures { forall j. 0 <= j < size result -> get result j = get t j }
ensures { forall j. 0 <= j < size result ->
get_aux result j = get_aux t j }
= match t with
| Empty -> absurd
| Node Empty _ Empty -> Empty
......@@ -143,13 +168,11 @@ module FlexibleArray
else Node l x (hr_aux (div s 2) r)
end
let hr (t: tree 'a) : tree 'a
requires { inv t }
requires { size t > 0 }
ensures { inv result }
ensures { size result = size t - 1 }
ensures { forall j. 0 <= j < size result -> get result j = get t j }
let hr (t: t 'a) : t 'a
requires { t.length > 0 }
ensures { result.length = t.length - 1 }
ensures { forall j. 0 <= j < result.length -> get result j = get t j }
=
hr_aux (size t) t
{ length = t.length - 1; tree = hr_aux t.length t.tree }
end
......@@ -4,39 +4,48 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<file name="../flexible_array.mlw" expanded="true">
<theory name="FlexibleArray" sum="5b3c6d4d053c044616fe54c5db5db770" expanded="true">
<theory name="FlexibleArray" sum="0ddc089b49190005c467c06361e9bd32" expanded="true">
<goal name="VC empty" expl="VC for empty" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="VC length" expl="VC for length" expanded="true">
<proof prover="0"><result status="valid" time="0.00" steps="0"/></proof>
</goal>
<goal name="VC is_empty" expl="VC for is_empty" expanded="true">
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="0"/></proof>
</goal>
<goal name="VC get_aux" expl="VC for get_aux" expanded="true">
<proof prover="0" steplimit="-1"><result status="valid" time="0.04" steps="110"/></proof>
</goal>
<goal name="VC get" expl="VC for get" expanded="true">
<proof prover="0"><result status="valid" time="0.05" steps="110"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="5"/></proof>
</goal>
<goal name="VC set_aux" expl="VC for set_aux" expanded="true">
<proof prover="0" steplimit="-1"><result status="valid" time="0.47" steps="742"/></proof>
</goal>
<goal name="VC set" expl="VC for set" expanded="true">
<proof prover="0"><result status="valid" time="0.52" steps="742"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="44"/></proof>
</goal>
<goal name="VC le_aux" expl="VC for le_aux" expanded="true">
<proof prover="0" steplimit="-1"><result status="valid" time="0.39" steps="521"/></proof>
</goal>
<goal name="VC le" expl="VC for le" expanded="true">
<proof prover="0"><result status="valid" time="0.33" steps="521"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="38"/></proof>
</goal>
<goal name="VC lr_aux" expl="VC for lr_aux" expanded="true">
<proof prover="0" steplimit="-1"><result status="valid" time="1.64" steps="1162"/></proof>
</goal>
<goal name="VC lr" expl="VC for lr" expanded="true">
<proof prover="0" steplimit="-1"><result status="valid" time="1.56" steps="1162"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="30"/></proof>
</goal>
<goal name="VC he_aux" expl="VC for he_aux" expanded="true">
<proof prover="0" steplimit="-1"><result status="valid" time="0.41" steps="607"/></proof>
<proof prover="0"><result status="valid" time="0.41" steps="607"/></proof>
</goal>
<goal name="VC he" expl="VC for he" expanded="true">
<proof prover="0" steplimit="-1"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="36"/></proof>
</goal>
<goal name="VC hr_aux" expl="VC for hr_aux" expanded="true">
<proof prover="0" steplimit="-1"><result status="valid" time="0.65" steps="826"/></proof>
<proof prover="0"><result status="valid" time="0.65" steps="826"/></proof>
</goal>
<goal name="VC hr" expl="VC for hr" expanded="true">
<proof prover="0" steplimit="-1"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="0"><result status="valid" time="0.00" steps="30"/></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