matrix.mlw 2.15 KB
Newer Older
1 2 3 4
(** {1 Matrices} *)

module Matrix

5
  use int.Int
6
  use map.Map
7

8
  type matrix 'a = private {
9
    ghost mutable elts: int -> int -> 'a;
10 11 12
                  rows: int;
               columns: int
  } invariant { 0 <= rows /\ 0 <= columns }
13

14 15
  predicate valid_index (a: matrix 'a) (r c: int) =
    0 <= r < a.rows /\ 0 <= c < a.columns
16

17 18 19 20
  function get (a: matrix 'a) (r c: int) : 'a =
    a.elts r c

  val get (a: matrix 'a) (r c: int) : 'a
21
    requires { [@expl:index in matrix bounds] valid_index a r c }
22
    ensures  { result = a.elts r c }
23

24 25 26 27 28
  val ghost function update (a: matrix 'a) (r c: int) (v: 'a) : matrix 'a
    ensures  { result.rows = a.rows }
    ensures  { result.columns = a.columns }
    ensures  { result.elts = a.elts[r <- (a.elts r)[c <- v]] }

29
  val set (a: matrix 'a) (r c: int) (v: 'a) : unit
30
    requires { [@expl:index in matrix bounds] valid_index a r c }
31
    writes   { a }
32
    ensures  { a.elts = (old a.elts)[r <- (old a.elts r)[c <- v]] }
33 34

  (** unsafe get/set operations with no precondition *)
35

36 37
  exception OutOfBounds

38
  let defensive_get (a: matrix 'a) (r c: int) : 'a
39
    ensures { [@expl:index in matrix bounds] valid_index a r c }
40
    ensures { result = a.elts r c }
41 42 43
    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
44

45
  let defensive_set (a: matrix 'a) (r c: int) (v: 'a) : unit
46
    ensures { [@expl:index in matrix bounds] valid_index a r c }
47
    ensures { a.elts = (old a.elts)[r <- (old a.elts r)[c <- v]] }
48 49 50
    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;
    set a r c v
51 52

  val make (r c: int) (v: 'a) : matrix 'a
53
    requires { r >= 0 /\ c >= 0 }
54 55
    ensures  { result.rows = r }
    ensures  { result.columns = c }
56
    ensures  {
57
      forall i j. 0 <= i < r /\ 0 <= j < c -> result.elts i j = v }
58 59 60 61 62

  val copy (a: matrix 'a) : matrix 'a
    ensures  { result.rows = a.rows /\ result.columns = a.columns }
    ensures  { forall r:int. 0 <= r < result.rows ->
               forall c:int. 0 <= c < result.columns ->
63
               result.elts r c = a.elts r c }
64 65

end