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:
- a set S of sorts;
- sets TFw,s, PFw,s, of total function symbols,
respectively partial function symbols, such that
TFw,s n PFw,s = Ø, for each function
profile (w,s) consisting of a sequence of
argument sorts w in S* and a result sort
s in S ( constants are treated as functions with no
arguments);
- sets Pw of predicate symbols, for each predicate
profile consisting of a sequence of argument sorts w in S*.
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 in S*, s in 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-v0.99-draft --DRAFT Version 0.99-- 25 March 1998.
Comments to cofi-language@brics.dk