Up Next
Go up to 2 Basic Constructs
Go forward to 2.2 Variable Declarations

2.1 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.
[DTS] When the BASIC-SPEC is used in an enrichment of another specification, does this restriction apply to the whole enriched specification and not just the enrichment, so e.g. it is also forbidden for an identifier to be used for a sort in the specification being enriched and for a function in the enrichment? (Either the restriction should be abandoned, or it should be imposed uniformly.)
Discharged: The restriction is abandoned.

2.1.1 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.

2.1.2 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.

2.1.3 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 Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk

Up Next