method Section5RemarkThree(A:int, B:int) returns (z:int) 
  requires A > 0
  requires B >= 0
  ensures z == power(A,B)
{
  var x := A;
  var y := B;
  z := 1;
 
  while y != 0
    invariant x > 0
    invariant y >= 0
    invariant power(A, B) == z * power(x, y)
  {
    halfExponentSquareBase(x, if odd(y) then y-1 else y);
 
    if odd(y)
    {
      y := y - 1;
      z := z * x;
    }
    y := y/2;
    x := x * x;
  }
}
 
lemma halfExponentSquareBase(x:int,y:int)
  requires x > 0
  requires y >= 0
  requires even(y)
  ensures power(x, y) == power(x*x, y/2)
 {
   if y != 0 {
     halfExponentSquareBase(x,y-2);
   }
 }
 
predicate method even(n: nat)
   ensures even(n) <==> n % 2 == 0
{
   if n == 0 then true else odd(n-1)
}
 
predicate method odd(n: nat)
   ensures odd(n) <==> n % 2 != 0
{
   if n == 0 then false else even(n-1)
}
 
function power(x:int, n:int):int
{
  if n <= 0 then 1
  else x * power(x, n-1)
}

method Section5RemarkThree(A:int, B:int) returns (z:int) requires A > 0 requires B >= 0 ensures z == power(A,B) { var x := A; var y := B; z := 1; while y != 0 invariant x > 0 invariant y >= 0 invariant power(A, B) == z * power(x, y) { halfExponentSquareBase(x, if odd(y) then y-1 else y); if odd(y) { y := y - 1; z := z * x; } y := y/2; x := x * x; } } lemma halfExponentSquareBase(x:int,y:int) requires x > 0 requires y >= 0 requires even(y) ensures power(x, y) == power(x*x, y/2) { if y != 0 { halfExponentSquareBase(x,y-2); } } predicate method even(n: nat) ensures even(n) <==> n % 2 == 0 { if n == 0 then true else odd(n-1) } predicate method odd(n: nat) ensures odd(n) <==> n % 2 != 0 { if n == 0 then false else even(n-1) } function power(x:int, n:int):int { if n <= 0 then 1 else x * power(x, n-1) }