CASL/Summary -- 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:

ON (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:

ON :S = T

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

ON (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:

ON :?S = T

It declares the operation name ON 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:

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

universally quantified over the declared argument variables, or just `ON = T' when the list of arguments is empty.

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

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