Why3 Standard Library index



Arrays


Generic Arrays

The length is a non-mutable field, so that we get for free that modification of an array does not modify its length.

module Array

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

  type array 'a model { length : int; mutable elts : map int 'a }
    invariant { 0 <= 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: int) : 'a
    requires { "expl:index in array bounds" 0 <= i < length a }
    ensures  { result = a[i] }

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

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

unsafe get/set operations with no precondition

  exception OutOfBounds

  let defensive_get (a: array 'a) (i: int)
    ensures { 0 <= i < length a /\ result = a[i] }
    raises { OutOfBounds -> i < 0 \/ i >= length a }
  = if i < 0 || i >= length a then raise OutOfBounds;
    a[i]

  let defensive_set (a: array 'a) (i: int) (v: 'a)
    ensures { 0 <= i < length a /\ a = (old a)[i <- v] }
    raises { OutOfBounds -> i < 0 \/ i >= length a /\ a = old a }
  = if i < 0 || i >= length a then raise OutOfBounds;
    a[i] <- v

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

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

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

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

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

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

  let self_blit (a: array ~'a) (ofs1: int) (ofs2: int) (len: int) : unit
    writes {a}
    requires { 0 <= ofs1 /\ 0 <= len /\ ofs1 + len <= length a }
    requires { 0 <= ofs2 /\             ofs2 + len <= length a }
    ensures  { forall i:int.
      (0 <= i < ofs2 \/ ofs2 + len <= i < length a) -> a[i] = (old a)[i] }
    ensures  { forall i:int.
      ofs2 <= i < ofs2 + len -> a[i] = (old a)[ofs1 + i - ofs2] }
  = 'Init:
    if ofs1 <= ofs2 then (* from right to left *)
      for k = len - 1 downto 0 do
        invariant  { forall i:int.
          (0 <= i <= ofs2 + k \/ ofs2 + len <= i < length a) ->
          a[i] = (at a 'Init)[i] }
        invariant  { forall i:int.
          ofs2 + k < i < ofs2 + len -> a[i] = (at a 'Init)[ofs1 + i - ofs2] }
        a[ofs2 + k] <- a[ofs1 + k]
      done
    else (* from left to right *)
      for k = 0 to len - 1 do
        invariant  { forall i:int.
          (0 <= i < ofs2 \/ ofs2 + k <= i < length a) ->
          a[i] = (at a 'Init)[i] }
        invariant  { forall i:int.
          ofs2 <= i < ofs2 + k -> a[i] = (at a 'Init)[ofs1 + i - ofs2] }
        a[ofs2 + k] <- a[ofs1 + k]
      done

end

Sorted Arrays

module IntArraySorted

  use import int.Int
  use import Array
  clone import map.MapSorted as M with type elt = int, predicate le = (<=)

  predicate sorted_sub (a : array int) (l u : int) =
    M.sorted_sub a.elts l u

sorted_sub a l u is true whenever the array segment a(l..u-1) is sorted w.r.t order relation le

  predicate sorted (a : array int) =
    M.sorted_sub a.elts 0 a.length

sorted a is true whenever the array a is sorted w.r.t le

end

module Sorted

  use import int.Int
  use import Array

  type elt

  predicate le elt elt

  predicate sorted_sub (a: array elt) (l u: int) =
    forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2]

sorted_sub a l u is true whenever the array segment a(l..u-1) is sorted w.r.t order relation le

  predicate sorted (a: array elt) =
    forall i1 i2 : int. 0 <= i1 <= i2 < length a -> le a[i1] a[i2]

sorted a is true whenever the array a is sorted w.r.t le

end

Arrays Equality

module ArrayEq

  use import int.Int
  use import Array
  use import map.MapEq

  predicate array_eq_sub (a1 a2: array 'a) (l u: int) =
    a1.length = a2.length /\ 0 <= l <= a1.length /\ 0 <= u <= a1.length /\
    map_eq_sub a1.elts a2.elts l u

  predicate array_eq (a1 a2: array 'a) =
    a1.length = a2.length /\ map_eq_sub a1.elts a2.elts 0 (length a1)

end

module ArrayExchange

  use import int.Int
  use import Array
  use import map.MapExchange as M

  predicate exchange (a1 a2: array 'a) (i j: int) =
    a1.length = a2.length /\
    M.exchange a1.elts a2.elts 0 a1.length i j

exchange a1 a2 i j means that arrays a1 and a2 only differ by the swapping of elements at indices i and j

end

Permutation

module ArrayPermut

  use import int.Int
  use import Array
  use import map.MapPermut as M
  use import map.MapEq
  use import ArrayEq
  use export ArrayExchange

  predicate permut (a1 a2: array 'a) (l u: int) =
    a1.length = a2.length /\ 0 <= l <= a1.length /\ 0 <= u <= a1.length /\
    M.permut a1.elts a2.elts l u

permut a1 a2 l u is true when the segment a1(l..u-1) is a permutation of the segment a2(l..u-1). Values outside of the interval (l..u-1) are ignored.

  predicate permut_sub (a1 a2: array 'a) (l u: int) =
    map_eq_sub a1.elts a2.elts 0 l /\
    permut a1 a2 l u /\
    map_eq_sub a1.elts a2.elts u (length a1)

permut_sub a1 a2 l u is true when the segment a1(l..u-1) is a permutation of the segment a2(l..u-1) and values outside of the interval (l..u-1) are equal.

  predicate permut_all (a1 a2: array 'a) =
    a1.length = a2.length /\ M.permut a1.elts a2.elts 0 a1.length

permut_all a1 a2 l u is true when array a1 is a permutation of array a2.

  lemma exchange_permut_sub:
    forall a1 a2: array 'a, i j l u: int.
    exchange a1 a2 i j -> l <= i < u -> l <= j < u ->
    0 <= l -> u <= length a1 -> permut_sub a1 a2 l u

we can always enlarge the interval

  lemma permut_sub_weakening:
    forall a1 a2: array 'a, l1 u1 l2 u2: int.
    permut_sub a1 a2 l1 u1 -> 0 <= l2 <= l1 -> u1 <= u2 <= length a1 ->
    permut_sub a1 a2 l2 u2

lemmas about permut_all

  lemma exchange_permut_all:
    forall a1 a2: array 'a, i j: int.
    exchange a1 a2 i j -> permut_all a1 a2

end

module ArraySwap

  use import int.Int
  use import Array
  use export ArrayExchange

  let swap (a:array 'a) (i:int) (j:int) : unit
    requires { 0 <= i < length a /\ 0 <= j < length a }
    writes   { a }
    ensures  { exchange (old a) a i j }
  = let v = a[i] in
    a[i] <- a[j];
    a[j] <- v

end

Sum of elements

module ArraySum

  use import Array
  use import map.MapSum as M

sum a l h is the sum of a[i] for l <= i < h

  function sum (a: array int) (l h: int) : int = M.sum a.elts l h

end

Number of array elements satisfying a given predicate

module NumOf
  use import Array
  use HighOrd
  use import Bool
  use int.NumOf as N

the number of ai such that l <= i < u and pr i a[i]

  function numof (pr: int -> 'a -> bool) (a: array 'a) (l u: int) : int =
    N.numof (\ i. pr i a[i]) l u

end

the number of ai such that l <= i < u and a[i] = v

module NumOfEq
  use import Array
  use int.NumOf as N

  function numof (a: array 'a) (v: 'a) (l u: int) : int =
    N.numof (\ i. a[i] = v) l u
end

module ToList
  use import int.Int
  use import Array
  use import list.List

  function to_list (a: array 'a) (l u: int) : list 'a

  axiom to_list_empty:
    forall a: array 'a, l u: int. u <= l ->
    to_list a l u = Nil

  axiom to_list_cons:
    forall a: array 'a, l u: int. l < u ->
    to_list a l u = Cons a[l] (to_list a (l+1) u)

  use import list.Append

  let rec lemma to_list_append (a: array 'a) (l m u: int)
    requires { l <= m <= u }
    variant  { m - l }
    ensures  { to_list a l m ++ to_list a m u = to_list a l u }
  = if l < m then to_list_append a (l+1) m u

  val to_list (a: array 'a) (l u: int) : list 'a
    requires { 0 <= l && u <= length a }
    ensures  { result = to_list a l u }

end

module ToSeq
  use import int.Int
  use import Array
  use seq.Seq as S

  function to_seq (a: array 'a) (l u: int) : S.seq 'a

  axiom to_seq_empty:
    forall a: array 'a, l u: int. u <= l ->
    to_seq a l u = S.empty

  axiom to_seq_cons:
    forall a: array 'a, l u: int. 0 <= l < u <= length a ->
    to_seq a l u = S.cons a[l] (to_seq a (l+1) u)

  let rec lemma to_seq_length
    (a: array 'a) (l u: int)
    requires { 0 <= l <= u <= length a }
    variant  { u - l }
    ensures  { S.length (to_seq a l u) = u - l }
  = if l < u then to_seq_length a (l+1) u

  let rec lemma to_seq_nth
    (a: array 'a) (l i u: int)
    requires { 0 <= l <= i < u <= length a }
    variant  { i - l }
    ensures  { S.get (to_seq a l u) (i - l) = a[i] }
  = if l < i then to_seq_nth a (l+1) i u

  val to_seq (a: array 'a) (l u: int) : S.seq 'a
    requires { 0 <= l && u <= length a }
    ensures  { result = to_seq a l u }

end

Generated by why3doc 0.88.0