// @(#)$Id: miracle.lh,v 1.9 1997/01/04 16:58:57 leavens Exp $
extern void miracle();
//@ behavior {
//@   extern everything;
//@
//@   requires true;
//@   modifies everything;
//@   trashes everything;
//@   ensures true;
//@ also
//@   requires true;
//@   modifies everything;
//@   trashes everything;
//@   ensures liberally false;
//@ }

[Index]

HTML generated using lcpp2html.