Commit fc68f4f7 authored by Martin Clochard's avatar Martin Clochard

Added opaque annotations on arrays/maps for output type.

parent 7f61ab4d
......@@ -15,24 +15,24 @@ module Array
type array 'a model { length : int; mutable elts : map int 'a }
invariant { 0 <= self.length }
function get (a: array 'a) (i: int) : 'a = M.get a.elts i
function get (a: array ~'a) (i: int) : 'a = M.get a.elts i
function set (a: array 'a) (i: int) (v: 'a) : array 'a =
function set (a: array ~'a) (i: int) (v: 'a) : array 'a =
{ a with elts = M.set a.elts i v }
(** syntactic sugar *)
function ([]) (a: array 'a) (i: int) : 'a = get a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
val ([]) (a: array 'a) (i: int) : 'a
val ([]) (a: array ~'a) (i: int) : 'a
requires { 0 <= i < length a }
ensures { result = a[i] }
val ([]<-) (a: array 'a) (i: int) (v: 'a) : unit writes {a}
val ([]<-) (a: array ~'a) (i: int) (v: 'a) : unit writes {a}
requires { 0 <= i < length a }
ensures { a.elts = M.set (old a.elts) i v }
val length (a: array 'a) : int ensures { result = a.length }
val length (a: array ~'a) : int ensures { result = a.length }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
......@@ -49,28 +49,28 @@ module Array
= if i < 0 || i >= length a then raise OutOfBounds;
a[i] <- v
function make (n: int) (v: 'a) : array 'a =
function make (n: int) (v: ~'a) : array 'a =
{ length = n; elts = M.const v }
val make (n: int) (v: 'a) : array 'a
val make (n: int) (v: ~'a) : array 'a
requires { n >= 0 } ensures { result = make n v }
val append (a1: array 'a) (a2: array 'a) : array 'a
val append (a1: array ~'a) (a2: array 'a) : array 'a
ensures { length result = length a1 + length a2 }
ensures { forall i:int. 0 <= i < length a1 -> result[i] = a1[i] }
ensures {
forall i:int. 0 <= i < length a2 -> result[length a1 + i] = a2[i] }
val sub (a: array 'a) (ofs: int) (len: int) : array 'a
val sub (a: array ~'a) (ofs: int) (len: int) : array 'a
requires { 0 <= ofs /\ 0 <= len /\ ofs + len <= length a }
ensures { length result = len }
ensures { forall i:int. 0 <= i < len -> result[i] = a[ofs + i] }
val copy (a: array 'a) : array 'a
val copy (a: array ~'a) : array 'a
ensures { length result = length a }
ensures { forall i:int. 0 <= i < length result -> result[i] = a[i] }
let fill (a: array 'a) (ofs: int) (len: int) (v: 'a)
let fill (a: array ~'a) (ofs: int) (len: int) (v: 'a)
requires { 0 <= ofs /\ 0 <= len /\ ofs + len <= length a }
ensures { forall i:int.
(0 <= i < ofs \/ ofs + len <= i < length a) -> a[i] = (old a)[i] }
......@@ -83,7 +83,7 @@ module Array
a[ofs + k] <- v
done
val blit (a1: array 'a) (ofs1: int)
val blit (a1: array ~'a) (ofs1: int)
(a2: array 'a) (ofs2: int) (len: int) : unit writes {a2}
requires { 0 <= ofs1 /\ 0 <= len /\ ofs1 + len <= length a1 }
requires { 0 <= ofs2 /\ ofs2 + len <= length a2 }
......@@ -92,7 +92,7 @@ module Array
ensures { forall i:int.
ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2] }
val self_blit (a: array 'a) (ofs1: int) (ofs2: int) (len: int) : unit
val self_blit (a: array ~'a) (ofs1: int) (ofs2: int) (len: int) : unit
writes {a}
requires { 0 <= ofs1 /\ 0 <= len /\ ofs1 + len <= length a }
requires { 0 <= ofs2 /\ ofs2 + len <= length a }
......
......@@ -10,8 +10,8 @@ theory Map
(** if ['b] is an infinite type, then [map 'a 'b] is infinite *)
meta "material_type_arg" type map, 1
function get (map 'a 'b) 'a : 'b
function set (map 'a 'b) 'a 'b : map 'a 'b
function get (map 'a ~'b) 'a : 'b
function set (map 'a ~'b) 'a 'b : map 'a 'b
(** syntactic sugar *)
function ([]) (a : map 'a 'b) (i : 'a) : 'b = get a i
......@@ -27,7 +27,7 @@ theory Map
forall b : 'b [m[a1 <- b][a2]].
a1 <> a2 -> m[a1 <- b][a2] = m[a2]
function const 'b : map 'a 'b
function const ~'b : map 'a 'b
axiom Const : forall b:'b, a:'a. (const b)[a] = b
......
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