Go up to Basic Constructs
Go forward to Variable Declarations

Signature Declarations

SIG-DECL        ::=   SORT-DECL | FUN-DECL | PRED-DECL
A sort declaration SORT-DECL determines one or more sorts. A function declaration FUN-DECL determines one or more function symbols of a particular profile; similarly for a predicate declaration PRED-DECL. Function and predicate symbols may be overloaded, being declared with several different profiles in the same basic specification. The declaration of several symbols together in a single DECL is equivalent to their separate declarations in a series of similar DECLs. 

ID              ::=   SIMPLE-ID
SIMPLE-ID       -- structure insignificant
The internal structure of simple identifiers SIMPLE-ID, used to identify sorts, functions, and predicates, is insignificant (ID is extended with compound identifiers in a later section). The same identifier may be used for both a function and a predicate in the same BASIC-SPEC, but not for a sort and for a function or predicate.

Sorts

SORT-DECL       ::=   sort-decl SORT+
SORT            ::=   ID
A sort declaration SORT-DECL determines that each of the sorts in the list SORT+ is in the signature.

Constants and Functions

FUN-DECL        ::=   fun-decl FUN-NAME+ FUN-TYPE
FUN-TYPE        ::=   fun-type TOTALITY SORT* SORT
TOTALITY        ::=   total | partial
FUN-NAME        ::=   ID
A constant is treated as a function with no arguments (thus its value may be undefined when it is declared to be partial). A function declaration FUN-DECL determines that each function name in the list FUN-NAME+ is in the signature, being in the set of partial or total function symbols, and with the specified argument sorts and result sort, according to the function type FUN-TYPE.

Predicates

PRED-DECL       ::=   pred-decl PRED-NAME+ PRED-TYPE
PRED-TYPE       ::=   pred-type SORT*
PRED-NAME       ::=   ID
A predicate declaration PRED-DECL determines that each predicate name in the list PRED-NAME+ is in the signature, with the specified argument sorts according to the predicate type PRED-TYPE.
CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk