@function fact : int -> int

@axiom A1:  fact(0) = 1
@axiom A2:  all n:int. n > 0 ==> fact(n) = n*fact(n-1)

@requires n >= 0
@ensures  f = fact(n)

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