Dictionnaires

TYPE map {key result: type SUCH THAT Subtype(key, equality{t})}
    -- The domain of the map must have an equality operation
    -- with the standard interpretation.

INHERIT partial_order{map{key, result}}
IMPORT Subtype FROM type
IMPORT distinct FROM sequence{pair}

MODEL(default: result, pairs: set{pair})
INVARIANT ALL(m: map{key, result} :: single_valued(m.pairs)),
  ALL(m: map{key, result}, p: pair SUCH THAT
      p IN m.pairs :: p.y ~= default )

  MESSAGE create(v: result)
    REPLY(m: map{key, result})
      WHERE m.default = v, m.pairs = { }
      -- m[x] = v for all x.

  MESSAGE bind(x: key, y: result, m: map{key, result})
    REPLY(mm: map{key, result})
      WHERE mm[x] = y, mm.default = m.default,
        ALL(z: key SUCH THAT z ~= x :: mm[z] = m[z])

  MESSAGE remove(x: key, m: map{key, result})
    REPLY(mm: map{key, result})
      WHERE mm[x] = m.default, mm.default = m.default,
        ALL(z: key SUCH THAT z ~= x :: mm[z] = m[z])

  MESSAGE remove(s: set{key}, m: map{key, result})
    REPLY(mm: map{key, result})
      WHERE ALL(x: key :: IF x IN s THEN mm[x] = m.default
                          ELSE mm[x] = m[x] FI ),
        mm.default = m.default

  MESSAGE extend(m1 m2: map{key, result})
    REPLY(m3: map{key, result})
      WHERE ALL(x: key :: IF x IN m1 THEN m3[x] = m1.default
                          ELSE IF x IN m2 THEN m3[x] = m2[x]
                          ELSE m3[x] = m1.default FI ),
        m3.default = m1.default

  MESSAGE "["(m: map{key, result}, x: key)
    -- "["(m, x) is written m[x].
    REPLY(y: result)
      WHERE IF x IN m
            THEN SOME(p: pair :: p IN m.pairs &
                                 p.x = x & p.y = y )
            ELSE y = m.default FI

  MESSAGE "IN"(x: key, m: map{key, result}) REPLY(b: boolean)
    WHERE b <=> x IN domain(m)
    -- b <=> m[x] ~= m.default.

  MESSAGE equal(m1 m2: map{key, result})
    REPLY(b: boolean)
      WHERE b <=> ALL(x: key :: m1[x] = m2[x])

  MESSAGE "<="(m1 m2: map{key, result})
    REPLY(b: boolean)
      WHERE b <=> subset(m1.pairs, m2.pairs) &
                  m1.default = m2.default
      -- b <=> ALL(x: key :: m1[x] = m2[x] |
      --                     m1[x] = default(m2) ).

  MESSAGE domain(m: map{key, result})
    REPLY(s: set{key})
      WHERE s = SET(p: pair SUCH THAT p IN m.pairs :: p.x)
      -- s = {x | x in m}.

  MESSAGE range(m: map{key, result})
    REPLY(s: set{result})
      WHERE ALL(y: result :: y IN s <=>
                SOME(x: key :: m[x] = y) )
      -- s = {y | y = m[x] for some x},
      -- includes the default value.

  MESSAGE default(m: map{key, result})
    REPLY(y: result)
      WHERE y = m.default
      -- The default value of the map.

  MESSAGE scan(m: map{key, result})
    GENERATE(s1: sequence{pair})
    WHERE ALL(x: t :: x IN s1 <=> x IN m.pairs), distinct(s1)

  CONCEPT pair: type
    WHERE pair = tuple{x :: key, y :: result}

  CONCEPT single_valued(s: set{pair})
    VALUE(b: boolean)
    WHERE b <=> ALL(p1 p2: pair SUCH THAT p1 IN s & p2 IN s
                    :: p1.x = p2.x => p1.y = p2.y )
    -- The map associates at most one y value with each x value.
END