examples/ropes.mlw

   1
   2 (*
   3   Ropes
   4
   5     Boehm, Hans-J; Atkinson, Russ; and Plass, Michael (December 1995).
   6     "Ropes: an Alternative to Strings".
   7     Software—Practice & Experience 25 (12):1315–1330.
   8
   9   Authors: Léon Gondelman (Université Paris Sud)
  10            Jean-Christophe Filliâtre (CNRS)
  11 *)
  12
  13 (* Immutable strings
  14
  15    Used both for rope leaves and for specification purposes *)
  16
  17 module String
  18
  19   use int.Int
  20
  21   type char
  22   constant dummy_char: char
  23
  24   type char_string
  25
  26   (* axiomatized function length *)
  27   val function length char_string: int
  28     ensures { 0 <= result }
  29
  30   (* string access routine *)
  31   val function ([]) (s: char_string) (i:int) : char
  32     requires { 0 <= i < s.length }
  33
  34   val constant empty: char_string
  35     ensures { length result = 0 }
  36
  37   (* extensional equality for strings *)
  38   predicate (==) (s1 s2: char_string) =
  39     length s1 = length s2 /\
  40     forall i:int. 0 <= i < length s1 -> s1[i] = s2[i]
  41
  42   axiom extensionality:
  43      forall s1 s2: char_string. s1 == s2 -> s1 = s2
  44
  45   (* axiomatized concatenation *)
  46   function app char_string char_string: char_string
  47
  48   axiom app_def1:
  49     forall s1 s2: char_string. length (app s1 s2) = length s1 + length s2
  50
  51   axiom app_def2:
  52     forall s1 s2: char_string, i: int.
  53     0 <= i < length s1 -> (app s1 s2)[i] = s1[i]
  54
  55   axiom app_def3:
  56     forall s1 s2: char_string, i: int.
  57     length s1 <= i < length s1 + length s2 ->
  58     (app s1 s2)[i] = s2[i - length s1]
  59
  60   lemma app_assoc:
  61     forall s1 s2 s3: char_string. app s1 (app s2 s3) == app (app s1 s2) s3
  62
  63   (* axiomatized substring *)
  64   function sub char_string int int: char_string
  65
  66   axiom sub_def1:
  67     forall s: char_string, ofs len: int.
  68     0 <= len -> 0 <= ofs <= length s -> ofs + len <= length s ->
  69     length (sub s ofs len) = len
  70
  71   axiom sub_def2:
  72     forall s: char_string, ofs len: int.
  73     0 <= len -> 0 <= ofs <= length s -> ofs + len <= length s ->
  74     forall i: int. 0 <= i < len -> (sub s ofs len)[i] = s[ofs + i]
  75
  76   (* substring routine *)
  77   val sub (s: char_string) (ofs len: int) : char_string
  78     requires { 0 <= len /\ 0 <= ofs <= length s /\ ofs + len <= length s }
  79     ensures  { result = sub s ofs len }
  80
  81 end
  82
  83 (* API *)
  84
  85 module Sig
  86
  87   use int.Int
  88   use import String as S
  89
  90   type rope
  91
  92   function string rope: char_string
  93     (** a rope is a string *)
  94
  95   function length rope: int
  96
  97   val constant empty : rope
  98     ensures { length result = 0 /\ string result == S.empty }
  99
 100   val is_empty (r: rope) : bool
 101     ensures  { result <-> string r == S.empty }
 102
 103   val of_string (s: char_string) : rope
 104     requires { 0 <= S.length s }
 105     ensures  { string result == s}
 106
 107   (* access to the i-th character *)
 108   val get (r: rope) (i: int) : char
 109     requires { 0 <= i < length r }
 110     ensures  { result = (string r)[i] }
 111
 112   val concat (r1 r2: rope) : rope
 113     ensures  { string result == S.app (string r1) (string r2) }
 114
 115   (* sub-rope construction *)
 116   val sub (r: rope) (ofs len: int) : rope
 117     requires { 0 <= len /\ 0 <= ofs <= length r /\ ofs + len <= length r }
 118     ensures  { string result == S.sub (string r) ofs len }
 119
 120   val balance (r: rope) : rope
 121     ensures  { string result == string r }
 122
 123 end
 124
 125 (* Implementation *)
 126
 127 module Rope (* : Sig *)
 128
 129   use int.Int
 130   use import String as S
 131
 132   (* ***** Logical description of rope type **** *)
 133   type rope =
 134     | Emp
 135     | Str char_string int  int  (* Str s ofs len is s[ofs..ofs+len[ *)
 136     | App rope   rope int  (* concatenation and total length   *)
 137
 138   let function length (r: rope) : int =
 139     match r with
 140     | Emp         -> 0
 141     | Str _ _ len -> len
 142     | App _ _ len -> len
 143     end
 144
 145   (* invariant predicate for ropes *)
 146   predicate inv (r: rope) = match r with
 147     | Emp ->
 148         true
 149     | Str s ofs len ->
 150         0 < len /\ 0 <= ofs < S.length s /\ ofs + len <= S.length s
 151         (* s[ofs..ofs+len[ is a non-empty substring of s *)
 152     | App l r len ->
 153         0 < length l /\ inv l /\ 0 < length r /\ inv r /\
 154         len = length l + length r
 155         (* l and r are non-empty strings of the size (|l| + |r|) = len *)
 156   end
 157
 158   (* the string model of a rope *)
 159   function string (r: rope) : char_string = match r with
 160     | 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   lemma rope_length_is_string_length:
 167     forall r: rope. inv r -> S.length (string r) = length r
 168
 169   (* NB: Here and below pay attention to the use of '==' predicate in
 170   contracts *)
 171
 172   (* empty rope *)
 173   let constant empty : rope = Emp
 174     ensures { length result = 0 /\ inv result /\ string result == S.empty }
 175
 176   let is_empty (r: rope) : bool
 177     requires { inv r }
 178     ensures  { result <-> string r == S.empty }
 179   = match r with Emp -> true | _ -> false end
 180
 181   (* string conversion into a rope *)
 182   let of_string (s: char_string) : rope
 183     requires { 0 <= S.length s }
 184     ensures  { string result == s}
 185     ensures  { inv result }
 186   = if S.length s = 0 then Emp else Str s 0 (S.length s)
 187
 188   (* access to the character of the given index i *)
 189   let rec get (r: rope) (i: int) : char
 190     requires { inv r }
 191     requires { 0 <= i < length r }
 192     ensures  { result = (string r)[i] }
 193     variant  { r }
 194   = match r with
 195     | Emp ->
 196         absurd
 197     | Str s ofs _ ->
 198        s[ofs + i]
 199     | App left right _   ->
 200         let n = length left in
 201         if i < n then get left i else get right (i - n)
 202     end
 203
 204   (* concatenation of two ropes *)
 205   let concat (r1 r2: rope) : rope
 206     requires { inv r1 /\ inv r2 }
 207     ensures  { inv result }
 208     ensures  { string result == S.app (string r1) (string r2) }
 209   = match r1, r2 with
 210     | Emp, r | r, Emp -> r
 211     | _               -> App r1 r2 (length r1 + length r2)
 212     end
 213
 214   (* sub-rope construction *)
 215   let rec sub (r: rope) (ofs len: int) : rope
 216     requires { inv r}
 217     requires { 0 <= len /\ 0 <= ofs <= length r /\ ofs + len <= length r }
 218     ensures  { inv result }
 219     ensures  { string result == S.sub (string r) ofs len }
 220     variant  { r }
 221   =
 222   match r with
 223     | Emp          -> assert { len = 0 }; Emp
 224     | Str s ofs' _ -> if len = 0 then Emp else Str s (ofs' + ofs) len
 225     | App r1 r2 _  ->
 226         let left  = length r1 - ofs in (* max chars to the left  *)
 227         let right = len - left      in (* max chars to the right *)
 228         if right <= 0 then sub r1 ofs len
 229         else if 0 >= left then sub r2 (- left) len
 230         else concat (sub r1 ofs left) (sub r2 0 right)
 231     end
 232
 233 end
 234
 235 module Balance
 236
 237   use String
 238   use import Rope as R
 239   use int.Int
 240   use int.Fibonacci
 241   use int.MinMax
 242   use array.Array
 243   use ref.Ref
 244
 245   (** we assume that any rope length is smaller than fib (max+1) *)
 246   val constant max : int (* e.g. = 100 *)
 247     ensures { 2 <= result }
 248
 249   function string_of_array (q: array rope) (l u: int) : char_string
 250     (** `q[u-1] + q[u-2] + ... + q[l]` *)
 251
 252   axiom string_of_array_empty:
 253     forall q: array rope, l: int.
 254     0 <= l <= length q -> string_of_array q l l == S.empty
 255
 256   axiom string_of_array_concat_left:
 257     forall q: array rope, l u: int. 0 <= l < u <= Array.length q ->
 258     string_of_array q l u ==
 259       S.app (string_of_array q (l+1) u) (string q[l])
 260
 261
 262   let rec lemma string_of_array_concat
 263     (q: array rope) (l mid u: int) : unit
 264     requires { 0 <= l <= mid <= u <= Array.length q }
 265     ensures  { string_of_array q l u ==
 266       S.app (string_of_array q mid u) (string_of_array q l mid) }
 267     = variant { mid - l } if l < mid then string_of_array_concat q (l+1) mid u
 268
 269   let rec lemma string_of_array_concat_right
 270     (q: array rope) (l u: int)
 271     requires { 0 <= l < u <= Array.length q }
 272     ensures { string_of_array q l u ==
 273                 S.app (string q[u-1]) (string_of_array q l (u-1)) }
 274     = variant { u -l } if l < u-1 then string_of_array_concat_right q (l+1) u
 275
 276   let lemma string_of_array_length
 277     (q: array rope) (l u i: int)
 278     requires { 0 <= l <= i < u <= Array.length q }
 279     requires { forall j: int. l <= j < u -> inv q[j] }
 280     ensures  { S.length (string_of_array q l u) >= S.length (string q[i]) }
 281     = assert { string_of_array q l (i+1) ==
 282                  S.app (string q[i]) (string_of_array q l i) };
 283       assert { string_of_array q l u ==
 284                S.app (string_of_array q (i+1) u) (string_of_array q l (i+1)) }
 285
 286   let rec lemma string_of_array_eq
 287     (q1 q2: array rope) (l u: int)
 288     requires { 0 <= l <= u <= Array.length q1 = Array.length q2 }
 289     requires { forall j: int. l <= j < u -> q1[j] = q2[j] }
 290     ensures  { string_of_array q1 l u == string_of_array q2 l u }
 291     = variant { u - l } if l < u then string_of_array_eq q1 q2 (l+1) u
 292
 293   lemma string_of_array_frame:
 294     forall q: array rope, l u: int. 0 <= l <= u <= Array.length q ->
 295     forall i: int, r: rope. (0 <= i < l \/ u <= i < Array.length q) ->
 296     string_of_array q l u == string_of_array q[i <- r] l u
 297
 298   let rec lemma string_of_array_concat_empty
 299     (q: array rope) (l u: int)
 300     requires { 0 <= l <= u <= Array.length q }
 301     requires { forall j: int. l <= j < u -> q[j] = Emp }
 302     ensures  { string_of_array q l u == S.empty }
 303     = variant { u - l } if l < u then string_of_array_concat_empty q (l+1) u
 304
 305   function string_of_queue (q: array rope) : char_string =
 306     string_of_array q 2 (Array.length q)
 307
 308   let rec insert (q: array rope) (i: int) (r: rope) : unit
 309     requires { 2 <= i < length q = max+1 }
 310     requires { inv r }
 311     requires { forall j: int. 2 <= j <= max -> inv q[j] }
 312     requires { S.length (string_of_array q i (max+1)) + R.length r
 313                < fib (max+1) }
 314     ensures  { forall j: int. 2 <= j <= max -> inv q[j] }
 315     ensures  { forall j: int. 2 <= j < i -> q[j] = (old q)[j] }
 316     ensures  { string_of_array q i (max+1) ==
 317                  S.app (string_of_array (old q) i (max+1)) (string r) }
 318     variant  { max - i }
 319   = let r' = concat q[i] r in
 320     if R.length r' < fib (i+1) then begin
 321       q[i] <- r';
 322       assert {    string_of_array q       (i+1) (max+1)
 323                == string_of_array (old q) (i+1) (max+1) }
 324     end else begin
 325       q[i] <- Emp;
 326       assert {    string_of_array q       i     (max+1)
 327                == string_of_array (old q) (i+1) (max+1) };
 328       assert {   S.app (string_of_array q       i (max+1)) (string r')
 329               == S.app (string_of_array (old q) i (max+1)) (string r) };
 330       insert q (i+1) r';
 331       assert { string_of_array q i (max+1) == string_of_array q (i+1) (max+1) }
 332     end
 333
 334   let rec insert_leaves (q: array rope) (r: rope) : unit
 335     requires { 2 < length q = max+1 }
 336     requires { inv r }
 337     requires { forall j: int. 2 <= j <= max -> inv q[j] }
 338     requires { S.length (string_of_queue q) + R.length r < fib (max+1) }
 339     ensures  { forall j: int. 2 <= j <= max -> inv q[j] }
 340     ensures  { string_of_queue q ==
 341                  S.app (string_of_queue (old q)) (string r) }
 342     variant  { r }
 343   = match r with
 344     | Emp              -> ()
 345     | Str _ _ _        -> insert q 2 r
 346     | App left right _ -> insert_leaves q left; insert_leaves q right
 347   end
 348
 349   let balance (r: rope) : rope
 350     requires { inv r }
 351     requires { R.length r < fib (max+1) }
 352     ensures  { inv result }
 353     ensures  { string result == string r }
 354   = let q = Array.make (max+1) Emp in
 355     assert { string_of_queue q == S.empty };
 356     insert_leaves q r;
 357     assert { string_of_queue q == string r };
 358     let res = ref Emp in
 359     for i = 2 to max do
 360       invariant { inv !res }
 361       invariant { string !res == string_of_array q 2 i }
 362       res := concat q[i] !res
 363     done;
 364     !res
 365
 366 end