Up Next
Go up to 1 Basic Concepts
Go forward to 1.2 Models

1.1 Signatures

A  many-sorted signature Sigma= (S,TF,PF,P) consists of:

Constants and functions are also referred to as  operations, following the traditions of algebraic specification.

Note that symbols used to identify sorts, operations, and predicates may be  overloaded, occurring in more than one of the above sets. To ensure that there is no ambiguity in sentences at this level, however, function symbols f and predicate symbols p are always  qualified by profiles when used, written fw,s and pw respectively. (The language considered in Chapter 2 allows the omission of such qualifications when these are unambiguously determined by the context.)

A  many-sorted signature morphism sigma: (S,TF,PF,P) -> (S',TF',PF',P') consists of a mapping from S to S', and for each w e S*, s e S, a mapping between the corresponding sets of function, resp. predicate symbols. A partial function symbol may be mapped also to a total function symbol, but not vice versa.

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

Up Next