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

<PRE>
BinaryTree (E, T): <b>trait</b>
  % One of the many interesting tree structures
  <b>introduces</b>
    [__]: E -&gt; T
    [__, __]: T, T -&gt; T
    content: T -&gt; E
    first, second: T -&gt; T
    isLeaf: T -&gt; Bool
  <b>asserts</b>
    T <b>generated</b> <b>by</b> [__], [__, __]
    T <b>partitioned</b> <b>by</b> content, first, second, isLeaf
    <b>forall</b> e: E, t1, t2: T
      content([e]) == e;
      first([t1, t2]) == t1;
      second([t1, t2]) == t2;
      isLeaf([e]);
      ~isLeaf([t1, t2])
  <b>implies</b> <b>converts</b> isLeaf
</PRE>

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