string.mlw 3.5 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4
(** {1 Characters and Strings} *)

(** {2 Characters} *)

5 6
module Char

7
  use int.Int
8

9 10
  type char = private { code : int }
    invariant { 0 <= code <= 255 }
11

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

  axiom uppercase_alpha:
16 17
    forall c:char. 97 <= c.code <= 122 ->
      (uppercase c).code = c.code - 32
18

19
  axiom uppercase_other:
20 21
    forall c:char. 0 <= c.code < 97 \/ 122 < c.code <= 127 ->
      (uppercase c).code = c.code
22 23

  axiom lowercase_alpha:
24 25
    forall c:char. 65 <= c.code <= 90 ->
      (lowercase c).code = c.code + 32
26

27
  axiom lowercase_other:
28 29
    forall c:char. 0 <= c.code < 65 \/ 90 < c.code <= 127 ->
      (lowercase c).code = c.code
30

31 32
  val chr (x:int) : char
    requires { 0 <= x <= 255 }
33
    ensures  { result.code = x }
34

MARCHE Claude's avatar
MARCHE Claude committed
35
  (*** TODO
36 37 38
     - compare ?
   *)

39 40
end

MARCHE Claude's avatar
MARCHE Claude committed
41 42
(** {2 Strings} *)

43 44
module String

45 46 47
  use int.Int
  use Char
  use map.Map as M
48

49
  type string = private {
50
    mutable ghost chars: M.map int char;
51 52
                 length: int
  } invariant { length >= 0 }
53

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

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

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

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

68
  val unsafe_get (s:string) (i:int) : char
69 70 71 72
    ensures { result = s[i] }

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

  val unsafe_set (s:string) (i:int) (v:char) : unit writes {s}
76
    ensures { s.chars = old M.(s.chars[i <- v]) }
77 78 79 80 81 82 83 84 85 86 87 88 89 90

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

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

103
end
104

MARCHE Claude's avatar
MARCHE Claude committed
105 106
(** {2 Buffers} *)

107 108
module Buffer

109 110
  use int.Int
  use Char
111
  use import String as S
112
  use import map.Map as M
113

114 115 116 117
  type t = private {
    ghost mutable  chars: map int char;
          mutable length: int
  } invariant { length >= 0 }
118

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

123
  val contents (b:t) : string
124 125 126 127 128
    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.
129 130
      0 <= i < length b -> b.chars[i] = old b.chars[i] }
    ensures { b.chars[length b - 1] = c }
131

132
  val add_string (b:t) (s:string) : unit writes {b}
133 134
    ensures { length b = old (length b) + S.length s }
    ensures { forall i: int.
135
      0 <= i < old (length b) -> b.chars[i] = old b.chars[i] }
136
    ensures { forall i: int.
137
      0 <= i < S.length s -> b.chars[old (length b) + i] = S.get s i }
138

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

144
end