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

% In this answer, we use the absolute values of integers,
% instead of testing for negatives.  This is another way to define
% factorial for negatives, although if one doesn't care about factorial's
% of negative numbers, then this may be thought of as cluttering up
% the specification with useless detail.

% This specification also uses pred(abs(n)) instead of abs(n)-1.
% See the integer trait in Guttag and Horning's LSL Handbook (p. 163).

answer3: trait      % note we had to change this line to match the file name
  includes Integer(int for Int)
  introduces
    factorial: int -> int
  asserts
    \forall n: int
      factorial(n)
       == if abs(n) = 0 then 1 else abs(n) * factorial(pred(abs(n)));
  implies
    equations
      factorial(0) == 1;
      factorial(1) == 1 * factorial(0);
      factorial(2) == 2 * factorial(1);
      factorial(3) == 3 * factorial(2);