Why3 Standard Library index



Arrays with bounded-size integers

Note: We currently duplicate code to get the various modules below but we should eventually be able to implement a single module and then to clone it.


Arrays with 32-bit indices

module Array32

  use import mach.int.Int32
  use import map.Map as M

  type array 'a model { length: int32; mutable elts: map int 'a }
    invariant { 0 <= to_int self.length }

  function get (a: array ~'a) (i: int) : 'a = M.get a.elts i

  function set (a: array ~'a) (i: int) (v: 'a) : array 'a =
    { a with elts = M.set a.elts i v }

syntactic sugar

  function ([]) (a: array 'a) (i: int) : 'a = get a i
  function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v

  val ([]) (a: array ~'a) (i: int32) : 'a
    requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
    ensures  { result = a[to_int i] }

  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 }

  val length (a: array ~'a) : int32 ensures { result = a.length }

unsafe get/set operations with no precondition

  exception OutOfBounds

  let defensive_get (a: array 'a) (i: int32)
    ensures { 0 <= to_int i < to_int a.length }
    ensures { result = a[to_int i] }
    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]

  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] }
    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

  val make (n: int32) (v: ~'a) : array 'a
    requires { "expl:array creation size" to_int n >= 0 }
    ensures  { length result = n }
    ensures  { forall i:int. 0 <= i < to_int n -> get result i = v }

  val append (a1: array ~'a) (a2: array 'a) : array 'a
    ensures { to_int result.length = to_int a1.length + to_int a2.length }
    ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] }
    ensures { forall i:int. 0 <= i < to_int a2.length ->
              result[to_int a1.length + i] = a2[i] }

  val sub (a: array ~'a) (ofs: int32) (len: int32) : array 'a
    requires { 0 <= to_int ofs /\ 0 <= to_int len }
    requires { to_int ofs + to_int len <= to_int a.length }
    ensures  { result.length = len }
    ensures  { forall i:int. 0 <= i < to_int len ->
               result[i] = a[to_int ofs + i] }

  val copy (a: array ~'a) : array 'a
    ensures  { result.length = a.length }
    ensures  { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }

  let fill (a: array ~'a) (ofs: int32) (len: int32) (v: 'a)
    requires { 0 <= to_int ofs /\ 0 <= to_int len }
    requires { to_int ofs + to_int len <= to_int a.length }
    ensures  { forall i:int.
      (0 <= i < to_int ofs \/
        to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
    ensures  { forall i:int. to_int ofs <= i < to_int ofs + to_int len ->
               a[i] = v }
  = 'Init:
    for k = 0 to Int.(-) (to_int len) 1 do (* FIXME: for loop on int32 *)
      invariant { forall i:int.
        (0 <= i < to_int ofs \/
          to_int ofs + to_int len <= i < to_int a.length) ->
        a[i] = (at a 'Init)[i] }
      invariant { forall i:int. to_int ofs <= i < to_int ofs + k -> a[i] = v }
      let k = of_int k in
      a[ofs + k] <- v
    done

  val blit (a1: array ~'a) (ofs1: int32)
                 (a2: array 'a) (ofs2: int32) (len: int32) : unit writes {a2}
    requires { 0 <= to_int ofs1 /\ 0 <= to_int len }
    requires { to_int ofs1 + to_int len <= to_int a1.length }
    requires { 0 <= to_int ofs2 /\
               to_int ofs2 + to_int len <= to_int a2.length }
    ensures  { forall i:int.
      (0 <= i < to_int ofs2 \/
       to_int ofs2 + to_int len <= i < to_int a2.length) ->
       a2[i] = (old a2)[i] }
    ensures  { forall i:int.
      to_int ofs2 <= i < to_int ofs2 + to_int len ->
      a2[i] = a1[to_int ofs1 + i - to_int ofs2] }

  val self_blit (a: array ~'a) (ofs1: int32) (ofs2: int32) (len: int32) : unit
    writes {a}
    requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\
               to_int ofs1 + to_int len <= to_int a.length }
    requires { 0 <= to_int ofs2 /\ to_int ofs2 + to_int len <= to_int a.length }
    ensures  { forall i:int.
      (0 <= i < to_int ofs2 \/
       to_int ofs2 + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
    ensures  { forall i:int.
      to_int ofs2 <= i < to_int ofs2 + to_int len ->
      a[i] = (old a)[to_int ofs1 + i - to_int ofs2] }

end

Arrays with 31-bit indices

module Array31

  use import mach.int.Int31
  use import map.Map as M

  type array 'a model { length: int31; mutable elts: map int 'a }
    invariant { 0 <= to_int self.length }

  function get (a: array ~'a) (i: int) : 'a = M.get a.elts i

  function set (a: array ~'a) (i: int) (v: 'a) : array 'a =
    { a with elts = M.set a.elts i v }

syntactic sugar

  function ([]) (a: array 'a) (i: int) : 'a = get a i
  function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v

  val ([]) (a: array ~'a) (i: int31) : 'a
    requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
    ensures  { result = a[to_int i] }

  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 }

  val length (a: array ~'a) : int31 ensures { result = a.length }

unsafe get/set operations with no precondition

  exception OutOfBounds

  let defensive_get (a: array 'a) (i: int31)
    ensures { 0 <= to_int i < to_int a.length }
    ensures { result = a[to_int i] }
    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]

  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] }
    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

  val make (n: int31) (v: ~'a) : array 'a
    requires { "expl:array creation size" to_int n >= 0 }
    ensures  { length result = n }
    ensures  { forall i:int. 0 <= i < to_int n -> get result i = v }

  val append (a1: array ~'a) (a2: array 'a) : array 'a
    ensures { to_int result.length = to_int a1.length + to_int a2.length }
    ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] }
    ensures { forall i:int. 0 <= i < to_int a2.length ->
              result[to_int a1.length + i] = a2[i] }

  val sub (a: array ~'a) (ofs: int31) (len: int31) : array 'a
    requires { 0 <= to_int ofs /\ 0 <= to_int len }
    requires { to_int ofs + to_int len <= to_int a.length }
    ensures  { result.length = len }
    ensures  { forall i:int. 0 <= i < to_int len ->
               result[i] = a[to_int ofs + i] }

  val copy (a: array ~'a) : array 'a
    ensures  { result.length = a.length }
    ensures  { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }

  let fill (a: array ~'a) (ofs: int31) (len: int31) (v: 'a)
    requires { 0 <= to_int ofs /\ 0 <= to_int len }
    requires { to_int ofs + to_int len <= to_int a.length }
    ensures  { forall i:int.
      (0 <= i < to_int ofs \/
        to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
    ensures  { forall i:int. to_int ofs <= i < to_int ofs + to_int len ->
               a[i] = v }
  = 'Init:
    for k = 0 to Int.(-) (to_int len) 1 do (* FIXME: for loop on int31 *)
      invariant { forall i:int.
        (0 <= i < to_int ofs \/
          to_int ofs + to_int len <= i < to_int a.length) ->
        a[i] = (at a 'Init)[i] }
      invariant { forall i:int. to_int ofs <= i < to_int ofs + k -> a[i] = v }
      let k = of_int k in
      a[ofs + k] <- v
    done

  val blit (a1: array ~'a) (ofs1: int31)
                 (a2: array 'a) (ofs2: int31) (len: int31) : unit writes {a2}
    requires { 0 <= to_int ofs1 /\ 0 <= to_int len }
    requires { to_int ofs1 + to_int len <= to_int a1.length }
    requires { 0 <= to_int ofs2 /\
               to_int ofs2 + to_int len <= to_int a2.length }
    ensures  { forall i:int.
      (0 <= i < to_int ofs2 \/
       to_int ofs2 + to_int len <= i < to_int a2.length) ->
       a2[i] = (old a2)[i] }
    ensures  { forall i:int.
      to_int ofs2 <= i < to_int ofs2 + to_int len ->
      a2[i] = a1[to_int ofs1 + i - to_int ofs2] }

  val self_blit (a: array ~'a) (ofs1: int31) (ofs2: int31) (len: int31) : unit
    writes {a}
    requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\
               to_int ofs1 + to_int len <= to_int a.length }
    requires { 0 <= to_int ofs2 /\ to_int ofs2 + to_int len <= to_int a.length }
    ensures  { forall i:int.
      (0 <= i < to_int ofs2 \/
       to_int ofs2 + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
    ensures  { forall i:int.
      to_int ofs2 <= i < to_int ofs2 + to_int len ->
      a[i] = (old a)[to_int ofs1 + i - to_int ofs2] }

end

Arrays with 63-bit indices

module Array63

  use import mach.int.Int63
  use import map.Map as M

  type array63 'a model { length: int63; mutable elts: map int 'a }
    invariant { 0 <= to_int self.length }

  function get (a: array63 ~'a) (i: int) : 'a = M.get a.elts i

  function set (a: array63 ~'a) (i: int) (v: 'a) : array63 'a =
    { a with elts = M.set a.elts i v }

syntactic sugar

  function ([]) (a: array63 'a) (i: int) : 'a = get a i
  function ([<-]) (a: array63 'a) (i: int) (v: 'a) : array63 'a = set a i v

  val ([]) (a: array63 ~'a) (i: int63) : 'a
    requires { "expl:index in array63 bounds" 0 <= to_int i < to_int a.length }
    ensures  { result = a[to_int i] }

  val ([]<-) (a: array63 ~'a) (i: int63) (v: 'a) : unit writes {a}
    requires { "expl:index in array63 bounds" 0 <= to_int i < to_int a.length }
    ensures  { a.elts = M.set (old a.elts) (to_int i) v }

  val length (a: array63 ~'a) : int63 ensures { result = a.length }

unsafe get/set operations with no precondition

  exception OutOfBounds

  let defensive_get (a: array63 'a) (i: int63)
    ensures { 0 <= to_int i < to_int a.length }
    ensures { result = a[to_int i] }
    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]

  let defensive_set (a: array63 'a) (i: int63) (v: 'a)
    ensures { 0 <= to_int i < to_int a.length }
    ensures { a = (old a)[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

  val make (n: int63) (v: ~'a) : array63 'a
    requires { "expl:array63 creation size" to_int n >= 0 }
    ensures  { length result = n }
    ensures  { forall i:int. 0 <= i < to_int n -> get result i = v }

  val append (a1: array63 ~'a) (a2: array63 'a) : array63 'a
    ensures { to_int result.length = to_int a1.length + to_int a2.length }
    ensures { forall i:int. 0 <= i < to_int a1.length -> result[i] = a1[i] }
    ensures { forall i:int. 0 <= i < to_int a2.length ->
              result[to_int a1.length + i] = a2[i] }

  val sub (a: array63 ~'a) (ofs: int63) (len: int63) : array63 'a
    requires { 0 <= to_int ofs /\ 0 <= to_int len }
    requires { to_int ofs + to_int len <= to_int a.length }
    ensures  { result.length = len }
    ensures  { forall i:int. 0 <= i < to_int len ->
               result[i] = a[to_int ofs + i] }

  val copy (a: array63 ~'a) : array63 'a
    ensures  { result.length = a.length }
    ensures  { forall i:int. 0 <= i < to_int result.length -> result[i] = a[i] }

  let fill (a: array63 ~'a) (ofs: int63) (len: int63) (v: 'a)
    requires { 0 <= to_int ofs /\ 0 <= to_int len }
    requires { to_int ofs + to_int len <= to_int a.length }
    ensures  { forall i:int.
      (0 <= i < to_int ofs \/
        to_int ofs + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
    ensures  { forall i:int. to_int ofs <= i < to_int ofs + to_int len ->
               a[i] = v }
  = 'Init:
    for k = 0 to Int.(-) (to_int len) 1 do (* FIXME: for loop on int63 *)
      invariant { forall i:int.
        (0 <= i < to_int ofs \/
          to_int ofs + to_int len <= i < to_int a.length) ->
        a[i] = (at a 'Init)[i] }
      invariant { forall i:int. to_int ofs <= i < to_int ofs + k -> a[i] = v }
      let k = of_int k in
      a[ofs + k] <- v
    done

  val blit (a1: array63 ~'a) (ofs1: int63)
                 (a2: array63 'a) (ofs2: int63) (len: int63) : unit writes {a2}
    requires { 0 <= to_int ofs1 /\ 0 <= to_int len }
    requires { to_int ofs1 + to_int len <= to_int a1.length }
    requires { 0 <= to_int ofs2 /\
               to_int ofs2 + to_int len <= to_int a2.length }
    ensures  { forall i:int.
      (0 <= i < to_int ofs2 \/
       to_int ofs2 + to_int len <= i < to_int a2.length) ->
       a2[i] = (old a2)[i] }
    ensures  { forall i:int.
      to_int ofs2 <= i < to_int ofs2 + to_int len ->
      a2[i] = a1[to_int ofs1 + i - to_int ofs2] }

  val self_blit (a: array63 ~'a) (ofs1: int63) (ofs2: int63) (len: int63) : unit
    writes {a}
    requires { 0 <= to_int ofs1 /\ 0 <= to_int len /\
               to_int ofs1 + to_int len <= to_int a.length }
    requires { 0 <= to_int ofs2 /\ to_int ofs2 + to_int len <= to_int a.length }
    ensures  { forall i:int.
      (0 <= i < to_int ofs2 \/
       to_int ofs2 + to_int len <= i < to_int a.length) -> a[i] = (old a)[i] }
    ensures  { forall i:int.
      to_int ofs2 <= i < to_int ofs2 + to_int len ->
      a[i] = (old a)[to_int ofs1 + i - to_int ofs2] }

end

(* TODO
   - Array64 ?
*)

Generated by why3doc 0.87.3