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

<PRE>
Array1 (E, I, A): <b>trait</b>
  % Basic one-dimensional array operators
  <b>introduces</b>
    assign: A, I, E -&gt; A
    __[__]: A, I -&gt; E
  <b>asserts</b>
    <b>forall</b> a: A, i, j: I, e: E
      assign(a, i, e)[j] ==
        <b>if</b> i = j <b>then</b> e <b>else</b> a[j]
</PRE>

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