**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:
**[CHANGED:]**

*f*_{1}, ..., *f*_{n} : *T*,
*A*_{1}, ..., *A*_{m}

**[]** When the list *A*_{1}, ..., *A*_{m} is empty, the declaration
is written simply:
*f*_{1}, ..., *f*_{n} : *T*

It declares each operation name *f*_{1}, ..., *f*_{n} as a
total or partial operation, with profile as specified by the operation
type *T*, and as having the attributes
*A*_{1}, ..., *A*_{m} (if any).

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:

*s*_{1}×...×*s*_{n} -> *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:

*s*_{1}×...×*s*_{n} ->? *s*

When the list of argument sorts is empty, the type is
simply written
**[CHANGED:]** `*? s*'.
**[]** The operation profile determined by the type has argument sorts
*s*_{1}, ..., *s*_{n} and result sort *s*.
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.
**[CHANGED:]** (This can also be used to add attributes to operations that have
previously been declared without them.)
**[]** The attribute `associative` is written `**assoc**'. It asserts the
*associativity* of an operation *f*:

*f*(x, *f*(y,z)) = *f*(*f*(x,y),z)

The attribute of associativity moreover
implies a parsing annotation that
allows an
**[CHANGED:]** infix operation *f* of the form
**[]** ``__`*t*__' (or ``__
__`')
to be iterated without explicit grouping parentheses.
The attribute `commutative` is written `**comm**'. It asserts the
*commutativity* of an operation *f*:

*f*(x,y) = *f*(y,x)

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

*f*(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 *f*:

*f*(*T*,x) = x /\ *f*(x, *T*) = x

In practice, the unit *T* is normally a constant.
**[CHANGED:]** In any case, *T* must not contain any variables.
**[]** 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-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk