Why3 Standard Library index



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 }

  function get (a: matrix 'a) (r c: int) : 'a =
    M.get (M.get a.elts r) c

  function set (a: matrix 'a) (r c: int) (v: 'a) : matrix 'a =
    { a with elts = M.set a.elts r (M.set (M.get a.elts r) c v) }

  predicate valid_index (a: matrix 'a) (r c: int) =
    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 }
    ensures  { result = get a r c }

  val set (a: matrix 'a) (r c: int) (v: 'a) : unit
    requires { "expl:index in array bounds" valid_index a r c }
    writes   { a }
    ensures  { 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) (r c: int) : 'a
    ensures { "expl:index in array bounds" valid_index a r c }
    ensures { result = get a 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 { a.elts = M.set (old a.elts) r (M.set (M.get (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;
    set a r c v

  val make (r c: int) (v: 'a) : matrix 'a
    requires { r >= 0 /\ c >= 0 }
    ensures  { result.rows = r }
    ensures  { result.columns = c }
    ensures  { forall i j. 0 <= i < r /\ 0 <= j < c -> get result i j = 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

Generated by why3doc 0.87.3