Up Next
Go up to 2.1.2 Operations
Go forward to 2.1.2.2 Operation Definitions

2.1.2.1 Operation Declarations

  OP-DECL          ::= op-decl OP-NAME+ OP-TYPE OP-ATTR*
  OP-NAME          ::= ID

An operation declaration OP-DECL is written:

ON1, ..., ONn : T, A1, ..., Am
When the list A1, ..., Am is empty, the declaration is written simply:
ON1, ..., ONn : T

It declares each operation name ON1, ..., ONn as a total or partial operation, with profile as specified by the operation type T, and as having the attributes A1, ..., Am (if any).

Operation Types
  OP-TYPE          ::= TOTAL-OP-TYPE | PARTIAL-OP-TYPE
  TOTAL-OP-TYPE    ::= total-op-type SORTS SORT
  PARTIAL-OP-TYPE  ::= partial-op-type SORTS SORT
  SORTS            ::= sorts SORT*

A total operation type TOTAL-OP-TYPE with some argument sorts is written:

S1 × ... × Sn   ->   S
When the list of argument sorts is empty, the type is simply written `S'. The sign displayed as ` × ' may be input as `×' in ISO Latin-1, or as `*' in ASCII. The sign displayed as an arrow in LaTeX is input as `->'.

A partial operation type PARTIAL-OP-TYPE with some argument sorts is written:

S1 × ... × Sn  ->?  S
When the list of argument sorts is empty, the type is simply written `?S'.

The operation profile determined by the type has argument sorts S1, ..., Sn and result sort S.

Operation Attributes
  OP-ATTR          ::= BINARY-OP-ATTR | UNIT-OP-ATTR
  BINARY-OP-ATTR   ::= associative | commutative | idempotent
  UNIT-OP-ATTR     ::= unit-op-attr TERM

Operation attributes assert that the operations being declared (which must be binary) have certain common properties, which are characterized by strong equations, universally quantified over variables of the appropriate sort.

The attribute associative is written `assoc'. It asserts the  associativity of an operation ON:

ON(x, ON(y,z)) = ON(ON(x,y),z)
The attribute of associativity moreover implies a parsing annotation that allows an infix operation `__t__' (or `__ __') to be iterated without explicit grouping parentheses.

The attribute commutative is written `comm'. It asserts the  commutativity of an operation ON:

ON(x,y) = ON(y,x)

The attribute idempotent is written `idem'. It asserts the  idempotency of an operation ON:

ON(x,x) = x

The attribute UNIT-OP-ATTR is written `unit T'. It asserts that the value of the term T is the  unit (left and right) of an operation ON:

ON(T,x) = x   /\   ON(x, T) = x
In practice, the unit T is normally a constant.

The declaration enclosing an operation attribute is ill-formed unless the operation profile has exactly two argument sorts, both the same as the result sort.

CoFI Document: CASL/Summary --Version 0.99-- 21 April 1998.
Comments to cofi-language@brics.dk

Up Next