string.mlw 3.63 KB
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2 3 4 5
(** {1 Characters and Strings} *)

(** {2 Characters} *)

6 7
module Char

8 9
  use import int.Int

10
  type char model { code : int }
11

12 13
  function uppercase char : char
  function lowercase char : char
14 15

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

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

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

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

31 32 33 34 35 36
  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 }
37

MARCHE Claude's avatar
MARCHE Claude committed
38
  (*** TODO
39 40 41
     - compare ?
   *)

42 43
end

MARCHE Claude's avatar
MARCHE Claude committed
44 45
(** {2 Strings} *)

46 47 48
module String

  use import int.Int
49
  use import Char
50
  use import map.Map as M
51

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
58 59
  function ([]) (s: string) (i :int) : char = M.([]) s.chars i
  function get (s: string) (i :int) : char = M.([]) s.chars i
60

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

Andrei Paskevich's avatar
Andrei Paskevich committed
66
  val get (s:string) (i:int) : char
67 68
    requires { 0 <= i < length s } ensures { result = s[i] }

Andrei Paskevich's avatar
Andrei Paskevich committed
69
  val unsafe_get (s:string) (i:int) : char
70 71 72 73 74 75 76 77 78
    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] }

Andrei Paskevich's avatar
Andrei Paskevich committed
79
  val length (s:string) : int ensures { result = length s }
80 81 82 83 84 85 86 87 88 89 90 91 92 93

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

MARCHE Claude's avatar
MARCHE Claude committed
95
  (*** TODO
96 97 98 99 100 101 102 103 104 105
     - copy
     - sub
     - fill
     - blit
     - concat
     - index / rindex / index_from / rindex_from
     - contains / contains_from / rcontains_from
     - capitalize / uncapitalize
  *)

106
end
107

MARCHE Claude's avatar
MARCHE Claude committed
108 109
(** {2 Buffers} *)

110 111 112
module Buffer

  use import int.Int
113 114
  use import Char
  use import String as S
115
  use import map.Map as M
116

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

120 121
  val create (size:int) : t
    requires { size >= 0 } ensures { result.length = 0 }
122 123
    (** [size] is only given as a hint for the initial size *)

Andrei Paskevich's avatar
Andrei Paskevich committed
124
  val contents (b:t) : string
125 126 127 128 129 130 131 132
    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 }

Andrei Paskevich's avatar
Andrei Paskevich committed
133
  val add_string (b:t) (s:string) : unit writes {b}
134 135 136 137 138
    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 }
139

MARCHE Claude's avatar
MARCHE Claude committed
140
  (*** TODO
141 142 143 144
     - add_substring
     - add_buffer
  *)

145
end