Commit e747314a authored by MARCHE Claude's avatar MARCHE Claude
Browse files

LCP: improved doc + separate module for test harness

parent 7cb45e8d
(** (**
{h <code>} {1 VerifyThis@fm2012 competition, Challenge 1: Longest Repeated Substring}
{h
The following is the original description of the verification task,
reproduced verbatim. A <a
href="http://fm2012.verifythis.org/challenges">reference
implementation in Java</a> (based on code by Robert Sedgewick and
Kevin Wayne) was also given. The Why3 implementation below follows the
Java implementation as faithfully as possible.
<pre>
Longest Common Prefix (LCP) - 45 minutes Longest Common Prefix (LCP) - 45 minutes
VERIFICATION TASK VERIFICATION TASK
...@@ -21,22 +31,16 @@ Pseudocode: ...@@ -21,22 +31,16 @@ Pseudocode:
int lcp(int[] a, int x, int y) { int lcp(int[] a, int x, int y) {
int l = 0; int l = 0;
while (x+l<a.length && y+l<a.length && a[x+l]==a[y+l]) { while (x+l&lt;a.length && y+l&lt;a.length && a[x+l]==a[y+l]) {
l++; l++;
} }
return l; return l;
} }
ADVANCED ADVANCED
======== ========
BACKGROUND BACKGROUND
---------- ----------
...@@ -61,7 +65,6 @@ sorted suffix array is: ...@@ -61,7 +65,6 @@ sorted suffix array is:
[3,0,2,1] [3,0,2,1]
VERIFICATION TASK VERIFICATION TASK
----------------- -----------------
...@@ -71,10 +74,7 @@ comparison on arrays, a sorting routine, and LCP. ...@@ -71,10 +74,7 @@ comparison on arrays, a sorting routine, and LCP.
The client code (LRS.java) uses these to solve the LRS problem. Verify The client code (LRS.java) uses these to solve the LRS problem. Verify
that it does so correctly. that it does so correctly.
</pre>}
(Based on code by Robert Sedgewick and Kevin Wayne.)
{h </code>}
*) *)
...@@ -95,12 +95,13 @@ use import array.Array ...@@ -95,12 +95,13 @@ use import array.Array
at respective positions [x] and [y] in array [a] are identical. In at respective positions [x] and [y] in array [a] are identical. In
other words, the array parts a[x..x+l-1] and a[y..y+l-1] are equal other words, the array parts a[x..x+l-1] and a[y..y+l-1] are equal
*) *)
predicate is_common_prefix (a:array int) (x y:int) (l:int) = predicate is_common_prefix (a:array int) (x y l:int) =
0 <= l /\ x+l <= a.length /\ y+l <= a.length /\ 0 <= l /\ x+l <= a.length /\ y+l <= a.length /\
(forall i:int. 0 <= i < l -> a[x+i] = a[y+i]) (forall i:int. 0 <= i < l -> a[x+i] = a[y+i])
(* helps the proof of [lcp] (but not mandatory) and needed later for [le_trans] *) (** This lemma helps for the proof of [lcp] (but is not mandatory) and
lemma not_common_prefix_if_last_different: is needed later (for [le_trans]) *)
lemma not_common_prefix_if_last_char_are_different:
forall a:array int, x y:int, l:int. forall a:array int, x y:int, l:int.
0 <= l /\ x+l < a.length /\ y+l < a.length /\ a[x+l] <> a[y+l] -> 0 <= l /\ x+l < a.length /\ y+l < a.length /\ a[x+l] <> a[y+l] ->
not is_common_prefix a x y (l+1) not is_common_prefix a x y (l+1)
...@@ -108,13 +109,13 @@ lemma not_common_prefix_if_last_different: ...@@ -108,13 +109,13 @@ lemma not_common_prefix_if_last_different:
(** [is_longest_common_prefix a x y l] is true when [l] is the maximal (** [is_longest_common_prefix a x y l] is true when [l] is the maximal
length such that prefixes at positions [x] and [y] in array [a] length such that prefixes at positions [x] and [y] in array [a]
are identical. *) are identical. *)
predicate is_longest_common_prefix (a:array int) (x y:int) (l:int) = predicate is_longest_common_prefix (a:array int) (x y l:int) =
is_common_prefix a x y l /\ is_common_prefix a x y l /\
forall m:int. l < m -> not (is_common_prefix a x y m) forall m:int. l < m -> not (is_common_prefix a x y m)
(* helps proving [lcp] (but not mandatory), and needed (** This lemma helps for proving [lcp] (but again is not mandatory),
for proving [lcp_sym] and [le_trans] lemmas, and the post of [compare] and is needed for proving [lcp_sym] and [le_trans] lemmas, and the
function in the absurd case *) post-condition of [compare] function in the "absurd" case *)
lemma longest_common_prefix_succ: lemma longest_common_prefix_succ:
forall a:array int, x y l:int. forall a:array int, x y l:int.
is_common_prefix a x y l /\ not (is_common_prefix a x y (l+1)) -> is_common_prefix a x y l /\ not (is_common_prefix a x y (l+1)) ->
...@@ -136,7 +137,16 @@ let lcp (a:array int) (x y:int) : int ...@@ -136,7 +137,16 @@ let lcp (a:array int) (x y:int) : int
assert { not is_common_prefix a x y (!l+1) }; assert { not is_common_prefix a x y (!l+1) };
!l !l
end
module LCP_test
(** test harness for lcp *) (** test harness for lcp *)
use import array.Array
use import LCP
let test () = let test () =
let arr = Array.make 4 0 in let arr = Array.make 4 0 in
arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5; arr[0]<-1; arr[1]<-2; arr[2]<-2; arr[3]<-5;
......
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