// @(#)$Id: fact_liberal3.lh,v 1.5 1997/06/03 20:30:05 leavens Exp $

extern int fact_liberal2(int n) throw();
//@ behavior {
//@   uses FactorialTrait;
//@
//@   requires 0 <= n /\ factorial(n) < INT_MAX;
//@   ensures true;
//@ also
//@   requires true;
//@   ensures liberally result = factorial(n);
//@ }

[Index]

HTML generated using lcpp2html.