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 list 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 ID may be used simultaneously to identify different kinds of entities, e.g., sorts, functions and predicates, in the same BASIC-SPEC.

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         ::=  SORT | PARTIAL-CON-TYPE | 
!                    |  TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE
! PARTIAL-CON-TYPE ::=  partial-con-type SORT
! TOTAL-FUN-TYPE   ::=  total-fun-type SORT+ SORT
! PARTIAL-FUN-TYPE ::=  partial-fun-type SORT+ SORT
  FUN-NAME         ::=  ID
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 argument sorts SORT+ and result SORT as specified by the function type FUN-TYPE. A FUN-TYPE consisting of just a SORT is for declaring total constants, which correspond to functions of no arguments. A PARTIAL-CON-TYPE is for declaring partial constants.

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 Document: LanguageSummary --DRAFT, Version 0.96-- 30 April 1997.
Comments to cofi-language@brics.dk