diff --git a/examples/word_common_factor.mlw b/examples/word_common_factor.mlw index a9f7f05bc75c84ab77ee90c5d17cde71ba4935a4..0e71e8276f13343c9632b20358a59ac44e64de05 100644 --- a/examples/word_common_factor.mlw +++ b/examples/word_common_factor.mlw @@ -1,7 +1,12 @@ (** {2 Common factor of two words} - If `a ++ b = b ++ a` then `a` and `b` are powers of a common word. *) + If `a ++ b = b ++ a` then `a` and `b` are powers of a common word. + + Authors: Jean-Christophe FilliĆ¢tre (CNRS) + Andrei Paskevich (Univ Paris-Sud) + +*) use int.Int use seq.Seq @@ -21,21 +26,17 @@ let rec lemma power_add (w: word) (n1 n2: int) ensures { power w (n1 + n2) == power w n1 ++ power w n2 } = if n1 > 0 then power_add w (n1 - 1) n2 -let rec remove_prefix (a b: word) : word - requires { length a <= length b && b[0 .. length a] == a } - ensures { b = a ++ result } - variant { length a } - = if length a = 0 then b else remove_prefix a[1..] b[1..] - let rec common_factor (a b: word) : (w: word, ka: int, kb: int) requires { a ++ b == b ++ a } - ensures { ka >= 0 /\ a == power w ka /\ kb >= 0 /\ b == power w kb } + ensures { ka >= 0 /\ a == power w ka } + ensures { kb >= 0 /\ b == power w kb } variant { length a, length b } = if length a = 0 then b, 0, 1 else if length b = 0 then a, 1, 0 else if length a <= length b then begin - let c = remove_prefix a b in + let c = b[length a ..] ensures { b == a ++ result } in let w, ka, kc = common_factor a c in w, ka, ka + kc end else - let w, ka, kb = common_factor b a in w, kb, ka + let w, ka, kb = common_factor b a in + w, kb, ka diff --git a/examples/word_common_factor/why3session.xml b/examples/word_common_factor/why3session.xml index dcb7294dacfeca6c6f8f37e08f0e9d10720a590d..c6cc77f9fc84cdc67674bef123cedde9603388b4 100644 --- a/examples/word_common_factor/why3session.xml +++ b/examples/word_common_factor/why3session.xml @@ -14,51 +14,54 @@ - - - - + + + + - + - + - - + + - + - + - + - + - + - + - + - + - - + + + + + diff --git a/examples/word_common_factor/why3shapes.gz b/examples/word_common_factor/why3shapes.gz index 0b9d21306e087a145edf2946925023947017a15a..249e9bfb481a8fdcd6c77bf2509f36dac6c7bd74 100644 Binary files a/examples/word_common_factor/why3shapes.gz and b/examples/word_common_factor/why3shapes.gz differ