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