[<A HREF="FloatingPoint.ps">PostScript</A>]

<PRE>
FloatingPoint (smallest, largest,
               gap, rational): <b>trait</b>
  <b>assumes</b> <A HREF="FPAssumptions.html">FPAssumptions</A>
  <b>includes</b>
    <A HREF="Rational.html">Rational</A>,
    <A HREF="TotalOrder.html">TotalOrder</A> (F)
  <b>introduces</b>
    mag: F -&gt; Q
    approx: F, Q, Q -&gt; Bool
    -__, abs, __\inv: F -&gt; F
    __+__, __*__, __-__, __/__: F, F -&gt; F
  <b>asserts</b>
    F <b>generated</b> <b>by</b> float
    <b>forall</b> f, f1, f2: F, q, t: Q
      f1 &lt;= f2 == rational(f1) &lt;= rational(f2);
      mag(f) == abs(rational(f));
      approx(f, q, t) ==
        abs(q) &lt;= largest
          =&gt; abs(rational(f) - q)
             &lt;= (smallest + 
                 (gap*(mag(f) + abs(q) + t)));
      approx(-f, -rational(f), 0);
      f \neq 0 =&gt; approx(f\inv, rational(f)\inv, 0);
      approx(abs(f), mag(f), 0);
      approx(f1 + f2, rational(f1) + rational(f2),
             mag(f1) + mag(f2));
      approx(f1 * f2, rational(f1) * rational(f2), 0);
      approx(f1 - f2, rational(f1) - rational(f2),
             mag(f1) + mag(f2));
      f2 \neq 0 
        =&gt; approx(f1/f2, rational(f1)/rational(f2), 0)
</PRE>

[<A HREF="toc.html">Table of Contents</A>] [<A HREF="index.html">Index</A>]