Why3 Standard Library index



Characters and Strings


Characters

module Char

  use import int.Int

  type char model { code : int }

  function uppercase char : char
  function lowercase char : char

  axiom uppercase_alpha:
    forall c:int. 97 <= c <= 122 ->
      uppercase { code = c } = { code = c - 32 }

  axiom uppercase_other:
    forall c:int. 0 <= c < 97 \/ 122 < c <= 127 ->
      uppercase { code = c } = { code = c }

  axiom lowercase_alpha:
    forall c:int. 65 <= c <= 90 ->
      lowercase { code = c } = { code = c + 32 }

  axiom lowercase_other:
    forall c:int. 0 <= c < 65 \/ 90 < c <= 127 ->
      lowercase { code = c } = { code = c }

  val chr (x:int) : char
    requires { 0 <= x <= 255 }
    ensures  { result = { code = x } }

  val code (c:char) : int
    ensures  { result = c.code /\ 0 <= c.code <= 255 }

end

Strings

module String

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

  type string model { length: int; mutable chars: map int char }
    invariant { self.length >= 0 }

  val create (len:int) : string
    requires { len >= 0 } ensures { length result = len }

  function ([]) (s: string) (i :int) : char = M.([]) s.chars i
  function get (s: string) (i :int) : char = M.([]) s.chars i

  val make (len:int) (c:char) : string
    requires { len >= 0 }
    ensures  { length result = len }
    ensures  { forall i:int. 0 <= i < len -> result[i] = c }

  val get (s:string) (i:int) : char
    requires { 0 <= i < length s } ensures { result = s[i] }

  val unsafe_get (s:string) (i:int) : char
    ensures { result = s[i] }

  val set (s:string) (i:int) (v:char) : unit writes {s}
    requires { 0 <= i < length s }
    ensures  { s.chars = (old s.chars)[i <- v] }

  val unsafe_set (s:string) (i:int) (v:char) : unit writes {s}
    ensures { s.chars = (old s.chars)[i <- v] }

  val length (s:string) : int ensures { result = length s }

  val copy (s:string) : string
    ensures { length result = length s }
    ensures { forall i:int. 0 <= i < length result -> result[i] = s[i] }

  val uppercase (s:string) : string
    ensures { length result = length s }
    ensures { forall i:int.
      0 <= i < length result -> result[i] = Char.uppercase s[i] }

  val lowercase (s:string) : string
    ensures { length result = length s }
    ensures { forall i:int.
      0 <= i < length result -> result[i] = Char.lowercase s[i] }

end

Buffers

module Buffer

  use import int.Int
  use import Char
  use import String as S
  use import map.Map as M

  type t model { mutable length: int; mutable contents: map int char }
    invariant { self.length >= 0 }

  val create (size:int) : t
    requires { size >= 0 } ensures { result.length = 0 }

size is only given as a hint for the initial size

  val contents (b:t) : string
    ensures { S.length result = length b }

  val add_char (b:t) (c:char) : unit writes {b}
    ensures { length b = old (length b) + 1 }
    ensures { forall i: int.
      0 <= i < length b -> b.contents[i] = (old b.contents)[i] }
    ensures { b.contents[length b - 1] = c }

  val add_string (b:t) (s:string) : unit writes {b}
    ensures { length b = old (length b) + S.length s }
    ensures { forall i: int.
      0 <= i < old (length b) -> b.contents[i] = (old b.contents)[i] }
    ensures { forall i: int.
      0 <= i < S.length s -> b.contents[old (length b) + i] = S.get s i }

end

Generated by why3doc 0.88.0