matrix.mlw 2.76 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23
(** {1 Matrices} *)

module Matrix

  use import int.Int
  use import map.Map as M

  type matrix 'a
    model { rows: int; columns: int; mutable elts: map int (map int 'a) }
    invariant { 0 <= self.rows /\ 0 <= self.columns }

  type index = (int, int)

  function get (a: matrix 'a) (i: index) : 'a =
    let r,c = i in M.get (M.get a.elts r) c

  function set (a: matrix 'a) (i: index) (v: 'a) : matrix 'a =
    let r,c = i in
    { a with elts = M.set a.elts r (M.set (M.get a.elts r) c v) }

  predicate valid_index (a: matrix 'a) (i: index) =
    let r,c = i in 0 <= r < a.rows /\ 0 <= c < a.columns

Andrei Paskevich's avatar
Andrei Paskevich committed
24
  val get (a: matrix 'a) (i: index) : 'a
25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
    requires { valid_index a i }
    ensures  { result = get a i }

  val set (a: matrix 'a) (i: index) (v: 'a) : unit writes {a}
    requires { let r,c = i in 0 <= r < a.rows /\ 0 <= c < a.columns }
    ensures  { let r,c = i in
             a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v) }

  val rows    (a: matrix 'a) : int ensures { result = a.rows    }
  val columns (a: matrix 'a) : int ensures { result = a.columns }

  (** unsafe get/set operations with no precondition *)
  exception OutOfBounds

  let defensive_get (a: matrix 'a) (i: index)
    ensures { valid_index a i /\ result = get a i }
    raises  { OutOfBounds -> not (valid_index a i) }
  = let r,c = i in
    if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
    get a i

  let defensive_set (a: matrix 'a) (i: index) (v: 'a)
    ensures { valid_index a i /\ a = set (old a) i v }
48
    raises  { OutOfBounds -> not (valid_index a i) /\ a = old a }
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76
  = let r,c = i in
    if r < 0 || r >= a.rows || c < 0 || c >= a.columns then raise OutOfBounds;
    set a i v

  function make (r c: int) (v: 'a) : matrix 'a =
    { rows = r; columns = c; elts = M.const (M.const v) }

  val make (r c: int) (v: 'a) : matrix 'a
    requires { r >= 0 /\ c >= 0 } ensures { result = make r c v }

  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 ->
                 get result (r,c) = get a (r,c) }

end

(* {2 Square bracket syntax in both logic and programs} *)

module Syntax

  use import int.Int
  use export Matrix

  function ([]) (a: matrix 'a) (i: index) : 'a = get a i
  function ([<-]) (a: matrix 'a) (i: index) (v: 'a) : matrix 'a = set a i v

Andrei Paskevich's avatar
Andrei Paskevich committed
77
  val ([]) (a: matrix 'a) (i: index) : 'a
78 79 80 81 82 83 84 85 86 87
    requires { valid_index a i }
    ensures  { result = get a i }

  val ([]<-) (a: matrix 'a) (i: index) (v: 'a) : unit writes {a}
    requires { let r,c = i in 0 <= r < a.rows /\ 0 <= c < a.columns }
    ensures  { let r,c = i in
             a.elts = M.set (old a.elts) r (M.set (M.get (old a.elts) r) c v) }

end