4 Subsorting ConstructsTop2 Basic Constructs3 Subsorting Concepts

3 Subsorting Concepts

This chapter introduces the signatures, models, and sentences characterizing basic specifications with subsorts, extending Chapter 1. The notion of satisfaction for subsorted specifications is essentially as for many-sorted specifications.

The intuition behind the treatment of subsorts adopted here is to represent subsort inclusion by embedding (which is not required to be identity), commuting, as usual in order-sorted approaches, with overloaded operation symbols. In the language described in Chapter 4, however, no conditions such as `regularity' are imposed on signatures. Instead, terms and sentences that can be given different parses (up to the commutativity between embedding and overloaded symbols) are simply rejected as ill-formed.

  • 3.1 Signatures
  • 3.2 Models
  • 3.3 Sentences

  • CoFI Document: CASL/Summary -- Version: 1.0.1 -- 25 March 2001.
    Comments to cofi-language@brics.dk

    4 Subsorting ConstructsTop2 Basic Constructs3 Subsorting Concepts