@function fact : int -> int
@function power: int, int -> int

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

@axiom P1:  all x:int. power(x,0) = 1
@axiom P2:  all x,n:int. n > 0 ==> power(x,n) = x*power(x,n-1)

@requires  true
@ensures  s =< 1    // a somewhat trivial condition for sine!

@program 
  @var i, s, n, x, sign : int
  i = 1;
  s = 0;
  sign = 1;
  
  sign = (0-1)*sign;
  i = i + 2;
  s = s + sign*power(x,i)/fact(i);
 
  sign = (0-1)*sign;
  i = i + 2;
  s = s + sign*power(x,i)/fact(i);

  sign = (0-1)*sign;
  i = i + 2;
  s = s + sign*power(x,i)/fact(i);
  
@end
--