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

<PRE>
Array2 (E, I1, I2, A): <b>trait</b>
  % Basic two-dimensional array operators
  <b>introduces</b>
    assign: A, I1, I2, E -&gt; A
    __[__, __]: A, I1, I2 -&gt; E
  <b>asserts</b>
    <b>forall</b> a: A, i1, j1: I1, i2, j2: I2, e: E
      assign(a, i1, i2, e)[j1, j2] ==
        <b>if</b> i1 = j1 /\ i2 = j2 <b>then</b> e <b>else</b> a[j1, j2]
</PRE>

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