NonDeterministic Computations Rules Specifications Modularity and parameterization 
Next Page

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 firstorder 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 nonconfluent or nonterminating 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.