Notes on Structured Programming – Section 5, Remark 3

Here is a Dafny proof of the “exercise for the reader” from section 5 of E.W.Dijkstra’s “Notes on Structured Programming” monograph in the book “Structured Programming (1972)”.

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