Up Next
Go up to 4.2 Axioms
Go forward to 4.2.2 Terms

4.2.1 Atomic Formulae

      ATOM ::= ... | MEMBERSHIP

As for many-sorted specifications, an atomic formula is well-formed (with respect to the current declarations) if it is well-sorted and expands to a unique atomic formula for constructing sentences of the underlying institution--but now for subsorted specifications, uniqueness is required only up to an  equivalence on atomic formulae and terms. This equivalence is the least one including fully-qualified terms that are the same up to profiles of operation symbols in the overloading relation < F and embedding, and fully-qualified atomic formulae that are the same up to the profiles of predicate symbols in the overloading relation < P and embedding.

The notions of when an atomic formula or term is well-sorted and of its expansion are indicated below for the various subsorting constructs. Due not only to overloading of predicate and/or operation symbols, but also to implicit embeddings from subsorts into supersorts, a well-sorted atomic formula [CHANGED:] may have several non-equivalent expansions, preventing it from being well-formed. Qualifications on operation and predicate symbols, or explicit sorts on terms, may be used to determine the intended expansion (up to the equivalence indicated above) and make the enclosing formula [] well-formed.

  • 4.2.1.1 Membership

  • CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
    Comments to cofi-language@brics.dk

    Up Next