Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
b6a894c5
Commit
b6a894c5
authored
Jul 15, 2011
by
Jean-Christophe Filliâtre
Browse files
removing old version of edit distance
parent
01374e3e
Changes
2
Hide whitespace changes
Inline
Side-by-side
.gitignore
View file @
b6a894c5
...
...
@@ -160,7 +160,6 @@ why3.conf
/examples/programs/algo65/
/examples/programs/binary_search_c/
/examples/programs/dijkstra/
/examples/programs/distance/
# modules
/modules/string/
...
...
examples/programs/distance.mlw
deleted
100644 → 0
View file @
01374e3e
(* 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 ref.Ref
use import module array.Array
(* Parameters. Input of the program is composed of two arrays
of characters, [w1] of size [n1] and [w2] of size [n2]. *)
function n1 : int
function n2 : int
type a
type word = list a
val w1 : array a
val 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]. *)
val t : array int
val i : ref int
val j : ref int
val 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
predicate min_dist (w1 w2:word) (n:int) =
dist w1 w2 n /\ forall m:int. dist w1 w2 m -> n <= m
function suffix (array a) int : word
axiom suffix_def_1:
forall m: array a. suffix m (length m) = Nil
axiom suffix_def_2:
forall m: array a, i: int.
0 <= i < length m -> suffix m i = Cons m[i] (suffix m (i+1))
predicate min_suffix (w1 w2: array a) (i j n: int) =
min_dist (suffix w1 i) (suffix w2 j) n
function word_of_array (m: array a) : word = suffix m 0
(* The code. *)
let distance () =
{ length w1 = n1 /\ length w2 = n2 /\ length t = n2+1 }
begin
(* initialization of t *)
for i = 0 to n2 do
invariant { length t = n2+1 /\
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
/\ 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
/\ (forall k:int. j < k <= n2 -> min_suffix w1 w2 i k t[k])
/\ (forall k:int. 0 <= k <= j -> min_suffix w1 w2 (i+1) k t[k])
/\ 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:
*)
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment