Ensembles

TYPE set{t: type SUCH THAT Subtype(t, equality{t})}
    -- The element type t must have an equality operation
    -- with the standard interpretation.
  INHERIT equality{set{t}}
  INHERIT partial_order{set{t}}
    RENAME "<=" AS subset
    RENAME "<" AS proper_subset
  IMPORT Commutative Associative FROM number{t}
  IMPORT Subtype FROM type
  IMPORT distinct FROM sequence{t}
    -- Generated by {empty, add} and partitioned by {"IN"}.

  MESSAGE empty
    -- Literal { } = empty.
    REPLY(s: set{t})
    WHERE ALL(x: t :: ~(x IN empty))

  MESSAGE add(x: t, s1: set{t})
    -- Literal {x} = add(x, empty).
    -- Literal {x, $s} = add(x, s).
    REPLY(s2: set{t})
    WHERE ALL(x y: t, s: set{t} ::
              x IN add(y, s) <=> (x = y | x IN s) )

  MESSAGE remove(x: t, s1: set{t})
    REPLY(s2: set{t})
    WHERE ALL(x y: t, s: set{t} ::
              x IN remove(y, s) <=> (x ~= y & x IN s) )

  MESSAGE "IN"(x: t, s: set{t})  -- "IN"(x, s) is written x IN s.
    REPLY(b: boolean)
    -- True if x is an element of the set s.

  MESSAGE "U"(s1 s2: set{t})  -- Literal {$s1, $s2} = s1 U s2.
    REPLY(s3: set{t})
    WHERE ALL(x: t :: x IN s3 <=> (x IN s1 | x IN s2))

  MESSAGE "-"(s1 s2: set{t}) REPLY(s3: set{t})
    WHERE ALL(x: t :: x IN s3 <=> (x IN s1 & ~(x IN s2)))

  MESSAGE intersection(s1 s2: set{t}) REPLY(s3: set{t})
    WHERE ALL(x: t :: x IN s3 <=> (x IN s1 & x IN s2))

  MESSAGE "*"{t1: type}(s1: set{t}, s2: set{t1})
    -- Cartesian product.
    REPLY(s3: set{tuple{c1:: t, c2:: t1}})
    WHERE ALL(x: t, y: t1 ::
              [c1:: x, c2:: y] IN s3 <=> (x IN s1 & y IN s2) )

  MESSAGE choose(s: set{t})
    WHEN size(s) > 0 REPLY(x: t)
      WHERE x IN s  -- Nondeterministic choice.
    OTHERWISE REPLY EXCEPTION empty_set

  MESSAGE size(s: set{t}) REPLY(n: nat)  -- Cardinality.
    WHERE n = NUMBER(x: t SUCH THAT x IN s :: x)

  MESSAGE equal(s1 s2: set{t}) REPLY(b: boolean)
    WHERE b <=> ALL(x: t :: x IN s1 <=> x IN s2)

  MESSAGE subset(s1 s2: set{t}) REPLY(b: boolean)
    WHERE b <=> ALL(x: t :: x IN s1 => x IN s2)

  MESSAGE ".."(x1 x2: t)  -- ".."(x1, x2) is written {x1 .. x2}.
    WHEN Subtype(t, partial_order) REPLY(s: set{t})
      WHERE ALL(x: t :: x IN s <=> x1 <= x <= x2)
    OTHERWISE REPLY EXCEPTION operation_not_applicable

  MESSAGE apply{rt: type}(f: function{t, rt}, s1: set{t})
    REPLY(s2: set{rt})
    WHERE ALL(y: rt :: y IN s2 <=>
              SOME(x: t :: x IN s1 & y = f(x)) )

  MESSAGE reduce{f: function{t, t, t}, identity: t
                 SUCH THAT Commutative(f), Associative(f),
                   ALL(y: t :: f(y, identity) = y) }
            (s: set{t})
      REPLY(x: t)
      WHERE IF s = { } THEN x = identity
            ELSE ALL(y: t :: y IN s =>
                     x = f(y, reduce{f}(s - {y})) ) FI

  MESSAGE reduce1{f: function{t, t, t} SUCH THAT
                  Commutative(f), Associative(f) }
            (s: set{t})
      WHEN size(s) > 1 REPLY(x: t)
        WHERE ALL(y: t :: y IN s =>
                  x = f(y, reduce1{f}(s - {y})) )
      WHEN size(s) = 1
        REPLY(x: t) WHERE x IN s
      OTHERWISE REPLY EXCEPTION empty_reduction_undefined

  MESSAGE scan(s: set{t})
    GENERATE(s1: sequence{t})
    WHERE ALL(x: t :: x IN s1 <=> x IN s), distinct(s1)
END