ropes.mlw 11.3 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 import 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 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
  type string

  (* axiomatized function length *)
  function length string: int
  axiom length_nonnegative: forall s: string. length s >= 0

  function ([]) string int: char (* access to i-th char *)

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

  constant empty: string
  axiom empty_def: length empty = 0


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

46 47 48
  axiom extensionality:
     forall s1 s2: string. s1 == s2 -> s1 = s2

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63
  (* 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
64 65
  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
66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85

  (* 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
86

87 88
(* API *)

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
89
module Sig
90

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
91 92
  use import int.Int
  use import String as S
93

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
94
  type rope
95

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
96
  function string rope: string
97
    (** a rope is a string *)
98

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
99
  function length rope: int
100

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

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

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
107 108 109
  val of_string (s: string) : rope
    requires { 0 <= S.length s }
    ensures  { string result == s}
110

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128
  (* 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

129 130
(* Implementation *)

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
131 132 133 134
module Rope (* : Sig *)

  use import int.Int
  use import String as S
135

136
  (* ***** Logical description of rope type **** *)
137
  type rope =
138 139 140 141 142 143 144 145 146
    | Emp
    | Str string int  int  (* Str s ofs len is s[ofs..ofs+len[ *)
    | App rope   rope int  (* concatenation and total length   *)

  function length (r: rope) : int = match r with
    | Emp         -> 0
    | Str _ _ len -> len
    | App _ _ len -> len
  end
147

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

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

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

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

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

180

181 182
  let is_empty (r: rope) : bool
    requires { inv r }
183
    ensures  { result <-> string r == empty }
184
  = r = Emp
185

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

193
  (* access to the character of the given index i *)
194
  let rec get (r: rope) (i: int) : char
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
195 196
    requires { inv r }
    requires { 0 <= i < length r }
197 198
    ensures  { result = (string r)[i] }
    variant  { r }
199
  = match r with
200 201 202 203 204 205 206
    | 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)
207
    end
208

209
  (* concatenation of two ropes *)
210
  let concat (r1 r2: rope) : rope
211 212
    requires { inv r1 /\ inv r2 }
    ensures  { inv result }
213 214 215 216 217
    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
218

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

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
238 239 240
end

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

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

250 251 252
  (** we assume that any rope length is smaller than fib (max+1) *)
  constant max : int (* e.g. = 100 *)
  axiom max_at_least_2: 2 <= max
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
253

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
254 255 256 257 258 259 260 261 262 263 264
  function string_of_array (q: Array.array rope) (l u: int) : string
    (** q[u-1] + q[u-2] + ... + q[l] *)

  axiom string_of_array_empty:
    forall q: Array.array rope, l: int.
    0 <= l <= length q -> string_of_array q l l == S.empty
  axiom string_of_array_concat_left:
    forall q: Array.array rope, l u: int. 0 <= l < u <= Array.length q ->
    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
265 266 267 268 269 270

  let rec lemma string_of_array_concat
    (q: Array.array rope) (l mid u: int) : unit
    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) }
271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295
    = variant { mid - l } if l < mid then string_of_array_concat q (l+1) mid u

  let rec lemma string_of_array_concat_right
    (q: Array.array rope) (l u: int)
    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
    (q: Array.array rope) (l u i: int)
    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
    (q1 q2: Array.array rope) (l u: int)
    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
296

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
297 298 299 300
  lemma string_of_array_frame:
    forall q: Array.array rope, l u: int. 0 <= l <= u <= Array.length q ->
    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
301 302 303 304 305 306 307

  let rec lemma string_of_array_concat_empty
    (q: Array.array rope) (l u: int)
    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
308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332

  function string_of_queue (q: Array.array rope) : string =
    string_of_array q 2 (Array.length q)

  let rec insert (q: Array.array rope) (i: int) (r: rope) : unit
    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 }
  = 'L:
    let r' = concat q[i] r in
    if R.length r' < fib (i+1) then begin
      q[i] <- r';
      assert {    string_of_array q         (i+1) (max+1)
               == string_of_array (at q 'L) (i+1) (max+1) }
    end else begin
      q[i] <- Emp;
      assert {    string_of_array q         i     (max+1)
               == string_of_array (at q 'L) (i+1) (max+1) };
333 334
      assert {   S.app (string_of_array q         i (max+1)) (string r')
              == S.app (string_of_array (at q 'L) i (max+1)) (string r) };
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
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 368 369 370
      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

371
end