% specification component 27.2.1991 hk


\chapter{Specification Component}

\label{spec.chap}
In this chapter we discuss the 
specification capabilities of MAS. In the first section we 
give an overview over the design considerations. 
Then we define the syntax of the respective language 
constructs and then we discuss the semantics of the 
constructs. 
\index{specification component}

\section{Overview} %--------------------------

MAS views mathematics in the 
sense of universal algebra and model theory and is 
in some parts influenced by category theory.
In contrast to other computer algebra systems
(like Scratchpad II \cite{Jenks 85}),
\index{Scratchpad II}
the MAS concept provides a clean seperation of 
computer science and mathematical concepts. 
The MAS language and its interpreter has no 
{\em knowledge of mathematics} and mathematical objects; 
however it is capable to describe (specify) and implement 
mathematical objects and to 
use libraries of implemented mathematical methods. 
Further the imperative programming, the conditional rewriting 
and function overloading concepts are seperated in a clean way.
The denotational semantics of the MAS language is 
discussed in \cite{Kredel 91}.
\index{semantics}\index{denotational semantics}
\index{algebra}\index{universal algebra}\index{model theory}
\index{category theory}

MAS includes the capability to 
join {\em specifications} and to rename sorts and operations 
during import of specifications. 
This allows both the specification of abstract objects 
(rings, fields),
concrete objects (integers, rational numbers) and 
concrete objects in terms of abstract objects 
(integers as a model of rings). 
Specifications can be parameterized in the sense of 
$\lambda$ abstraction.
\index{join}\index{rename}
\index{concrete objects}\index{abstract objects}

The {\em semantics} of a specification can be 
described either by implementations, axioms or models.
\index{specification}
The {\em implementation} part describes 
(imperative) procedures and data representations.   
\index{implementation}

The {\em axioms} part describes conditional rewrite rules  
which define a reduction relation on the term algebra generated 
by the sorts and operations of the specification. 
The semantics is therefor the class of models of the 
term algebra modulo the (congruence) relation.   
Currently there are no facilities to solve conditional equations.
\index{axioms}

The {\em model} part describes the association between 
abstract specifications (like rings) and 
concrete specifications (like integers). 
The semantics is the interpretation of the (abstract) function 
in the model. Operations in models can be compiled functions, 
user defined imperative functions or term rewrite rules. 
The function overloading capabilities are realized by this concept.
Dynamic abstract objects like finite fields can be handled 
by a descriptor concept.
\index{model}

{\em Evaluation} of functional terms is as follows: 
If there is a model in which the function has an interpretation
and a condition on the parameters is fulfilled,
then the interpretation of the function in this model is applied 
to the interpretation (values) of the arguments.   
If there is an imperative procedure, then the procedure body 
is evaluated in the procedure context.
If the unification with the left hand side of a rewrite rule 
is possible and the associated condition evaluates to true, then 
the right hand side of the rewrite rule is evaluated.  
Otherwise the functional term is left unchanged.
\index{evaluation}

In contrast to functional programming languages 
(like SML \cite{Appel 88}) which implement \index{SML}
typed lambda calculus the types of 
operations are not deduced from the program text 
but must be explicitly defined in the specification 
of an operation, in a variable declaration 
or in a typed string expression.
\index{lambda calculus}

A weak point in the current MAS design is that the language 
is only interpreted. This is actualy not a handicap 
in execution speed since compiled libraries can be used, 
but in a too weak semantic analysis of the specifications.
This means that certain errors in the specifications are 
only detected during actual evaluation of an expression.    


%---------------------------------------------------
\section{Syntax}

To precisely define the syntax we first 
specify the syntactic domains and then 
give the EBNF definition of the language.
Note that we use the terms `function' and `procedure'
interchangeably throughout the rest of the 
text.
 
\subsection{Syntax Diagram}

The syntax\index{syntax} definition is given in extended 
BNF\index{EBNF} notation. That means
\verb/name/ denotes non--termial symbols,
\verb/{}/ denotes (possibly empty) sequences,
\verb/()/ denotes required entities,
\verb/|/ denotes case selection and
\verb/[]/ denotes optional cases. 
Terminal symbols are enclosed in double quotes
and productions are denoted by \verb/=/. 
The syntax diagramms are listed in 
table \ref{tabSyC}. % and \ref{tabSyC2}.

\begin{table}[thbp]
\small
\begin{center}
\begin{verbatim}
      program      = topblock "."
      topblock     = { ( unitspec | var | proc | expose ) ";" }
                     statement
      block        = { ( var | proc ) ";" } statement
      unitspec     = { spec | implement | model | axioms }
      spec         = "SPECIFICATION" header ";" 
                      { ( sort | import | sig ) ";" } "END" ident
      implement    = "IMPLEMENTATION" header ";" 
                      { ( sort | import | var | proc ) ";" } 
                      statement "END" ident
      model        = "MODEL" header ";" 
                      { ( sort | import | map ) ";" } "END" ident
      axioms       = "AXIOMS" header ";" 
                      { ( sort | import | rule ) ";" }  "END" ident
      sort         = "SORT" identlist   
      import       = "IMPORT" header [ renamings ]   
      sig          = "SIGNATURE" ident [ "(" [identlist] ")" ] 
                                       [ ":" "(" [identlist]")" ] 
      var          = "VAR" identlist  ":" typeexpr  
      proc         = "PROCEDURE" ident ["("[identlist ]")"]
                                 [":" ident]";" block ident 
      map          = "MAP" header "->" header [ "WHEN" header ]
      rule         = "RULE" expression "=>" expression 
                            [ "WHEN" condition ]
      typeexpr     = header [ string ]
      header       = ident [ "(" [identlist] ")" ]
      renamings    = "[" { ident "/" ident ";" } "]"
      expose       = "EXPOSE" ident [ "(" [actualparms] ")" ]
\end{verbatim}
\end{center}
\caption{Specification Syntax Diagram}
\label{tabSyC}\index{specification syntax}\index{syntax diagram}
\end{table}

Observe that a program is a (possibly empty) sequence of 
declarations, followed by a (possibly empty) statement
followed by a period.
\index{program}
A statement can be an assignment, a procedure call or
a IF--, WHILE--, REPEAT--, BEGIN--statement or
EXPOSE--statement.
Declarations are VAR and PROCEDURE; 
Unit specifications are 
SPECIFICATION, IMPLEMENTATION, MODEL, AXIOMS, 
IMPORT, SORT, SIGNATURE, MAP and RULE.
The syntax of statements and expressions
has already been discussed in chapter \ref{lang.chap}.
Context conditions have also been discussed there.


%---------------------------------------------------
\section{Unit Declarations}

A collection of denotations which belong to the 
same algebraic structure is called a {\bf unit}.
A unit consists of at most one 
SPECIFICATION construct which defines the 
(algebraic) language of the structure.
Optionally several constructs may accompany a specification 
which define the semantics of the algebraic object: 
IMPLEMENTATION, MODEL and AXIOMS.
\index{unit}

The pair SPECIFICATION, IMPLEMENTATION is similar to the pair 
DEFINITION MODULE, IMPLEMENTATION MODULE in Modula--2. 
The semantics for functions is fixpoint semantics of 
$\lambda$--terms which are given by (imperative) 
procedures contained in the IMPLEMENTATION construct.

The pair SPECIFICATION, AXIOMS 
is similar to constructs from algebraic specification 
languages. The semantics of functions is given by 
a term model modulo a congruence relation defined by 
the rewrite rules defined in the \verb/AXIOMS/ construct.

The pair SPECIFICATION, MODEL is as far as I know unique to MAS. 
The semantics of functions is given by mappings 
which associate an interpretation function according to
certain types of arguments.  

When all constituents of an unit have been defined, 
the unit must be exposed (with the EXPOSE construct) 
to make the functions available for use in expressions.

We turn now to a more detailed discussion 
of these constructs.


%---------------------------------------------------
\section{Specifications}

The specification part defines the 
(algebraic) language of an algebraic structure.
\index{specification}

The syntax of the SPECIFICATION declaration is:
\begin{verbatim}
     spec = "SPECIFICATION" header ";" 
            { ( sort | import | sig ) ";" } "END" ident1
   header = ident1 [ "(" [identlist] ")" ]
\end{verbatim}
The identifier \verb/ident1/ defines the name 
of the specification and of the unit.
The specifications can be parametrized 
with formal parameters given by \verb/identlist/.  
The semantics is $\lambda$--abstraction
of a specification. 
\index{header}

\subsection{SORT Declaration}

The syntax of the SORT declaration is:
\begin{verbatim}
      sort = "SORT" identlist   
\end{verbatim}
The \verb/SORT/ declaration reserves the names 
in \verb/identlist/ for use as sorts.\index{SORT}

\subsection{IMPORT Declaration}

The syntax of the IMPORT declaration is:
\begin{verbatim}
      import = "IMPORT" header [ renamings ]   
   renamings = "[" { ident "/" ident ";" } "]"
\end{verbatim}
The \verb/IMPORT/ declaration 
includes an already defined specification, 
named by the identifier in the \verb/header/,
into the actual specification. 
Since several specifications can be imported 
it is possible to join specifications.\index{IMPORT}
\index{join specifications}

The actual specification is therefore extended 
by the (old) specification. 
During import it is possible to rename functions 
and sorts in the imported specification.
The \verb/ident/ after the `\verb./.' must be 
defined in the imported specification and  
is given the new name before the `\verb./.'.

\subsection{SIGNATURE Declaration}

The syntax of the SIGNATURE declaration is:
\begin{verbatim}
      sig = "SIGNATURE" ident [ "(" [identlist] ")" ] 
                              [ ":" "(" [identlist]")" ] 
\end{verbatim}
\index{SIGNATURE}
The \verb/SIGNATURE/ declaration defines 
new function names (\verb/ident/).
Together with the 
input and output parameter sorts named 
by the identifieres in \verb/identlist/. 

\subsection{Example Specification}

These constructs allow both the specification of 
abstract objects (rings, fields),
concrete objects (integers, rational numbers) and 
concrete objects in terms of abstract objects 
(integers as a model of rings). 

The specification of a concrete item like the 
rational numbers could be as follows: 
\begin{verbatim}
        SPECIFICATION RATIONAL;
        (*Rational numbers specification. *)
        (*1*) SORT RAT, INT, atom;
        (*2*) SIGNATURE RNWRITE (RAT)     ;
              SIGNATURE RNDRD   (RAT)     : RAT;
        (*3*) SIGNATURE RNone   ()        : RAT;
              SIGNATURE RNzero  ()        : RAT;
        (*4*) SIGNATURE RNPROD  (RAT,RAT) : RAT;
              SIGNATURE RNSUM   (RAT,RAT) : RAT;
              SIGNATURE RNDIF   (RAT,RAT) : RAT;
              SIGNATURE RNNEG   (RAT)     : RAT;
              SIGNATURE RNINV   (RAT)     : RAT;
              SIGNATURE RNQ     (RAT,RAT) : RAT;
        (*5*) SIGNATURE RNINT   (INT)     : RAT;
              SIGNATURE RNprec  (atom)    ;
        (*9*) END RATIONAL.
\end{verbatim}
In this specification the sorts \verb/RAT/, 
\verb/INT/ and \verb/atom/ are defined. 
Then the input and output parameter sorts of various 
functions are defined. 
\index{field}\index{rational number}

The most general unit is an object which 
specifies the communication (input / output) 
operations of objects. 
\begin{verbatim}
        SPECIFICATION OBJECT;
        (*Object specification. *)
        (*1*) SORT obj;
        (*2*) SIGNATURE READ     (obj) : obj;
              SIGNATURE WRITE    (obj) ;
        (*3*) SIGNATURE DECREAD  (obj) : obj;
              SIGNATURE DECWRITE (obj) ;
        (*4*) SIGNATURE DEFAULT  (obj) : obj;
              SIGNATURE COERCE   (obj) : obj;
        (*9*) END OBJECT.
\end{verbatim}
\index{OBJECT}

Abstract specifications can be build from smaller pieces. 
For example (commutative) fields can be defined 
in terms of two abelian groups, which are themselves 
build from abelian monoids (which extend objects).  
\begin{verbatim}
        SPECIFICATION AMONO;
        (*Abelian monoid specification. *)
        (*1*) IMPORT OBJECT[ amono/obj ];
        (*2*) SIGNATURE ZERO (amono)       : amono;
        (*3*) SIGNATURE SUM  (amono,amono) : amono;
        (*9*) END AMONO.

        SPECIFICATION AGROUP;
        (*Abelian group specification. *)
        (*1*) IMPORT AMONO[ ag/amono ];
        (*2*) SIGNATURE DIF  (ag,ag) : ag;
              SIGNATURE NEG  (ag)    : ag;
        (*9*) END AGROUP.
      
        SPECIFICATION FIELD;
        (*Field specification joining two abelian groups. *)
        (*1*) IMPORT AGROUP[ field/ag ];
              IMPORT AGROUP[ field/ag, ONE/ZERO, PROD/SUM, 
                             REZIP/NEG, Q/DIF ];
        (*9*) END FIELD.
\end{verbatim}
The renamings are used to write one abelian group  
`multiplicatively', like \verb/PROD/ for \verb/SUM/.
\index{abelian monoid}
\index{abelian group}
\index{FIELD}

Using the field specification one could derive an
alternative definition of the rational number specification. 
\begin{verbatim}
        SPECIFICATION RATIONAL;
        (*Rational numbers specification using the abstract 
        field specification. *)
        (*1*) SORT INT, atom;
        (*2*) IMPORT FIELD[ RAT/field,
                            RNDRD/READ, RNWRITE/WRITE,
                            RNone/ONE, RNzero/ZERO, 
                            RNSUM/SUM, RNNEG/NEG, RNDIF/DIF,
                            RNPROD/PROD, RNQ/RECIP, RNQ/Q ];
        (*3*) SIGNATURE RNINT  (INT): RAT;
              SIGNATURE RNprec (atom);
        (*9*) END RATIONAL.
\end{verbatim}
Note that some unique functions for rational numbers 
must be specified seperately.
\index{rational number}


%---------------------------------------------------
\section{Implementations}

The {\em implementation} part describes 
(imperative) procedures and data representations.   
\index{implementation}

The syntax of the IMPLEMENTATION declaration is:
\begin{verbatim}
    implement = "IMPLEMENTATION" header ";" 
                 { ( sort | import | var | proc ) ";" } 
                 statement "END" ident1
   header = ident1 [ "(" [identlist] ")" ]
\end{verbatim}
The identifier \verb/ident1/ defines the name 
of the specification and of the unit.
The specifications can be parametrized 
with formal parameters given by \verb/identlist/.  

A statement can be a BEGIN--statement and is executed 
during the exposition of the unit.
The Modula--2 library functions exist a priori and 
can be accessed without further implementation definitions.

An implementation defines a closed environment 
for the contained variable and procedure declarations 
(so called closures).\index{closure}

\subsection{SORT Declaration}

The syntax of the SORT declaration is:
\begin{verbatim}
      sort = "SORT" identlist   
\end{verbatim}
The \verb/SORT/ declaration reserves the names 
in \verb/identlist/ for use as sorts.\index{SORT}

\subsection{IMPORT Declaration}

The syntax of the IMPORT declaration is:
\begin{verbatim}
      import = "IMPORT" header [ renamings ]   
   renamings = "[" { ident "/" ident ";" } "]"
\end{verbatim}
The \verb/IMPORT/ declaration 
makes the sorts and operations of a specification 
locally available. Its semantics correspond to the 
\verb/EXPOSE/ statement.\index{EXPOSE}\index{IMPORT}

\subsection{VAR Declaration}

The syntax of the VAR declaration is the same as already 
discussed in chapter \ref{lang.chap}:
\begin{verbatim}
      var          = "VAR" identlist  ":" typeexpr  
      typeexpr     = header [ string ]
\end{verbatim}
The \verb/VAR/ declaration reserves names for 
local variables and associates type information with them. 
\index{VAR}

\subsection{PROCEDURE Declaration}

The syntax of the PROCEDURE declaration is the same as 
already discussed in chapter \ref{lang.chap}:
\begin{verbatim}
      proc         = "PROCEDURE" ident ["("[identlist ]")"]
                                 [":" ident]";" block ident 
      block        = { ( var | proc ) ";" } statement
\end{verbatim}
The \verb/PROCEDURE/ declaration defines the 
imperative (or functional) implementation of a procedure.
\index{PROCEDURE}
A \verb/block/ can contain further declarations and 
a statement. 

\subsection{Example Implementation}

The implementations can be used to define 
concrete procedures, abstract procedures or 
as extension to some existing library functions. 
The imperative language constructs (like assignments and loops) 
are fairly standard and are not discussed here.

In case of the rational number unit just 
some gaps left by the library functions need to be filled. 
\begin{verbatim}
        IMPLEMENTATION RATIONAL;
              VAR s: atom;
        (*1*) PROCEDURE RNone();
              BEGIN RETURN(RNINT(1)) END RNone;
        (*2*) PROCEDURE RNzero();
              BEGIN RETURN(RNINT(0)) END RNzero;
        (*3*) PROCEDURE RNWRITE(a);
              BEGIN IF s < 0 THEN RNWRIT(a) ELSE RNDWR(a,s) END; 
                    END RNWRITE;
        (*4*) PROCEDURE RNprec(a);
              BEGIN s:=a END RNprec;
        (*8*) BEGIN 
                    s:=-1; 
        (*9*) END RATIONAL.
\end{verbatim}
Here \verb/RNWRITE/ is defined for convenience 
and internally switches between the two 
rational number write functions \verb/RNWRIT/ and \verb/RNDWR/
according to the local precision variable \verb/s/. 
\index{rational number}

Abstract functions are those which use function names of 
abstract specifications to implement something. 
For example in an ring one could have an abstract 
exponentiation function \verb/EXP/.
\begin{verbatim}
        IMPLEMENTATION RING;
        (*1*) PROCEDURE EXP(X,n);
              VAR   x: ring; VAR   i: atom;
              BEGIN 
              (*1*) IF n <= 0 THEN x:=ONE(X); RETURN(x) END;
              (*3*) i:=n; x:=X; 
                    WHILE i > 1 DO i:=i-1; 
                          x:=PROD(x,X) END;
                    RETURN(x)
              (*9*) END EXP;
        (*9*) END RING.
\end{verbatim}
Here \verb/ONE/ and \verb/PROD/ denote (abstract) functions 
from the ring.
The operators \verb/<=/, \verb/>/ and \verb/-/ are 
used on atoms (integers $k$ in the range 
$-2^{29} = \beta < k < \beta = 2^{29}$).  
\index{EXP}


%---------------------------------------------------
\section{Models}

The {\em model} part describes the association between 
abstract specifications (like rings) and 
concrete specifications (like integers).\index{model}

The syntax of the IMPLEMENTATION declaration is:
\begin{verbatim}
    model = "MODEL" header ";" 
             { ( sort | import | map ) ";" } "END" ident1
   header = ident1 [ "(" [identlist] ")" ]
\end{verbatim}
The identifier \verb/ident1/ defines the name 
of the specification and of the unit.
The specifications can be parametrized 
with formal parameters given by \verb/identlist/.  

Operations / functions in models can be compiled functions, 
user defined imperative functions or term rewrite rules. 
Dynamic abstract objects like finite fields can be handled 
by a descriptor concept. The descriptor can then specify 
the characteristic of the field.\index{descriptor}

\subsection{SORT Declaration}

The syntax of the SORT declaration is:
\begin{verbatim}
      sort = "SORT" identlist   
\end{verbatim}
The \verb/SORT/ declaration reserves the names 
in \verb/identlist/ for use as sorts.\index{SORT}

\subsection{IMPORT Declaration}

The syntax of the IMPORT declaration is:
\begin{verbatim}
      import = "IMPORT" header [ renamings ]   
   renamings = "[" { ident "/" ident ";" } "]"
\end{verbatim}
The \verb/IMPORT/ declaration 
makes the sorts and operations of a specification 
locally available. Its semantics correspond to the 
\verb/EXPOSE/ statement.\index{EXPOSE}\index{IMPORT}

\subsection{MAP Declaration}

The syntax of the MAP declaration is:
\begin{verbatim}
     map = "MAP" header1 "->" header2 [ "WHEN" header3 ]
\end{verbatim}
The \verb/MAP/ declaration defines the 
interpretation of an abstract operation 
(named by the identifier in \verb/header1/)
In the parameter list of an abstract function 
the sort names of a model are specified.

In the parameter list of a concrete function 
(named by the identifier in \verb/header2/)
the two selectors \verb/VAL/ and \verb/DESC/ can appear.
The i--th \verb/VAL/ selects the value of the 
i--th abstract function parameter. 
The i--th \verb/DESC/ selects the descriptor of the 
i--th abstract function parameter. 
Descriptors are only sketched in the sequel.
\index{VAL}\index{MAP}\index{DESC}

Conditional interpretation can be expressed by 
a \verb/WHEN/ clause following the real function.
\verb/header3/ defines the name and parameters of a 
LISP condition.
In the condition the \verb/VAL/ and \verb/DESC/ selectors 
can be used.\index{WHEN}

Observe that the model interpretation can 
be viewed as function overloading. 
The abstract functions are sometimes also called 
generic functions.
\index{overload}\index{function overload}
\index{generic function}

\subsection{Example Model}

On the left hand side in a \verb/MAP/ clause appears the 
abstract function name with sort names as parameters.
On the right hand side after the `\verb/->/' stands the 
concrete function name with \verb/VAL/ and \verb/DESC/ 
selector parameters. 
\begin{verbatim}
        MODEL FIELD;
        (*Rational numbers are a model for fields. *)
        (*1*) IMPORT RATIONAL;
        (*2*) MAP READ(RAT)      -> RNDRD(); 
              MAP WRITE(RAT)     -> RNWRITE(VAL);
        (*3*) MAP ONE(RAT)       -> RNone();
              MAP ZERO(RAT)      -> RNzero();
        (*4*) MAP PROD(RAT,RAT)  -> RNPROD(VAL,VAL);
              MAP SUM(RAT,RAT)   -> RNSUM(VAL,VAL);
              MAP DIF(RAT,RAT)   -> RNDIF(VAL,VAL);
              MAP NEG(RAT)       -> RNNEG(VAL);
              MAP Q(RAT,RAT)     -> RNQ(VAL,VAL);
              MAP REZIP(RAT)     -> RNINV(VAL);
        (*9*) END FIELD.
\end{verbatim}
This reads as follows:
the product function \verb/PROD/ is 
interpreted in the model of rational numbers 
(two rational numbers as parameters \verb/RAT/)  
as the concrete function \verb/RNPROD/ 
(from the abstract parameters the values are to be taken 
according to the \verb/VAL/ selectors).
\index{field}\index{rational number}

An example using descriptors and conditional interpretation 
is as follows.
\begin{verbatim}
      MODEL FIELD;
      (*Modular integers are a model for fields. *)
            ...
      (*4*) MAP PROD(MI,MI)   -> MIPROD(DESC,VAL,VAL) 
                            WHEN EQ(DESC,DESC);
            ...
      (*9*) END FIELD.
\end{verbatim}
\verb/MI/ denotes the modular integer ${\bf Z}/_{(p)}$ sort. 
\verb/MIPROD/ denotes the modular integer product where the 
first parameter is the modulus $p$ selected by \verb/DESC/. 
The \verb/WHEN/ clause specifies that 
only numbers from the same finite field are to be multiplied
(that is their descriptors must be equal (\verb/EQ/)).  
Descriptors can be specified in \verb/VAR/ declarations 
provided the specifications have defined them.
\index{modular integers}


%---------------------------------------------------
\section{Axioms}

The {\em axioms} part describes conditional rewrite rules. 
\index{axioms}

The syntax of the AXIOM declaration is:
\begin{verbatim}
   axioms = "AXIOMS" header ";" 
            { ( sort | import | rule ) ";" }  "END" ident1
   header = ident1 [ "(" [identlist] ")" ]
\end{verbatim}
The identifier \verb/ident1/ defines the name 
of the specification and of the unit.
The specifications can be parametrized 
with formal parameters given by \verb/identlist/.  

\subsection{SORT Declaration}

The syntax of the SORT declaration is:
\begin{verbatim}
      sort = "SORT" identlist   
\end{verbatim}
The \verb/SORT/ declaration reserves the names 
in \verb/identlist/ for use as sorts.\index{SORT}

\subsection{IMPORT Declaration}

The syntax of the IMPORT declaration is:
\begin{verbatim}
      import = "IMPORT" header [ renamings ]   
   renamings = "[" { ident "/" ident ";" } "]"
\end{verbatim}
The \verb/IMPORT/ declaration 
makes the sorts and operations of a specification 
locally available. Its semantics correspond to the 
\verb/EXPOSE/ statement.\index{EXPOSE}\index{IMPORT}

\subsection{RULE Declaration}

The syntax of the MAP declaration is:
\begin{verbatim}
      rule = "RULE" expression1 "=>" expression2 
              [ "WHEN" condition ]
\end{verbatim}

The \verb/RULE/ declaration defines a rewrite rule.
The meaning is as follows:
if the left hand side of a rule (\verb/expression1/ above)
can be unified with the expression under consideration, 
then the variables in the right hand side 
(\verb/expression2/ above)
are substituted according to the unification. 
Then the right hand side replaces the actual expression.

The rules define a reduction relation on the term algebra 
generated by the sorts and operations of the specification. 
\index{term algebra}\index{RULE}\index{term rewriting}
\index{unification}\index{substitution}

Variables need not be declared and are assumed 
to be universally quantified and unbound.\index{variable}

Conditional rewriting can be expressed by 
a \verb/WHEN/ clause following the right hand side of the  
rewrite rule (\verb/condition/ above).
The condition is evaluated with the variables 
substituted according to the actual unification of 
the left hand side. 
\index{conditional rewriting}\index{WHEN}

Currently there are no facilities to solve conditional 
equations since there is no back tracking of unsuccessful
rewritings.\index{back track}

There are also no provisions to check if the 
rewrite system is confluent or Noetherian.
\index{confluence}\index{Noetherian relation}

\subsection{Example Axioms}

The Peano structure can be specified as follows:
\begin{verbatim}
        SPECIFICATION PEANO;
        (*Peano structure specification. *)
        (*1*) SORT nat, bool;
        (*2*) SIGNATURE null  ()        : nat;
              SIGNATURE one   ()        : nat;
           (* SIGNATURE succ  (nat)     : nat; *)
              SIGNATURE add   (nat,nat) : nat;
              SIGNATURE prod  (nat,nat) : nat;
        (*3*) SIGNATURE equal (nat,nat) : bool;
        (*9*) END PEANO.
\end{verbatim}
Observe that the \verb/succ/ (successor) constructor 
need not be defined in the specification, since 
no rule has \verb/succ/ on the first functional term 
in the right hand side expression. 
\index{Peano structure}
The Peano axioms can then be coded as rewrite rules
as follows:
\begin{verbatim}
        AXIOMS PEANO;
        (*Axioms for Peano system. *)
              IMPORT PROPLOG;
              RULE one()                  => succ(null());
        (*1*) RULE equal(X,X)             => TRUE();
              RULE equal(succ(X),null())  => FALSE();
              RULE equal(null(),succ(X))  => FALSE();
        (*2*) RULE equal(succ(X),succ(Y)) => equal(X,Y);
        (*3*) RULE add(X,null())          => X;
              RULE add(null(),X)          => X;
        (*4*) RULE add(X,succ(Y))         => succ(add(X,Y));
        (*5*) RULE prod(X,null())         => null();
              RULE prod(null(),X)         => null();
        (*6*) RULE prod(X,succ(Y))        => add(prod(X,Y),X);
        (*9*) END PEANO.
\end{verbatim}
\verb/PROPLOG/ denotes a propositional logic specification 
not listed here. 
There the constant functions 
\verb/TRUE()/ and \verb/FALSE()/ are defined.
During unification the variables \verb/X/ and \verb/Y/ 
are bound in the left hand side and then substituted in the 
right hand side.
\index{Peano axioms}


\section{EXPOSE Statement}

Once this specification aparatus has been setup one 
wants to see how it works and what benefits are obtained.
\index{evaluation}
The language constructs discussed so far 
modify only the decalaration data base. 
To access the defined functions they must first be exposed,  
that means they must be made visible.  

The syntax of the EXPOSE statement is:
\begin{verbatim}
   expose = "EXPOSE" ident [ "(" [actualparms] ")" ]
\end{verbatim}
The identifier \verb/ident/ defines the name 
of the unit.
The actual parameters are given by \verb/actualparms/ 
and can be any MAS expression which evaluate 
to an item meaningful in the unit.

During the exposition of an implementation part 
the actual environment is used to define the 
procedure closures. This implies that the order of 
the exposition is important. 
So only models which have already been exposed are 
visible in an abstract implementation.

For example the earlier defined units can be exposed 
as follows:
\begin{verbatim}
        EXPOSE RATIONAL.
        EXPOSE PEANO.
        EXPOSE FIELD. 
\end{verbatim}
From then on the functions like \verb/PROD/ can be 
used in expressions or top level statements and procedures.
\index{EXPOSE}


\section{Operator Overloading}

For convenience of the users the MAS parser can be 
instructed to generate generic function names for the 
arithmetic operators. However some care is needed 
since then also a specification of the atoms structure 
is required to access the built--in primitive arithmetic. 
\index{generic parse}\index{parser}
\index{operator overloading}

This feature of the parser is set by the pragma switch 
\verb/GENPARSE/. It activates / inactivates 
the generic code generation of the parser.
The operators correspond to the following functions:
\verb/+/ to \verb/SUM/, 
\verb/-/ to \verb/DIF/ or \verb/NEG/, 
\verb/*/ to \verb/PROD/, \verb./. to \verb/Q/
and \verb/^/ to \verb/EXP/.
See also the section on PRAGMAS \ref{prag.sec}.
\index{PRAGMA}
\index{\verb/+/}\index{\verb/-/}\index{\verb/*/}
\index{\verb./.}\index{\verb/^/}


\section{Expression Evaluation}

We turn now to the evaluation of arbitrary expressions.
Expressions are transformed to functional terms by the parser. 
The evaluation of functional terms is defined as follows:
\begin{enumerate}
\item If there is a model in which the function has an interpretation
      and the WHEN--condition on the parameters is fulfilled,
      then the interpretation of the function in this model is 
      applied to the interpretation (values) of the arguments.   
      \index{interpretation}
\item If there is an imperative procedure, then the procedure body 
      is evaluated in the procedure context.\index{procedure}
\item If the unification with the left hand side of a rewrite rule 
      is possible and the associated condition evaluates to true, 
      then the right hand side of the rewrite rule is evaluated.
      \index{unification}\index{rewrite rule}
\item Otherwise the functional term is left unchanged.
\end{enumerate}
\index{evaluation}

Let us step through the following examples:
\begin{verbatim}
        VAR r, s: RAT.             ANS: RAT().

        r:="2222222222.777777777777777".
        ANS: "2222222222777777777777777/1000000000000000".

        s:=r/r.                    ANS: "1".

        s:=r^0 + s - "1": RAT.     ANS: "1".
\end{verbatim}
The first line declares the variables \verb/r/ and \verb/s/ 
to be of type \verb/RAT/, that is to be rational numbers. 
The second line is a so called generic assignment. 
Depending on the type of \verb/r/ the character string on the
right hand side is read (or converted to internal form). 
Recall that the interpretation of \verb/READ(RAT)/ 
was defined as \verb/RNDRD()/ which reads a rational number 
in decimal representation. 

Internally an object with type, value and descriptor information 
is created. This information is then used by the 
generic write function \verb/WRITE(RAT)/ for displaying 
the result in the next line.

The fourth line shows the computation of \verb.r/r.. 
According to the type information of \verb/r/ the 
corresponding generic function \verb/Q(RAT,RAT)/ is determined. 
Then \verb/RNQ(VAL,VAL)/ is computed where the 
values of the data objects are substituted. 
Finally the information on the output parameters of 
\verb/RNQ/ namely \verb/RAT/ is used to create 
a new typed object. This object is then bound to 
the variable \verb/s/ and finally it is displayed.

The last line shows the computation of a more 
complex expression \verb/r^0 + s - "1": RAT/.
The term \verb/"1": RAT/ denotes a constant from 
the rational numbers, namely \verb/1/. The contents of the 
character string are read by the generic function 
\verb/READ(RAT)/ and a new typed object is created. 
Note further that \verb/r^0/ is computed by an abstract function 
(namely \verb/EXP/) of the abstract \verb/RING/ implementation.
Then the computation proceeds as expected.

A final example for the use of term algebras which 
explains itself:
\begin{verbatim}
        x:=one().          ANS: succ(null()).
        x:=add(x,x).       ANS: succ(succ(null())).
        x:=prod(x,x).      ANS: succ(succ(succ(succ(null())))).
\end{verbatim}
\index{Peano arithmetic}

This concludes the discussion of the 
language constructs used in the specification component.
