Commit 91d56a6c authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

modules: use the same specification for array, matrix, and mach/array

parent d514f045
......@@ -13,11 +13,11 @@ module Array
use import map.Map as M
type array 'a = private {
mutable ghost elts : map int 'a;
mutable ghost elts : int -> 'a;
length : int
} invariant { 0 <= length }
function ([]) (a: array 'a) (i: int) : 'a = M.get a.elts i
function ([]) (a: array 'a) (i: int) : 'a = a.elts i
val ([]) (a: array 'a) (i: int) : 'a
requires { "expl:index in array bounds" 0 <= i < length a }
......@@ -275,17 +275,9 @@ module ToList
use import Array
use import list.List
function to_list (a: array 'a) (l u: int) : list 'a
axiom to_list_empty:
forall a: array 'a, l u: int. u <= l ->
to_list a l u = Nil
axiom to_list_cons:
forall a: array 'a, l u: int. l < u ->
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 }
let rec function to_list (a: array 'a) (l u: int) : list 'a
requires { l >= 0 /\ u <= a.length }
variant { u - l }
= if u <= l then Nil else Cons a[l] (to_list a (l+1) u)
end
......@@ -13,18 +13,11 @@ module Array32
use import map.Map as M
type array 'a = private {
mutable ghost elts : map int 'a;
mutable ghost elts : int -> 'a;
length : int32;
} invariant { 0 <= to_int length }
let ghost function get_unsafe (a: array 'a) (i: int) : 'a = a.elts i
val ghost function set_unsafe (a: array 'a) (i: int) (v: 'a) : array 'a
ensures { result.elts = M.set a.elts i v /\ result.length = a.length }
(** syntactic sugar *)
function ([]) (a: array 'a) (i: int) : 'a = get_unsafe a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set_unsafe a i v
function ([]) (a: array 'a) (i: int) : 'a = a.elts i
val ([]) (a: array 'a) (i: int32) : 'a
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
......@@ -32,7 +25,7 @@ module Array32
val ([]<-) (a: array 'a) (i: int32) (v: 'a) : unit writes {a}
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { a.elts = M.set (old a.elts) (to_int i) v }
ensures { a.elts = (old a.elts)[to_int i <- v] }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
......@@ -46,7 +39,7 @@ module Array32
let defensive_set (a: array 'a) (i: int32) (v: 'a)
ensures { 0 <= to_int i < to_int a.length }
ensures { a = (old a)[to_int i <- v] }
ensures { a.elts = (old a.elts)[to_int i <- v] }
raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
......@@ -119,18 +112,11 @@ module Array31
use import map.Map as M
type array 'a = private {
mutable ghost elts : map int 'a;
mutable ghost elts : int -> 'a;
length : int31;
} invariant { 0 <= to_int length }
let ghost function get_unsafe (a: array 'a) (i: int) : 'a = a.elts i
val ghost function set_unsafe (a: array 'a) (i: int) (v: 'a) : array 'a
ensures { result.elts = M.set a.elts i v /\ result.length = a.length }
(** syntactic sugar *)
function ([]) (a: array 'a) (i: int) : 'a = get_unsafe a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set_unsafe a i v
function ([]) (a: array 'a) (i: int) : 'a = a.elts i
val ([]) (a: array 'a) (i: int31) : 'a
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
......@@ -138,7 +124,7 @@ module Array31
val ([]<-) (a: array 'a) (i: int31) (v: 'a) : unit writes {a}
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { a.elts = M.set (old a.elts) (to_int i) v }
ensures { a.elts = (old a.elts)[to_int i <- v] }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
......@@ -152,7 +138,7 @@ module Array31
let defensive_set (a: array 'a) (i: int31) (v: 'a)
ensures { 0 <= to_int i < to_int a.length }
ensures { a = (old a)[to_int i <- v] }
ensures { a.elts = (old a.elts)[to_int i <- v] }
raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
......@@ -225,18 +211,11 @@ module Array63
use import map.Map as M
type array 'a = private {
mutable ghost elts : map int 'a;
mutable ghost elts : int -> 'a;
length : int63;
} invariant { 0 <= to_int length }
let ghost function get_unsafe (a: array 'a) (i: int) : 'a = a.elts i
val ghost function set_unsafe (a: array 'a) (i: int) (v: 'a) : array 'a
ensures { result.elts = M.set a.elts i v /\ result.length = a.length }
(** syntactic sugar *)
function ([]) (a: array 'a) (i: int) : 'a = get_unsafe a i
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set_unsafe a i v
function ([]) (a: array 'a) (i: int) : 'a = a.elts i
val ([]) (a: array 'a) (i: int63) : 'a
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
......@@ -244,7 +223,7 @@ module Array63
val ([]<-) (a: array 'a) (i: int63) (v: 'a) : unit writes {a}
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { a.elts = M.set (old a.elts) (to_int i) v }
ensures { a.elts = (old a.elts)[to_int i <- v] }
(** unsafe get/set operations with no precondition *)
exception OutOfBounds
......@@ -258,7 +237,7 @@ module Array63
let defensive_set (a: array 'a) (i: int63) (v: 'a)
ensures { 0 <= to_int i < to_int a.length }
ensures { a = (old a)[to_int i <- v] }
ensures { a.elts = (old a.elts)[to_int i <- v] }
raises { OutOfBounds -> to_int i < 0 \/ to_int i >= to_int a.length }
= if i < of_int 0 || i >= length a then raise OutOfBounds;
a[i] <- v
......
......@@ -15,11 +15,11 @@ module Matrix
0 <= r < a.rows /\ 0 <= c < a.columns
val get (a: matrix 'a) (r c: int) : 'a
requires { "expl:index in array bounds" valid_index a r c }
requires { "expl:index in matrix bounds" valid_index a r c }
ensures { result = a.elts r c }
val set (a: matrix 'a) (r c: int) (v: 'a) : unit
requires { "expl:index in array bounds" valid_index a r c }
requires { "expl:index in matrix bounds" valid_index a r c }
writes { a }
ensures { a.elts = (old a.elts)[r <- (old a.elts r)[c <- v]] }
......@@ -27,14 +27,14 @@ module Matrix
exception OutOfBounds
let defensive_get (a: matrix 'a) (r c: int) : 'a
ensures { "expl:index in array bounds" valid_index a r c }
ensures { "expl:index in matrix bounds" valid_index a r c }
ensures { result = a.elts r c }
raises { OutOfBounds -> not (valid_index a r c) }
= if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
get a r c
let defensive_set (a: matrix 'a) (r c: int) (v: 'a) : unit
ensures { "expl:index in array bounds" valid_index a r c }
ensures { "expl:index in matrix bounds" valid_index a r c }
ensures { a.elts = (old a.elts)[r <- (old a.elts r)[c <- v]] }
raises { OutOfBounds -> not (valid_index a r c) /\ a = old a }
= if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
......
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