mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
dccef8ab6c
We use now the more idiomatic `let empty = ...` expression. TODO: port `queens_bv` example. After applying this change to the code, I was able to reproduce the proof.
367 lines
11 KiB
Plaintext
367 lines
11 KiB
Plaintext
|
||
(*
|
||
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 char_string
|
||
|
||
(* axiomatized function length *)
|
||
val function length char_string: int
|
||
ensures { 0 <= result }
|
||
|
||
(* string access routine *)
|
||
val function ([]) (s: char_string) (i:int) : char
|
||
requires { 0 <= i < s.length }
|
||
|
||
val constant empty: char_string
|
||
ensures { length result = 0 }
|
||
|
||
(* extensional equality for strings *)
|
||
predicate (==) (s1 s2: char_string) =
|
||
length s1 = length s2 /\
|
||
forall i:int. 0 <= i < length s1 -> s1[i] = s2[i]
|
||
|
||
axiom extensionality:
|
||
forall s1 s2: char_string. s1 == s2 -> s1 = s2
|
||
|
||
(* axiomatized concatenation *)
|
||
function app char_string char_string: char_string
|
||
|
||
axiom app_def1:
|
||
forall s1 s2: char_string. length (app s1 s2) = length s1 + length s2
|
||
|
||
axiom app_def2:
|
||
forall s1 s2: char_string, i: int.
|
||
0 <= i < length s1 -> (app s1 s2)[i] = s1[i]
|
||
|
||
axiom app_def3:
|
||
forall s1 s2: char_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: char_string. app s1 (app s2 s3) == app (app s1 s2) s3
|
||
|
||
(* axiomatized substring *)
|
||
function sub char_string int int: char_string
|
||
|
||
axiom sub_def1:
|
||
forall s: char_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: char_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: char_string) (ofs len: int) : char_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: char_string
|
||
(** a rope is a string *)
|
||
|
||
function length rope: int
|
||
|
||
val constant empty : rope
|
||
ensures { length result = 0 /\ string result == S.empty }
|
||
|
||
val is_empty (r: rope) : bool
|
||
ensures { result <-> string r == S.empty }
|
||
|
||
val of_string (s: char_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 int.Int
|
||
use import String as S
|
||
|
||
(* ***** Logical description of rope type **** *)
|
||
type rope =
|
||
| Emp
|
||
| Str char_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) : char_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 constant empty : rope = Emp
|
||
ensures { length result = 0 /\ inv result /\ string result == S.empty }
|
||
|
||
let is_empty (r: rope) : bool
|
||
requires { inv r }
|
||
ensures { result <-> string r == S.empty }
|
||
= match r with Emp -> true | _ -> false end
|
||
|
||
(* string conversion into a rope *)
|
||
let of_string (s: char_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 String
|
||
use import Rope as R
|
||
use int.Int
|
||
use int.Fibonacci
|
||
use int.MinMax
|
||
use array.Array
|
||
use ref.Ref
|
||
|
||
(** we assume that any rope length is smaller than fib (max+1) *)
|
||
val constant max : int (* e.g. = 100 *)
|
||
ensures { 2 <= result }
|
||
|
||
function string_of_array (q: array rope) (l u: int) : char_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) : char_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
|