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

<PRE>
IntegerPredicates (Int): <b>trait</b>
  % Frequently used subranges of the integers
  <b>assumes</b> <A HREF="Integer.html">Integer</A>
  <b>introduces</b>
    InRange: Int, Int, Int -&gt; Bool
    Natural, Positive, Signed, Unsigned: Int -&gt; Bool
    maxSigned, maxUnsigned: -&gt; Int
  <b>asserts</b> <b>forall</b> n, low, high: Int
    InRange(n, low, high) == low &lt;= n /\ n &lt;= high;
    Natural(n) == n &gt;= 0;
    Positive(n) == n &gt; 0;
    Signed(n) ==
      InRange(n, -succ(maxSigned), maxSigned);
    Unsigned(n) == InRange(n, 0, maxUnsigned)
  <b>implies</b> <b>forall</b> n: Int
    Positive(n) =&gt; Natural(n);
    Unsigned(n) =&gt; Natural(n)
</PRE>

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