## Ropes

From Boehm, Atkinson & Plass's 'Ropes: an Alternative to Strings'

Topics: Data Structures

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

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

use int.Int

type char
constant dummy_char: char

type string

(* axiomatized function length *)
val function length string: int
ensures { 0 <= result }

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

val constant empty: string
ensures { length result = 0 }

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

axiom extensionality:
forall s1 s2: string. s1 == s2 -> s1 = s2

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

lemma app_assoc:
forall s1 s2 s3: string. app s1 (app s2 s3) == app (app s1 s2) s3

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

(* API *)

module Sig

use int.Int
use import String as S

type rope

function string rope: string
```

a rope is a string

```  function length rope: int

val empty () : rope
ensures { length result = 0 /\ string result == S.empty }

val is_empty (r: rope) : bool
ensures  { result <-> string r == empty }

val of_string (s: string) : rope
requires { 0 <= S.length s }
ensures  { string result == s}

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

(* Implementation *)

module Rope (* : Sig *)

use int.Int
use import String as S

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

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

(* invariant predicate for ropes *)
predicate inv (r: rope) = match r with
| Emp ->
true
| Str s ofs len ->
0 < len /\ 0 <= ofs < S.length s /\ ofs + len <= S.length s
(* s[ofs..ofs+len[ is a non-empty substring of s *)
| App l r len ->
0 < length l /\ inv l /\ 0 < length r /\ inv r /\
len = length l + length r
(* l and r are non-empty strings of the size (|l| + |r|) = len *)
end

(* the string model of a rope *)
function string (r: rope) : string = match r with
| Emp           -> S.empty
| Str s ofs len -> S.sub s ofs len
| App l r _     -> S.app (string l) (string r)
end

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

(* NB: Here and below pay attention to the use of '==' predicate in
contracts *)

(* empty rope *)
let empty () : rope
ensures { length result = 0 /\ inv result /\ string result == S.empty }
= Emp

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

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

let rec get (r: rope) (i: int) : char
requires { inv r }
requires { 0 <= i < length r }
ensures  { result = (string r)[i] }
variant  { r }
= match r with
| 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)
end

(* concatenation of two ropes *)
let concat (r1 r2: rope) : rope
requires { inv r1 /\ inv r2 }
ensures  { inv result }
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

(* sub-rope construction *)
let rec sub (r: rope) (ofs len: int) : rope
requires { inv r}
requires { 0 <= len /\ 0 <= ofs <= length r /\ ofs + len <= length r }
ensures  { inv result }
ensures  { string result == S.sub (string r) ofs len }
variant  { r }
=
match r with
| Emp          -> assert { len = 0 }; Emp
| Str s ofs' _ -> if len = 0 then Emp else Str s (ofs' + ofs) len
| App r1 r2 _  ->
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
else if 0 >= left then sub r2 (- left) len
else concat (sub r1 ofs left) (sub r2 0 right)
end

end

module Balance

use String
use import Rope as R
use int.Int
use int.Fibonacci
use int.MinMax
use array.Array
use ref.Ref

val constant max : int (* e.g. = 100 *)
ensures { 2 <= result }
```

we assume that any rope length is smaller than fib (max+1)

```  function string_of_array (q: array rope) (l u: int) : string
```

`q[u-1] + q[u-2] + ... + q[l]`

```  axiom string_of_array_empty:
forall q: 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 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])

let rec lemma string_of_array_concat
(q: 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) }
= 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 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 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 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

lemma string_of_array_frame:
forall q: 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

let rec lemma string_of_array_concat_empty
(q: 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

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

let rec insert (q: 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 }
= 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 (old q) (i+1) (max+1) }
end else begin
q[i] <- Emp;
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) };
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

end
```