library: fixed array.ToList, added array.ToSeq

parent 6d59bb6c
......@@ -7,7 +7,8 @@
<prover id="2" name="CVC4" version="1.3" timelimit="6" steplimit="1" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="10" steplimit="1" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="10" steplimit="1" memlimit="1000"/>
<file name="../cursor.mlw">
<prover id="5" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<file name="../cursor.mlw" expanded="true">
<theory name="Cursor" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestCursor" sum="4a864b2c874ceb1b6d23670c5e40f80b">
......@@ -100,9 +101,9 @@
</transf>
</goal>
</theory>
<theory name="IntArrayCursor" sum="b0842edc620996a629ec35b7446b1834">
<goal name="WP_parameter create" expl="VC for create">
<proof prover="1"><result status="valid" time="0.01" steps="14"/></proof>
<theory name="IntArrayCursor" sum="8090cb9a5eb720659015e09ae27d5ddf" expanded="true">
<goal name="WP_parameter create" expl="VC for create" expanded="true">
<proof prover="5"><result status="valid" time="0.05" steps="15"/></proof>
</goal>
<goal name="WP_parameter has_next" expl="VC for has_next">
<proof prover="0"><result status="valid" time="0.01"/></proof>
......
......@@ -296,6 +296,28 @@ module ToList
to_list a l u = Cons a[l] (to_list a (l+1) u)
val to_list (a: array 'a) (l u: int) : list 'a
ensures { result = to_list a l u }
requires { 0 <= l && u <= length a }
ensures { result = to_list a l u }
end
module ToSeq
use import int.Int
use import Array
use seq.Seq as S
function to_seq (a: array 'a) (l u: int) : S.seq 'a
axiom to_seq_empty:
forall a: array 'a, l u: int. u <= l ->
to_seq a l u = S.empty
axiom to_seq_cons:
forall a: array 'a, l u: int. l < u ->
to_seq a l u = S.cons a[l] (to_seq a (l+1) u)
val to_seq (a: array 'a) (l u: int) : S.seq 'a
requires { 0 <= l && u <= length a }
ensures { result = to_seq a l u }
end
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