Abstract

Implementation of formal specifications is very important in formal software development and can be described in terms of simple logical concepts. Formal specifications are presentations of theories in many-sorted first-order logic, and an implementation of a formal specification on another formal specification amounts to an interpretation of the former into a conservative extension of the latter. Here we present and analyse some sort introducing constructs akin to those found in many programming languages. This is of importance because it occurs often in implementing formal specifications, when new sorts are ‘constructed’ from the concrete ones. We specify these constructs and show that these specifications provide extensions with behaviour close to that of the familiar extensions by definitions