[gallery] 'ropes' completed

parent ba4b8d2d
module String
use import int.Int
use HighOrd as HO
type char
constant dummy_char: char
type string = { length: int; chars: HO.func int char }
function ([]) (s: string) (i: int) : char = s.chars i
constant empty : string = { length = 0; chars = \ i: int. dummy_char }
val get (s: string) (i:int) : char
requires { 0 <= i < s.length }
ensures { result = s.chars i }
function app (s1 s2: string) : string =
{ length = s1.length + s2.length;
chars = \ i: int.
if i < s1.length then s1.chars i else s2.chars (i - s1.length) }
function sub (s: string) (ofs: int) (len: int) : string =
{ length = len; chars = \ i: int. s.chars (i - ofs) }
predicate (==) (s1 s2: string) =
s1.length = s2.length /\
forall i:int. 0 <= i < s1.length -> s1.chars i = s2.chars i
end
module String "immutable strings" (*
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 use import int.Int
...@@ -64,36 +79,10 @@ module String "immutable strings" ...@@ -64,36 +79,10 @@ module String "immutable strings"
requires { 0 <= len /\ 0 <= ofs <= length s /\ ofs + len <= length s } requires { 0 <= len /\ 0 <= ofs <= length s /\ ofs + len <= length s }
ensures { result = sub s ofs len } ensures { result = sub s ofs len }
(**
namespace import S
use HighOrd as HO
type char
constant dummy_char: char
type string = { length: int; chars: HO.func int char }
function ([]) (s: string) (i: int) : char = s.chars i
val get (s: string) (i:int) : char
requires { 0 <= i < s.length }
ensures { result = s.chars i }
function app (s1 s2: string) : string =
{ length = s1.length + s2.length;
chars = \ i: int.
if i < s1.length then s1.chars i else s2.chars (i - s1.length) }
function sub (s: string) (ofs: int) (len: int) : string =
{ length = len; chars = \ i: int. s.chars (i - ofs) }
constant empty : string = { length = 0; chars = \ i: int. dummy_char }
predicate (==) (s1 s2: string) =
s1.length = s2.length /\
forall i:int. 0 <= i < s1.length -> s1.chars i = s2.chars i
end
**)
end end
(* API *)
module Sig module Sig
use import int.Int use import int.Int
...@@ -102,6 +91,7 @@ module Sig ...@@ -102,6 +91,7 @@ module Sig
type rope type rope
function string rope: string function string rope: string
(** a rope is a string *)
function length rope: int function length rope: int
...@@ -133,6 +123,8 @@ module Sig ...@@ -133,6 +123,8 @@ module Sig
end end
(* Implementation *)
module Rope (* : Sig *) module Rope (* : Sig *)
use import int.Int use import int.Int
...@@ -251,21 +243,9 @@ module Balance ...@@ -251,21 +243,9 @@ module Balance
use import array.Array use import array.Array
use import ref.Ref use import ref.Ref
function height (r: rope) : int = match r with (** we assume that any rope length is smaller than fib (max+1) *)
| Emp | Str _ _ _ -> 0 constant max : int (* e.g. = 100 *)
| App left right _ -> 1 + max (height left) (height right) axiom max_at_least_2: 2 <= max
end
constant max : int = 44
(**
TODO:
1. code + safety
2. ensures string result == string r
3. ensures inv result
4. file[i] <> Emp -> height(file[i]) <= i -2 /\ length file[i] >= fib i
**)
function string_of_array (q: Array.array rope) (l u: int) : string function string_of_array (q: Array.array rope) (l u: int) : string
(** q[u-1] + q[u-2] + ... + q[l] *) (** q[u-1] + q[u-2] + ... + q[l] *)
...@@ -284,30 +264,43 @@ module Balance ...@@ -284,30 +264,43 @@ module Balance
requires { 0 <= l <= mid <= u <= Array.length q } requires { 0 <= l <= mid <= u <= Array.length q }
ensures { string_of_array q l u == ensures { string_of_array q l u ==
S.app (string_of_array q mid u) (string_of_array q l mid) } S.app (string_of_array q mid u) (string_of_array q l mid) }
variant { mid - l } = variant { mid - l } if l < mid then string_of_array_concat q (l+1) mid u
= 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_concat_right:
forall q: Array.array rope, l u: int. 0 <= l < u <= Array.length q ->
string_of_array q l u ==
S.app (string q[u-1]) (string_of_array q l (u-1))
lemma string_of_array_length:
forall q: Array.array rope, l u i: int. 0 <= l <= i < u <= Array.length q ->
(forall j: int. l <= j < u -> inv q[j]) ->
S.length (string_of_array q l u) >= S.length (string q[i])
lemma string_of_array_eq:
forall q1 q2: Array.array rope, l u: int.
0 <= l <= u <= Array.length q1 = Array.length q2 ->
(forall j: int. l <= j < u -> q1[j] = q2[j]) ->
string_of_array q1 l u == string_of_array q2 l u
lemma string_of_array_frame: lemma string_of_array_frame:
forall q: Array.array rope, l u: int. 0 <= l <= u <= Array.length q -> 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) -> 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 string_of_array q l u == string_of_array q[i <- r] l u
lemma string_of_array_concat_empty:
forall q: Array.array rope, l u: int. 0 <= l <= u <= Array.length q -> let rec lemma string_of_array_concat_empty
(forall j: int. l <= j < u -> q[j] = Emp) -> (q: Array.array rope) (l u: int)
string_of_array q l u == S.empty 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 = function string_of_queue (q: Array.array rope) : string =
string_of_array q 2 (Array.length q) string_of_array q 2 (Array.length q)
......
This source diff could not be displayed because it is too large. You can view the blob instead.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment