mach.array.ArrayInt63: added init and sub

parent 892f05d5
......@@ -485,10 +485,12 @@ end
module mach.array.ArrayInt63
syntax type array63 "(int array)"
syntax val make "Array.make"
syntax val init "Array.init"
syntax val ([]) "%1.(%2)" prec 2 1 18
syntax val ([]<-) "%1.(%2) <- %3" prec 15 1 18 15
syntax val length "Array.length %1" prec 4 3
syntax val copy "Array.copy"
syntax val sub "Array.sub"
end
module mach.matrix.Matrix63
......
......@@ -453,6 +453,18 @@ module ArrayInt63
ensures { result.length = a.length }
ensures { forall i. 0 <= i < result.length -> result[i] = a[i] }
let sub (a: array63) (ofs: int63) (len: int63) : array63
requires { 0 <= ofs /\ 0 <= len /\ ofs + len <= length a }
ensures { length result = len }
ensures { forall i. 0 <= i < len -> result[i] = a[ofs + i] }
=
let b = make len 0 in
for i = 0 to len - 1 do
invariant { forall k. 0 <= k < i -> b[k] = a[ofs+k] }
b[i] <- a[ofs + i];
done;
b
use seq.Exchange
let swap (a:array63) (i j:int63) : unit
......@@ -463,4 +475,16 @@ module ArrayInt63
a[i] <- a[j];
a[j] <- v
let init (n: int63) (f: int63 -> int63) : array63
requires { [@expl:array creation size] n >= 0 }
ensures { forall i: int63. 0 <= i < n -> result[i] = f i }
ensures { length result = n }
=
let a = make n 0 in
for i = 0 to n - 1 do
invariant { forall k: int63. 0 <= k < i -> a[k] = f k }
a[i] <- f i
done;
a
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