# The Specification Language

The specification formalism provided in the ELAN system is close to the algebraic specification formalism. Signatures introduce sorts of data and operations applied of them. One particularity of ELAN is to provide mixfix syntax for operators. For defining Booleans for instance, a sort Bool is declared inhabited by two constants true and false. Boolean terms are constructed with operators and, or, not. Attributes assocLeft, assocRight and AC may be used to declare an operator as left-associative, right-associative for parsing purposes, or associative and commutative. The associativity and commutativity axioms are called structural axioms and their application is embedded into the matching process. Priorities may be defined too, using the attribute pri, and aliased syntactic forms for an operator are introduced with an attribute alias.
module boolean
sort Bool; end
operators global
true : Bool;
false : Bool;
@ and @ : (Bool Bool) Bool assocLeft pri 100;
@ or @ : (Bool Bool) Bool assocLeft pri 100;
(@ and @) : (Bool Bool) Bool assocLeft pri 100 alias @ and @:;
(@ or @) : (Bool Bool) Bool assocLeft pri 100 alias @ or @:;
not @ : (Bool ) Bool pri 200;
not (@) : (Bool ) Bool pri 200 alias not @:;
end

It may sometimes be useful to define an injection of one sort into another. This is done in ELAN with an anonymous operator. Assume that we want to define a sort Constraint embedding the sort Bool, so that any boolean formula becomes a constraint. This is expressed in ELAN as follows:
module constraint
sort Constraint; end
operators global
@ : (Bool) Constraint;
end

In the algebraic style, the semantics of operations on data is described by a set of first-order formulas. In ELAN, the formulas are a very general form of rewrite rules with conditions and local evaluations. For instance, simple rewrite rules for booleans are given as follows:
rules for Bool
P : Bool;
global
[] true or P => true end
[] false or P => P end
[] true and P => P end
[] false and P => false end
[] not true => false end
[] not false => true end
end

The two values true and false are said irreducible or in normal form. This set of rules is terminating and confluent, which ensures that any boolean formula has a unique normal form. For such systems, it is not needed to specify in which order the rules are applied, nor at which position in the term. The ELAN system adopts in such a case a strategy by default which selects the leftmost and innermost redex at each step. However in many situations, and especially to deal with non-confluent or non-terminating rewrite systems, it is suitable to express which rule to apply. For specifying this kind of control, ELAN introduces the possibility to name rules, using brackets in front of a rule to enclose its name. In the previous boolean example, the names are unspecified and such rules are said unlabelled. The capability of specifying control is a main originality of ELAN compared to other specification languages. Let us explain in more details how to build strategies that compute one or several results, specify the order of applied rules, or iterate as much as possible the application of a strategy or a rule on a term.