diff --git a/.gitignore b/.gitignore index eb8aa92613631c565ac064940c99b78705bba151..7d3c85fad017ca9a2eec5a792c61a10c548234b9 100644 --- a/.gitignore +++ b/.gitignore @@ -160,7 +160,6 @@ why3.conf /examples/programs/algo65/ /examples/programs/binary_search_c/ /examples/programs/dijkstra/ -/examples/programs/distance/ # modules /modules/string/ diff --git a/examples/programs/distance.mlw b/examples/programs/distance.mlw deleted file mode 100644 index f2d97be2aecbd5aff122e1099fb6315c0762560d..0000000000000000000000000000000000000000 --- a/examples/programs/distance.mlw +++ /dev/null @@ -1,120 +0,0 @@ - -(* 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: -*)