// @(#)$Id: SetToRMS-desugared.lh,v 1.7 1997/07/31 04:02:26 leavens Exp $

extern void SetToRMS(double & v, double x, double y) throw();
//@ behavior {
//@   requires informally "x and y are not too big";
//@   modifies v;
//@   ensures informally "v' is an approximation to"
//@                      "the root mean square of x and y";

//@ also

//@   requires (x*x) + (y*y) < DBL_MAX;
//@   modifies v;
//@   ensures  approx(v' * v', rational((x*x) + (y*y) / 2.0), 1/100);

//@ also

//@   requires (x*x) + (y*y) < DBL_MAX;
//@   modifies v;
//@   ensures  v' >= 0.0;
//@ }

[Index]

HTML generated using lcpp2html.