ropes.mlw 11.1 KB
Newer Older
1

2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
(*
  Ropes

    Boehm, Hans-J; Atkinson, Russ; and Plass, Michael (December 1995).
    "Ropes: an Alternative to Strings".
    Software—Practice & Experience 25 (12):1315–1330.

  Authors: Léon Gondelman (Université Paris Sud)
           Jean-Christophe Filliâtre (CNRS)
*)

(* Immutable strings

   Used both for rope leaves and for specification purposes *)

module String
18

19
  use int.Int
20

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
21 22
  type char
  constant dummy_char: char
23

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
24 25 26
  type string

  (* axiomatized function length *)
27 28
  val function length string: int
    ensures { 0 <= result }
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
29 30

  (* string access routine *)
31
  val function ([]) (s: string) (i:int) : char
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
32 33
    requires { 0 <= i < s.length }

34 35
  val constant empty: string
    ensures { length result = 0 }
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
36 37 38 39 40 41

  (* extensional equality for strings *)
  predicate (==) (s1 s2: string) =
    length s1 = length s2 /\
    forall i:int. 0 <= i < length s1 -> s1[i] = s2[i]

42 43 44
  axiom extensionality:
     forall s1 s2: string. s1 == s2 -> s1 = s2

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
  (* axiomatized concatenation *)
  function app string string: string

  axiom app_def1:
    forall s1 s2: string. length (app s1 s2) = length s1 + length s2

  axiom app_def2:
    forall s1 s2: string, i: int.
    0 <= i < length s1 -> (app s1 s2)[i] = s1[i]

  axiom app_def3:
    forall s1 s2: string, i: int.
    length s1 <= i < length s1 + length s2 ->
    (app s1 s2)[i] = s2[i - length s1]

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
60 61
  lemma app_assoc:
    forall s1 s2 s3: string. app s1 (app s2 s3) == app (app s1 s2) s3
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81

  (* axiomatized substring *)
  function sub string int int: string

  axiom sub_def1:
    forall s: string, ofs len: int.
    0 <= len -> 0 <= ofs <= length s -> ofs + len <= length s ->
    length (sub s ofs len) = len

  axiom sub_def2:
    forall s: string, ofs len: int.
    0 <= len -> 0 <= ofs <= length s -> ofs + len <= length s ->
    forall i: int. 0 <= i < len -> (sub s ofs len)[i] = s[ofs + i]

  (* substring routine *)
  val sub (s: string) (ofs len: int) : string
    requires { 0 <= len /\ 0 <= ofs <= length s /\ ofs + len <= length s }
    ensures  { result = sub s ofs len }

end
82

83 84
(* API *)

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
85
module Sig
86

87
  use int.Int
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
88
  use import String as S
89

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
90
  type rope
91

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
92
  function string rope: string
93
    (** a rope is a string *)
94

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
95
  function length rope: int
96

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
97 98
  val empty () : rope
    ensures { length result = 0 /\ string result == S.empty }
99

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
100 101
  val is_empty (r: rope) : bool
    ensures  { result <-> string r == empty }
102

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
103 104 105
  val of_string (s: string) : rope
    requires { 0 <= S.length s }
    ensures  { string result == s}
106

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
  (* access to the i-th character *)
  val get (r: rope) (i: int) : char
    requires { 0 <= i < length r }
    ensures  { result = (string r)[i] }

  val concat (r1 r2: rope) : rope
    ensures  { string result == S.app (string r1) (string r2) }

  (* sub-rope construction *)
  val sub (r: rope) (ofs len: int) : rope
    requires { 0 <= len /\ 0 <= ofs <= length r /\ ofs + len <= length r }
    ensures  { string result == S.sub (string r) ofs len }

  val balance (r: rope) : rope
    ensures  { string result == string r }

end

125 126
(* Implementation *)

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
127 128
module Rope (* : Sig *)

129
  use int.Int
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
130
  use import String as S
131

132
  (* ***** Logical description of rope type **** *)
133
  type rope =
134 135 136 137
    | Emp
    | Str string int  int  (* Str s ofs len is s[ofs..ofs+len[ *)
    | App rope   rope int  (* concatenation and total length   *)

138 139
  let function length (r: rope) : int =
    match r with
140 141 142
    | Emp         -> 0
    | Str _ _ len -> len
    | App _ _ len -> len
143
    end
144

145
  (* invariant predicate for ropes *)
146
  predicate inv (r: rope) = match r with
147 148
    | Emp ->
        true
149
    | Str s ofs len ->
150
        0 < len /\ 0 <= ofs < S.length s /\ ofs + len <= S.length s
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
151
        (* s[ofs..ofs+len[ is a non-empty substring of s *)
152 153 154
    | App l r len ->
        0 < length l /\ inv l /\ 0 < length r /\ inv r /\
        len = length l + length r
155
        (* l and r are non-empty strings of the size (|l| + |r|) = len *)
156
  end
157

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
158
  (* the string model of a rope *)
159 160
  function string (r: rope) : string = match r with
    | Emp           -> S.empty
161
    | Str s ofs len -> S.sub s ofs len
162
    | App l r _     -> S.app (string l) (string r)
163
  end
164

165
  (* length of stored string is equal to the length of the corresponding rope *)
166 167
  lemma rope_length_is_string_length:
    forall r: rope. inv r -> S.length (string r) = length r
168

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
169 170
  (* NB: Here and below pay attention to the use of '==' predicate in
  contracts *)
171 172

  (* empty rope *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
173
  let empty () : rope
174 175
    ensures { length result = 0 /\ inv result /\ string result == S.empty }
  = Emp
176

177

178 179
  let is_empty (r: rope) : bool
    requires { inv r }
180
    ensures  { result <-> string r == empty }
181
  = match r with Emp -> true | _ -> false end
182

183
  (* string conversion into a rope *)
184 185
  let of_string (s: string) : rope
    requires { 0 <= S.length s }
186
    ensures  { string result == s}
187 188 189
    ensures  { inv result }
  = if S.length s = 0 then Emp else Str s 0 (S.length s)

190
  (* access to the character of the given index i *)
191
  let rec get (r: rope) (i: int) : char
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
192 193
    requires { inv r }
    requires { 0 <= i < length r }
194 195
    ensures  { result = (string r)[i] }
    variant  { r }
196
  = match r with
197 198 199 200 201 202 203
    | Emp ->
        absurd
    | Str s ofs _ ->
       s[ofs + i]
    | App left right _   ->
        let n = length left in
        if i < n then get left i else get right (i - n)
204
    end
205

206
  (* concatenation of two ropes *)
207
  let concat (r1 r2: rope) : rope
208 209
    requires { inv r1 /\ inv r2 }
    ensures  { inv result }
210 211 212 213 214
    ensures  { string result == S.app (string r1) (string r2) }
  = match r1, r2 with
    | Emp, r | r, Emp -> r
    | _               -> App r1 r2 (length r1 + length r2)
    end
215

216
  (* sub-rope construction *)
217
  let rec sub (r: rope) (ofs len: int) : rope
218
    requires { inv r}
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
219
    requires { 0 <= len /\ 0 <= ofs <= length r /\ ofs + len <= length r }
220
    ensures  { inv result }
221
    ensures  { string result == S.sub (string r) ofs len }
222 223 224
    variant  { r }
  =
  match r with
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
225 226
    | Emp          -> assert { len = 0 }; Emp
    | Str s ofs' _ -> if len = 0 then Emp else Str s (ofs' + ofs) len
227
    | App r1 r2 _  ->
228 229 230
        let left  = length r1 - ofs in (* max chars to the left  *)
        let right = len - left      in (* max chars to the right *)
        if right <= 0 then sub r1 ofs len
231
        else if 0 >= left then sub r2 (- left) len
232
        else concat (sub r1 ofs left) (sub r2 0 right)
233
    end
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
234

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
235 236 237
end

module Balance
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
238

239
  use String
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
240
  use import Rope as R
241 242 243 244 245
  use int.Int
  use int.Fibonacci
  use int.MinMax
  use array.Array
  use ref.Ref
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
246

247
  (** we assume that any rope length is smaller than fib (max+1) *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
248 249
  val constant max : int (* e.g. = 100 *)
    ensures { 2 <= result }
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
250

251
  function string_of_array (q: array rope) (l u: int) : string
252
    (** `q[u-1] + q[u-2] + ... + q[l]` *)
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
253 254

  axiom string_of_array_empty:
255
    forall q: array rope, l: int.
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
256
    0 <= l <= length q -> string_of_array q l l == S.empty
257

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
258
  axiom string_of_array_concat_left:
259
    forall q: array rope, l u: int. 0 <= l < u <= Array.length q ->
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
260 261 262
    string_of_array q l u ==
      S.app (string_of_array q (l+1) u) (string q[l])

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
263 264

  let rec lemma string_of_array_concat
265
    (q: array rope) (l mid u: int) : unit
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
266 267 268
    requires { 0 <= l <= mid <= u <= Array.length q }
    ensures  { string_of_array q l u ==
      S.app (string_of_array q mid u) (string_of_array q l mid) }
269 270 271
    = variant { mid - l } if l < mid then string_of_array_concat q (l+1) mid u

  let rec lemma string_of_array_concat_right
272
    (q: array rope) (l u: int)
273 274 275 276 277 278
    requires { 0 <= l < u <= Array.length q }
    ensures { string_of_array q l u ==
                S.app (string q[u-1]) (string_of_array q l (u-1)) }
    = variant { u -l } if l < u-1 then string_of_array_concat_right q (l+1) u

  let lemma string_of_array_length
279
    (q: array rope) (l u i: int)
280 281 282 283 284 285 286 287 288
    requires { 0 <= l <= i < u <= Array.length q }
    requires { forall j: int. l <= j < u -> inv q[j] }
    ensures  { S.length (string_of_array q l u) >= S.length (string q[i]) }
    = assert { string_of_array q l (i+1) ==
                 S.app (string q[i]) (string_of_array q l i) };
      assert { string_of_array q l u ==
               S.app (string_of_array q (i+1) u) (string_of_array q l (i+1)) }

  let rec lemma string_of_array_eq
289
    (q1 q2: array rope) (l u: int)
290 291 292 293
    requires { 0 <= l <= u <= Array.length q1 = Array.length q2 }
    requires { forall j: int. l <= j < u -> q1[j] = q2[j] }
    ensures  { string_of_array q1 l u == string_of_array q2 l u }
    = variant { u - l } if l < u then string_of_array_eq q1 q2 (l+1) u
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
294

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
295
  lemma string_of_array_frame:
296
    forall q: array rope, l u: int. 0 <= l <= u <= Array.length q ->
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
297 298
    forall i: int, r: rope. (0 <= i < l \/ u <= i < Array.length q) ->
    string_of_array q l u == string_of_array q[i <- r] l u
299 300

  let rec lemma string_of_array_concat_empty
301
    (q: array rope) (l u: int)
302 303 304 305
    requires { 0 <= l <= u <= Array.length q }
    requires { forall j: int. l <= j < u -> q[j] = Emp }
    ensures  { string_of_array q l u == S.empty }
    = variant { u - l } if l < u then string_of_array_concat_empty q (l+1) u
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
306

307
  function string_of_queue (q: array rope) : string =
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
308 309
    string_of_array q 2 (Array.length q)

310
  let rec insert (q: array rope) (i: int) (r: rope) : unit
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
311 312 313 314 315 316 317 318 319 320
    requires { 2 <= i < length q = max+1 }
    requires { inv r }
    requires { forall j: int. 2 <= j <= max -> inv q[j] }
    requires { S.length (string_of_array q i (max+1)) + R.length r
               < fib (max+1) }
    ensures  { forall j: int. 2 <= j <= max -> inv q[j] }
    ensures  { forall j: int. 2 <= j < i -> q[j] = (old q)[j] }
    ensures  { string_of_array q i (max+1) ==
                 S.app (string_of_array (old q) i (max+1)) (string r) }
    variant  { max - i }
321
  = let r' = concat q[i] r in
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
322 323
    if R.length r' < fib (i+1) then begin
      q[i] <- r';
324 325
      assert {    string_of_array q       (i+1) (max+1)
               == string_of_array (old q) (i+1) (max+1) }
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
326 327
    end else begin
      q[i] <- Emp;
328 329 330 331
      assert {    string_of_array q       i     (max+1)
               == string_of_array (old q) (i+1) (max+1) };
      assert {   S.app (string_of_array q       i (max+1)) (string r')
              == S.app (string_of_array (old q) i (max+1)) (string r) };
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
      insert q (i+1) r';
      assert { string_of_array q i (max+1) == string_of_array q (i+1) (max+1) }
    end

  let rec insert_leaves (q: array rope) (r: rope) : unit
    requires { 2 < length q = max+1 }
    requires { inv r }
    requires { forall j: int. 2 <= j <= max -> inv q[j] }
    requires { S.length (string_of_queue q) + R.length r < fib (max+1) }
    ensures  { forall j: int. 2 <= j <= max -> inv q[j] }
    ensures  { string_of_queue q ==
                 S.app (string_of_queue (old q)) (string r) }
    variant  { r }
  = match r with
    | Emp              -> ()
    | Str _ _ _        -> insert q 2 r
    | App left right _ -> insert_leaves q left; insert_leaves q right
  end

  let balance (r: rope) : rope
    requires { inv r }
    requires { R.length r < fib (max+1) }
    ensures  { inv result }
    ensures  { string result == string r }
  = let q = Array.make (max+1) Emp in
    assert { string_of_queue q == S.empty };
    insert_leaves q r;
    assert { string_of_queue q == string r };
    let res = ref Emp in
    for i = 2 to max do
      invariant { inv !res }
      invariant { string !res == string_of_array q 2 i }
      res := concat q[i] !res
    done;
    !res

368
end