// @(#)$Id: SetToRMS-refined.lh,v 1.6 1997/06/13 05:23:46 leavens Exp $
#include "SetToRMS-formal.lh"
//@ refine SetToRMS
//@ by
extern void SetToRMS(double & v, double x, double y) throw();
//@ behavior {
//@ requires (x*x) + (y*y) < DBL_MAX;
//@ modifies v;
//@ ensures v' >= 0.0;
//@ }
[Index]
HTML generated using lcpp2html.