new program: distance

parent 4969d47d
......@@ -367,11 +367,9 @@ install_local: bin/why3ml
GALLERYPGMS = binary_search bresenham sf same_fringe relabel quicksort \
power mergesort_list mac_carthy isqrt insertion_sort_list flag \
vstte10_aqueue \
vstte10_inverting \
vstte10_max_sum \
vstte10_queens \
vstte10_search_list \
distance \
vstte10_aqueue vstte10_inverting vstte10_max_sum \
vstte10_queens vstte10_search_list \
vacid_0_sparse_array
GALLERYFILES = $(addprefix examples/programs/, $(GALLERYPGMS))
GALLERY = $(addsuffix .gallery, $(GALLERYFILES))
......
(* Correctness of a program computing the minimal distance between
two words (code by Claude Marché).
This program computes a variant of the Levenshtein distance. Given
two strings [w1] and [w2] of respective lengths [n1] and [n2], it
computes the minimal numbers of insertions and deletions to
perform in one of the strings to get the other one. (The
traditional edit distance also includes substitutions.)
The nice point about this code is to work in linear space, in an
array of min(n1,n2) integers. Time complexity is O(n1 * n2), as
usual. *)
module Distance
use import int.Int
use import int.MinMax
use import list.List
use import module stdlib.Ref
use import module stdlib.Array
(* Parameters. Input of the program is composed of two arrays
of characters, [w1] of size [n1] and [w2] of size [n2]. *)
logic n1 : int
logic n2 : int
type a
type word = list a
parameter w1 : array a
parameter w2 : array a
(* Global variables of the program. The program uses an auxiliary
array [t] of integers of size [n2+1] and three auxiliary
integer variables [i], [j] and [old]. *)
parameter t : array int
parameter i : ref int
parameter j : ref int
parameter o : ref int
(* Auxiliary definitions for the program and its specification. *)
inductive dist word word int =
| dist_eps :
dist Nil Nil 0
| dist_add_left :
forall w1 w2: word, n:int.
dist w1 w2 n -> forall a:a. dist (Cons a w1) w2 (n + 1)
| dist_add_right :
forall w1 w2: word, n:int.
dist w1 w2 n -> forall a:a. dist w1 (Cons a w2) (n + 1)
| dist_context :
forall w1 w2: word, n:int.
dist w1 w2 n -> forall a:a. dist (Cons a w1) (Cons a w2) n
logic min_dist (w1 w2:word) (n:int) =
dist w1 w2 n and forall m:int. dist w1 w2 m -> n <= m
logic suffix (map a) int : word
axiom suffix_def_1:
forall m: map a. suffix m (length m) = Nil
axiom suffix_def_2:
forall m: map a, i: int.
0 <= i < length m -> suffix m i = Cons m[i] (suffix m (i+1))
logic min_suffix (w1 w2: map a) (i j n: int) =
min_dist (suffix w1 i) (suffix w2 j) n
logic word_of_array (m: map a) : word = suffix m 0
(* The code. *)
let distance () =
{ length w1 = n1 and length w2 = n2 and length t = n2+1 }
begin
(* initialization of t *)
for i = 0 to n2 do
invariant { length t = n2+1 and
forall j:int. 0 <= j < i -> t[j] = n2-j }
t[i <- n2 - i]
done;
(* loop over w1 *)
for i = n1-1 downto 0 do
invariant { length t = n2+1
and forall j:int. 0 <= j <= n2 -> min_suffix w1 w2 (i+1) j t[j] }
o := t[n2];
t[n2 <- t[n2] + 1];
(* loop over w2 *)
for j = n2-1 downto 0 do
invariant { length t = n2+1
and (forall k:int. j < k <= n2 -> min_suffix w1 w2 i k t[k])
and (forall k:int. 0 <= k <= j -> min_suffix w1 w2 (i+1) k t[k])
and min_suffix w1 w2 (i+1) (j+1) o }
begin
let temp = !o in
o := t[j];
if w1[i] = w2[j] then
t[j <- temp]
else
t[j <- (min t[j] t[j+1]) + 1]
end
done
done;
t[0]
end
{ min_dist (word_of_array w1) (word_of_array w2) result }
end
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. examples/programs/distance.gui"
End:
*)
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