(* 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 import int.Int type char constant dummy_char: char 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] 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 import 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} (* 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 (* Implementation *) module Rope (* : Sig *) use import 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 *) 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 } = r = Emp (* 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) (* access to the character of the given index i *) 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 import String use import Rope as R use import int.Int use import int.Fibonacci use import int.MinMax use import array.Array use import ref.Ref (** 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 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]) 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) } = 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 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 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 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) }; 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) }; 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