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

f1, ..., fn : T, A1, ..., Am
[] When the list A1, ..., Am is empty, the declaration is written simply:
f1, ..., fn : T

It declares each operation name f1, ..., fn 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 [CHANGED:] `? 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. [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 `unitT'. 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

Up Next