CASL/Summary-v1.0 -- 2.1.2.2 Operation Definitions

Go backward to 2.1.2.1 Operation Declarations
Go up to 2.1.2 Operations

2.1.2.2 Operation Definitions

      OP-DEFN         ::= op-defn OP-NAME OP-HEAD TERM
      OP-HEAD         ::= TOTAL-OP-HEAD | PARTIAL-OP-HEAD
      TOTAL-OP-HEAD   ::= total-op-head ARG-DECL* SORT
      PARTIAL-OP-HEAD ::= partial-op-head ARG-DECL* SORT
      ARG-DECL        ::= arg-decl VAR+ SORT
      VAR             ::= SIMPLE-ID

A definition OP-DEFN of a total operation with some arguments is written:

f (V₁₁, ..., V_1m₁:s₁; ...; V_n1, ..., V_{nm_n}:s_n):s = T

When the list of arguments is empty, the definition is simply written:

f :s = T

A definition OP-DEFN of a partial operation with some arguments is written:

f (V₁₁, ..., V_1m₁:s₁; ...; V_n1, ..., V_{nm_n}:s_n):? s = T

When the list of arguments is empty, the definition is simply written:

f :? s = T

It declares the operation name f as a total, respectively partial operation, with a profile having argument sorts s₁ (m₁ times), ..., s_n (m_n times) and result sort s. It also asserts the strong equation:

f(V₁₁, ..., V_{nm_n}) = T

universally quantified over the declared argument variables [CHANGED:] (which must be distinct, and are the only ones allowed in T), [] or just `f = T' when the list of arguments is empty.

In each of the above cases, the operation name f may occur in the term T, and may have any interpretation satisfying the equation--not necessarily the least fixed point.

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.
Comments to cofi-language@brics.dk