Skip to content
STELF
Documentation out of dateLearn more

%mode

The %mode declaration specifies the way in which a relation is intended to be used, by specifying those arguments that are inputs or outputs. STELF then checks that all constants defining the relation respect the mode specified (are “well-moded”).

The %mode declaration is an important part of the specification of a totality assertion. In the “for all/exists” statement about a relation, the “for all” terms are the input arguments to the relation, and the “exists” terms are its outputs.

Syntax

Section titled “Syntax”

A mode declaration for the family id with n arguments usually takes the following (“short”) form:

%mode id a1 ... an.

Each argument ai is +ID, -ID, or *ID for some distinct identifier ID.

  • + indicates that the argument is an input,
  • - indicates that the argument is an output, and
  • * indicates that the argument is unrestricted. (The * mode is rarely used.)

For example, a natural mode for the plus relation on natural numbers is:

%sort plus {_ nat} {_ nat} {_ nat} %.
%mode plus %in %in %out %.

The names N1..N3 are arbitrary, but each must be distinct.

Full form

Section titled “Full form”

The short mode declaration above only specifies the mode for explicit parameters; the modes for implicit parameters are then assigned automatically. Occasionally, one needs to use a “full” form to specify the modes of implicit parameters:

%mode p1 ... pm term.

Each parameter pi is +\{ID : term\}, -\{ID : term\}, or *\{ID : term\} for distinct identifiers ID. Terms may refer to the variables bound in the previous parameters. For example, the full mode declaration corresponding to the short one above would be:

%sort plus {_ nat} {_ nat} {_ nat} %.
%mode {%in N1 nat} {%in N2 nat} {%out N3 nat} plus N1 N2 N3 %.

See also

Section titled “See also”