// @(#)$Id: exercise.txt,v 1.1 1995/09/14 23:03:45 leavens Exp $

Start reading, or read chapter 4 of
``Larch: Languages and Tools for Formal Specification''
by John V. Guttag, James J. Horning, et al. (Springer-Verlag, 1993).
This gives you the basics of LSL.  Reading at least sections 4.1,
and 4.3-4.5 should be considered required before continuing.

Fill in the following trait outline with a specification of
the factorial function.  If you have expercience with functional
programming, think of that when you write this trait.

	% this is a comment
	answer1: trait
	  includes Integer(int for Int)   % see appendix A, page 163
		                          % of Guttag and Horning's book
	  introduces
	    factorial: ...
	  asserts
	    \forall n: int
	      factorial(n) == ...;
	  implies
	    equations
	      factorial(0) == 1;
	      factorial(1) == 1 * factorial(0);
	      factorial(2) == 2 * factorial(1);
	      factorial(3) == 3 * factorial(2);

Your exercise is to fill in the missing part indicated by the dots (...) above.

Try using the LSL checker (it may be the command named lsl on your system)
to check your work for syntax and type problems.
To do this, put your LSL specification in a file answer1.lsl (in some other
directory, as you probably can't write into our answer file).
Then type (on Unix anyway)
	lsl answer1.lsl
to check the file.
If it just says ``Finished checking LSL traits'', then your work was fine.