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

<PRE>
FiniteMap (M, D, R): <b>trait</b>
  % An M is a map from D's to R's.
  <b>introduces</b>
    {}: -&gt; M
    update: M, D, R -&gt; M
    apply: M, D -&gt; R
    defined: M, D -&gt; Bool
  <b>asserts</b> 
    M <b>generated</b> <b>by</b> {}, update
    M <b>partitioned</b> <b>by</b> apply, defined
    <b>forall</b> m: M, d, d1, d2: D, r: R
      apply(update(m, d2, r), d1) ==
        <b>if</b> d1 = d2 <b>then</b> r <b>else</b> apply(m, d1);
      ~defined({}, d);
      defined(update(m, d2, r), d1) ==
        d1 = d2 \/ defined(m, d1)
  <b>implies</b>
    <A HREF="Array1.html">Array1</A> (update <b>for</b> assign, apply <b>for</b> __[__],
            M <b>for</b> A, D <b>for</b> I, R <b>for</b> E)
    <b>converts</b> apply, defined
      exempting <b>forall</b> d: D apply({}, d)
</PRE>

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