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.