// @(#)$Id: answer2.h,v 1.3 1997/06/03 23:06:52 leavens Exp $

// It's possible, by a bit of logical trickery,
// to dispense with writing a trait.
// But compare the readability of the following answer with answer1.

unsigned int fact(unsigned int n) throw();
//@ behavior {
//@   requires \exists f:unsignedInt (f <= UINT_MAX /\   // f is factorial(n)
//@ 	(\forall k:unsignedInt ((0 < k /\ k <= n) \implies mod(f,k) = 0)));
//@   ensures if n = 0 then result = 1
//@ 	  else \forall k:unsignedInt
//@ 			 ((0 < k /\ k <= n) \implies mod(result,k) = 0);
//@ }

/*
 Let's explore this a bit.  Can the precondition be satisfied if n is 0?
 Substituting 0 for n in the precondition, we get:
 \exists f:unsignedInt (f <= UINT_MAX /\
	(\forall k:unsignedInt ((0 < k /\ k <= 0) \implies mod(f,k) = 0)))
 Since there is no k such that 0 < k and k <= 0, the implication is true,
 and so the \forall is true.  Hence the whole thing boils down to 
	 \exists f:unsignedInt (f <= UINT_MAX)
 which should be satisfiable.

 How about the postcondition when n is 0?  Clearly that's taken care of.
 But why was the if-then-else needed?  Because by the same reasoning as above,
 when n is 0, the \forall in the postcondition is true regardless of the
 value of result!

 We leave it to you to check that this specification is correct in all
 the other cases.  (Thinking about it a bit will convince you of the value
 of writing a trait.)
*/