                  
\newfont{\bfsl}{cmbxsl10 scaled 1000}

\def\ISA{IS-A\ }
\def\IsA{IS-A\ }
\def\WHERE{WHERE\ }
\def\IS{IS\ }
\def\COUNT{Count}
\def\SetOf{SetOf\ }
\def\ANYTHING{Anything}
\def\EACH{{\bfsl each}\ }
\def\OF{{\bfsl of}\ }
\def\IN{{\bfsl in}\ }
\def\IsIn{\ {\bfsl isIn}\ }
\def\SubSetOf{{\bfsl subsetOf}\ }
\def\THIS{{\bfsl this}}
\def\ALL{ {\bfsl all}\ }
\def\AND{ {\bfsl and}\ }
\def\NOT{{\bfsl not}\ }
\def\OR{{\bfsl or}\ }
\def\ADDED{{\bfsl Added}\ }
\def\REMOVED{{\bfsl Removed}\ }
\def\NEW{{\bfsl New}}

           
\def\fig#1#2{

{ \centerline{{\bf Fig. #1:} #2} }}

The language of abstract machines has the following syntax, 
whereby keywords in brackets are optional.
{\sl\begin{tabbing}
xxxxxxxxxxxxxxxxxxxxxxx\=xxxx\=xxxxxxxxxxxxxxxxxxxxxxxxxxxxx\kill
$<$abstract machine$>$\>=\> Abstract Machine $<$machine name$>$\\
\>\> BASIC SETS $<$basicset-list$>$;\\
\>\> [CONTEXT $<$context-specification$>$];\\   
\>\> VARIABLES $<$variable-list$>$;\\
\>\> INVARIANT $<$predicate-list$>$;\\
\>\> [DEFINITIONS $<$definition-list$>$];\\
\>\> INITIALIZATION $<$init-operation-list$>$;\\
\>\> OPERATIONS $<$operation-list$>$;\\
\>\> END $<$machine-name$>$\\
  
\\


$<$basicset-list$>$ 	\>=\>	$<$basicset-name$>$ $\mid$\\ 
\>\>$<$basicset-name$>$ , $<$basicset-list$>$ \\
\\

$<$context-specification$>$  \>=\>	
$<$type-specifications$>$ $\mid$\\
\>\>$<$constant-specifications$>$\\

$<$type-specifications$>$    \>	= \>	$<$type-specification$>$ $\mid$ \\
\>\>$<$type-specification$>$ $<$type-specifications$>$ \\
\\
$<$type-specification$>$     \>	= \>	$<$renamed-type$>$ $\mid$\\
\>\>$<$enumerated-type$>$ $\mid$\\
\>\>$<$subrange-type$>$ \\
\\
$<$renamed-type$>$    \> = \>	$<$type-name$>$ "=" $<$existing-type-name$>$\\
\\
$<$enumerated-type$>$ \> = \>	$<$type-name$>$ "="  "\{" $<$ident-list$>$
"\}"\\
\\
$<$ident-list$>$      \> = \>	$<$identifier$>$ $\mid$ \\
\>\>$<$identifier$>$  , $<$ident-list$>$ \\
\\
$<$subrange-type$>$ \> = \>	$<$type-name$>$ "="  "[" $<$const-expression$>$
 .. $<$const-expression$>$ "]" \\
\\
$<$constant-specifications$>$ \> = \> $<$constant-name$>$ ":"
$<$type-expression$>$ \\
\\
$<$variable-list$>$ 	\>=\>	$<$variable-name$>$ $\mid$\\ 
\>\>$<$variable-name$>$ , $<$variable-list$>$ \\
\\

$<$predicate-list$>$	\>=\>	$<$predicate$>$ $\mid$\\ 
\>\>$<$predicate$>$ , $<$predicate-list$>$\\
\\

$<$definition-list$>$	\>=\>	$<$definition$>$ $\mid$\\ 
\>\>$<$definition$>$ , $<$definition-list$>$\\
\\

$<$definition $>$	\>=\>	$<$variable-name$>$ "=" $<$expression$>$\\
\\

$<$init-operation-list$>$	\>=\>	$<$init-operation$>$ $\mid$\\ 
\>\>$<$init-operation$>$ , $<$init-operation-list$>$\\
\\

$<$init-operation$>$	\>=\>	$<$variable-name$>$ ":=" $<$expression$>$\\
\\

$<$operation-list$>$ 	\>=\>	$<$operation$>$ $\mid$\\ 
\>\>$<$operation$>$ ; $<$operation-list$>$ \\
\\
$<$operation$>$	\>=\>	[ $<$output-parameters$>$ "$\longleftarrow$" ]\\
\>\>$<$operation-name$>$ [ "(" $<$input-parameters$>$ ")" ]\\
\>\>$<$operation-specification$>$\\
\\

$<$output-parameters$>$	\>=\>	$<$parameter-name$>$ $\mid$\\ 
\>\>$<$parameter-name$>$ , $<$output-parameters$>$\\
\\
$<$input-parameters$>$	\>=\>	$<$parameter-name$>$ $\mid$\\ 
\>\>$<$parameter-name$>$ , $<$input-parameters$>$\\
\\
$<$operation-specification$>$   \>=\>	skip $\mid$\\ 
\>\>x1 := E1 $\mid$$\mid$ .. $\mid$$\mid$ xn := En $\mid$\\ 
\>\>PRE  $<$predicate$>$  BEGIN $<$operation-specification$>$ END $\mid$\\ 
\>\>IF $<$predicate$>$  THEN $<$operation-specification$>$ $\mid$\\ 
\>\>IF $<$predicate$>$  THEN $<$operation-specification$>$ \\
\>\>ELSE $<$operation-specification$>$ $\mid$\\ 
\>\>ANY z IN $<$predicate$>$ THEN $<$operation-specification$>$\\ 
\>\>WHILE $<$predicate$>$ DO $<$operation-specification$>$ END\\
\>\>$<$operation-specification$>$ ; $<$operation-specification$>$\\   

\\
$<$variable-name$>$ \> = \> $<$string$>$ \\
$<$operation-name$>$ \> = \> $<$string$>$ \\
$<$inputparameter-name$>$ \> = \> $<$string$>$ \\
$<$outputparameter-name$>$ \> = \> $<$string$>$ \\
$<$basicset-name$>$ \> = \> $<$String$>$ \\
$<$type-name$>$ \> = \> $<$String$>$ \\ 
$<$constant-name$>$ \> = \> $<$String$>$ \\ 
\end{tabbing}}     
*** definition of predicate and expression is missing ***


We have the following additional constraints:
\begin{itemize}
\item For each variable listed within the variable clause a membership or
subsetrelationship to a basic set should be deducable out of the definitions
within the invariant. (This conditions results often in a membership predicate
for each variable but must not).
\item In the initialisation clause for each variable listed within the variable
clause an initialising substitution has to be defined.
\item Variables defined in the definition paragraph as well as constants
introduced within the context are not allowed to be
substituted within an operation.
\item Names of operations are not allowed to be referenced within operations of the
same machine (unlike as within USED machines, a possiblity we didn't exploit within
the project).
\item For each used parameter variable within an operation membership
to a
domain has to be defined within the precondition.
\item The operators used in predicate definitions (within invariant or
substitution definitions) are not fixed beforehand. A
user is allowed to introduce new operators (which should have a formal semantic
definit\item Machine names within the IMP clause must exist.   ion within an enhanced CONTEXT).
\end{itemize}

Out of these syntax rules several control categories arise:
\begin{itemize}
\item control of existence\\
Each free variable used within the invariant has to be referenced within the
variables clause.\\
For each variable listed within the variable clause a predicate has to fix
it's membership to a certain basic set (or has to provide enough information
for deriving this property).\\  
For each parameter variable locally defined within an operation a
membership definition has to follow within the precondition of the operation.
\item control of visibility \\
A name clash between locally defined parameter names and globally defined
variable names should be ruled out.\\
The bound variable name within the ANY-substitution should not be identical
to any other global
variable. \\
Variable capture within quantified predicates has to be avoided.\\

\item control of usage\\
Constants and derived variables are not allowed to be substituted.\\
Operations of the same machine are not allowed for use within other operations
of the same machine.
\end{itemize}

