why3/examples_in_progress/ewd650.mlw

(* EWD 650: A Theorem About Odd Powers of Odd Integers *)

module EWD650

  use int.Int
  use int.Power
  use number.Parity
  use number.Divisibility
  use ref.Refint

  let theorem (p: int) (k: int) (r: int)
    requires { p >= 1 /\ odd p /\ k >= 1 /\ 1 <= r < power 2 k /\ odd r }
    ensures  { 1 <= result < power 2 k }
    ensures  { divides (power 2 k) (power result p - r) }
    ensures  { odd result }
  = let x = ref 1 in
    let d = ref 2 in
    for i = 1 to k do
      invariant { !d = power 2 i /\ 1 <= !x < !d }
      invariant { divides !d (power !x p - r) /\ odd !x }
      if not (divides (2 * !d) (power !x p - r)) then x := !x + !d;
      d := 2 * !d
    done;
    !x

end