// @(#)$Id: make_sratl.lh,v 1.8 1997/07/31 17:25:53 leavens Exp $
struct sratl { int num; int den; };
extern sratl& make_sratl(int n, int d) throw();
//@ behavior {
//@   requires d > 0;
//@   ensures fresh(result, result'.num, result'.den)
//@           /\ assigned(result, post)
//@           /\ assigned(result.num, post) /\ assigned(result.den, post)
//@           /\ result'.num' = n /\ result'.den' = d;
//@ }

[Index]

HTML generated using lcpp2html.