// @(#)$Id: fact_liberal2.lh,v 1.6 1997/06/03 20:30:04 leavens Exp $

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

[Index]

HTML generated using lcpp2html.