stdlib/matrix.mlw

   1 (** {1 Matrices} *)
   2
   3 module Matrix
   4
   5   use int.Int
   6   use map.Map
   7
   8   type matrix 'a = private {
   9     ghost mutable elts: int -> int -> 'a;
  10                   rows: int;
  11                columns: int
  12   } invariant { 0 <= rows /\ 0 <= columns }
  13
  14   predicate valid_index (a: matrix 'a) (r c: int) =
  15     0 <= r < a.rows /\ 0 <= c < a.columns
  16
  17   function get (a: matrix 'a) (r c: int) : 'a =
  18     a.elts r c
  19
  20   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   val ghost function update (a: matrix 'a) (r c: int) (v: 'a) : matrix 'a
  25     ensures  { result.rows = a.rows }
  26     ensures  { result.columns = a.columns }
  27     ensures  { result.elts = a.elts[r <- (a.elts r)[c <- v]] }
  28
  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   exception OutOfBounds
  37
  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     raises  { OutOfBounds -> not (valid_index a r c) }
  42   = if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
  43     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     raises  { OutOfBounds -> not (valid_index a r c) /\ a = old a }
  49   = if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
  50     set a r c v
  51
  52   val make (r c: int) (v: 'a) : matrix 'a
  53     requires { r >= 0 /\ c >= 0 }
  54     ensures  { result.rows = r }
  55     ensures  { result.columns = c }
  56     ensures  {
  57       forall i j. 0 <= i < r /\ 0 <= j < c -> result.elts i j = v }
  58
  59   val copy (a: matrix 'a) : matrix 'a
  60     ensures  { result.rows = a.rows /\ result.columns = a.columns }
  61     ensures  { forall r:int. 0 <= r < result.rows ->
  62                forall c:int. 0 <= c < result.columns ->
  63                result.elts r c = a.elts r c }
  64
  65 end