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 | FUN-DEFN | PRED-DECL 
                   |  DATATYPE-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. A function definition FUN-DEFN declares a function symbol, and determines a sentence that defines its values. A DATATYPE-DECL determines a sort together with some cosntructor and (optional) selector functions, and sentences defining the selector functions on the values given by the constructors with which they are associated. 

ID               ::=  SIMPLE-ID
SIMPLE-ID         --  structure insignificant for abstract syntax
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.

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-ATTR*
FUN-TYPE         ::=  TOTAL-FUN-TYPE | PARTIAL-FUN-TYPE
TOTAL-FUN-TYPE   ::=  total-fun-type SORTS SORT
PARTIAL-FUN-TYPE ::=  partial-fun-type SORTS SORT
SORTS            ::=  sorts 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. 

FUN-ATTR         ::=  BINARY-FUN-ATTR | UNIT-FUN-ATTR
BINARY-FUN-ATTR  ::=  associative | commutative | idempotent
UNIT-FUN-ATTR    ::=  unit-fun-attr FUN-SYMB
A function attribution FUN-ATTR in a FUN-DECL determines sentences asserting that the declared functions (which must be binary) all have the property of being  associative,  commutative, or  idempotent, or of having a particular constant (declared separately) as both left and right  unit. It is ill-formed unless the two argument sorts of the specified FUN-TYPE are the same as the result sort. 

FUN-DEFN         ::=  fun-defn FUN-NAME VAR-DECL* SORT TERM
A function (or constant) definition FUN-DEFN declares a partial function with the specified FUN-NAME, with a profile having the sorts of the variable declarations VAR-DECL* as argument sorts and the specified SORT as result sort. It also determines a sentence, universally quantified over the declared variables, strongly equating the value of the application of the function to the variables with the value of the specified TERM.

2.1.3 Predicates

PRED-DECL        ::=  pred-decl PRED-NAME+ PRED-TYPE
PRED-TYPE        ::=  pred-type SORTS
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.

2.1.4 Datatype Declarations

DATATYPE-DECL    ::=  datatype-decl SORT ALTERNATIVE+
ALTERNATIVE      ::=  CONSTRUCT
A datatype declaration DATATYPE-DECL declares its component SORT. For each alternative CONSTRUCT it declares the required constructor and selector functions, and determines axioms asserting the expected relationship between any selectors and the constructors. All sorts used in each ALTERNATIVE must be declared in the local environment provided to the enclosing DATATYPE-DECL.

Note that a DATATYPE-DECL allows models where the ranges of the constructors are not disjoint, and where not all values are the results of constructors. This looseness can be eliminated in a general way by use of free extensions in structured specifications (summarized in Part II), or within basic specifications by use of sort generation constraints and (rather tedious) axioms. 

CONSTRUCT        ::=  construct FUN-NAME COMPONENT*
A function FUN-NAME specified in a CONSTRUCT is declared as a total constructor. Each COMPONENT specifies one argument sort for the constructor; its result sort is the SORT of the enclosing DATATYPE-DECL.

When all the ALTERNATIVE constructs are CONSTRUCTSs with no components, the declared type corresponds to an (unordered) enumeration of constants. 

COMPONENT        ::=  component FUN-NAME? SORT
A COMPONENT without a FUN-NAME merely provides its SORT as an argument sort for the constructor for the enclosing CONSTRUCT.

A COMPONENT with a FUN-NAME moreover declares the function FUN-NAME as a selector, with the argument sort given by the enclosing DATATYPE-DECL, and with the indicated result sort. The function is declared as partial (also when there is only one ALTERNATIVE in the enclosing DATATYPE-DECL).

CoFI Document: CASL/Summary-v0.97 --Version 0.97-- 20 May 1997.
Comments to cofi-language@brics.dk

Up Next