Wiki Agenda Contact Version française

Common factor of two words

If ab = ba then the words a and b are powers of a common word.


Authors: Jean-Christophe Filliâtre / Andrei Paskevich

Topics: Words

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


Common factor of two words

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
use seq.FreeMonoid

type char
type word = seq char

let rec function power (w: word) (n: int) : word
  requires { n >= 0 }
  variant  { n }
  = if n = 0 then empty else w ++ power w (n - 1)

let rec lemma power_add (w: word) (n1 n2: int)
  requires { n1 >= 0 && n2 >= 0 }
  variant  { n1 }
  ensures  { power w (n1 + n2) == power w n1 ++ power w n2 }
  = if n1 > 0 then power_add w (n1 - 1) n2

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 }
  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 = 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

download ZIP archive

Why3 Proof Results for Project "word_common_factor"

Theory "word_common_factor.Top": fully verified

ObligationsAlt-Ergo 2.2.0Alt-Ergo 2.4.1CVC4 1.6
VC for power------0.05
VC for power_add0.14------
VC for common_factor---------
split_vc
precondition0.01------
postcondition------0.14
variant decrease------0.05
precondition---------
split_all_full
precondition------0.06
variant decrease---------
split_all_full
variant decrease------0.05
variant decrease------0.05
variant decrease------0.04
variant decrease------0.04
variant decrease------0.04
variant decrease------0.03
precondition------0.03
postcondition------0.06
postcondition---0.10---