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

// The most plausible answer, which, as in the hint,
// uses the trait answer1.lsl.  (Normally that would be given another name.)

//@ uses answer1;

unsigned int fact(unsigned int n) throw();
//@ behavior {
//@  requires factorial(n) <= UINT_MAX;
//@  ensures result = factorial(n);
//@ }

/*
 Why is a precondition necessary?  Because fact always returns a number
 that is at least as large as its argument, and if the number is too big,
 then overflow will occur.  Some of the other answers will explore
 other ways of dealing with this.  The name UINT_MAX comes from the
 Larch/C++ trait unsignedInt.  It is intended to be the
 largest unsigned integer.

 But most of the interest in this exercise is in the trait.
 Why is the trait necessary?   That is, why can't you use the following
 formula as the postcondition?
 (1)	result = if n = 0 then n*fact(n-1);
 The answer is that you cannot use a C++ function, fact, in the postcondition,
 becuase only trait functions can appear in the postcondition.
 The postcondition is purely mathematical, and trait functions live in that
 world.  A C++ function lives in a different world.
 See the trait in the file answer1.lsl in this directory for the rest of
 this answer.

 Why is the following implementation of the above specification incorrect?

	// C++ code in factorial.C
	unsigned int factorial(unsigned int n) throw() {
	  if (n == 0) then {
	    return(1);
	  } else {
            return n * factorial(n - 1);
          }
	}

 Hmm...  it looks okay (at least it's supposed to!).
 But it has the wrong interface: look at the name of the function!
 An implementation of a function specification must have the same name
 as that specified.  And an implementation of a Larch/C++ specification also
 requires a header file.  Can you write a correct implementation?

*/