@function power: int, int -> int

@axiom A1: all x,y:int. y = 0  ==> power(x, y) = 1
@axiom A2: all x,y:int. y > 0  ==> power(x, y) = x * power(x, y-1)

@requires x > 0 && n > 0
@ensures y = power(x, n)

@program 
        @var x, y, i, n : int
         i = 1;
         y = x;
         @invariant y = power(x, i)  && 
                    i > 0  && i =< n
         while (i < n) {
            y = y * x;
            i = i + 1;
        }
@end
--