%
%\appendix
%
%\chapter{The Action Semantics of MicroSpecimen}
%\label{microspecimen}
%
%\documentstyle[headerfooter,a4,a4wide,notation]{marticle}
%\newcommand{\version}{24 Sep 1991}
%\pagestyle{headings}
%\pageheaderlinetrue
%\pageheader{\sl\rightmark}{\bf\version}{\thepage}
%\pageheader{\sl\rightmark}{}{\thepage}
%\pagefooter{}{}{}
%
%\title{\huge Action Semantics of MicroSpecimen}
%\author{Hermano Moura
%\thanks{Supported by CNPq, Brazil. On leave from
%    Caixa Econ\^omica Federal, Brazil.}\\
%University of Glasgow\\ 
%Department of Computing Science\\
%Glasgow, G12\ 8QQ, Scotland \\
%{\tt moura@dcs.glasgow.ac.uk}\\ \\
%\date{3rd June 1992}}
%
%\begin{document}
%
%\maketitle
%\begin{abstract}
%\noindent
%This document gives the definition of MicroSpecimen, a simple imperative
%language designed to serve as an example language in our research on 
%semantics-directed compiler generation.
%\end{abstract}
%\tableofcontents
%\newpage
%\input{informal}
%\section*{The Action Semantics of {\it Specimen}}
% *** Contents ***
%\contentsline {section}{\numberline {A}Abstract Syntax}{25}
%\contentsline {subsection}{\numberline {A.1}Programs}{25}
%\contentsline {subsection}{\numberline {A.2}Declarations}{25}
%\contentsline {subsection}{\numberline {A.3}Commands}{25}
%\contentsline {subsection}{\numberline {A.4}Expressions}{25}
%\contentsline {subsection}{\numberline {A.5}Types}{26}
%\contentsline {section}{\numberline {B}Semantic Entities}{26}
%\contentsline {subsection}{\numberline {B.1}Data}{26}
%\contentsline {subsection}{\numberline {B.2}Bindings}{26}
%\contentsline {subsection}{\numberline {B.3}Storage}{26}
%\contentsline {subsection}{\numberline {B.4}Abstractions}{27}
%\contentsline {section}{\numberline {C}Semantic Functions}{27}
%\contentsline {subsection}{\numberline {C.1}Programs}{27}
%\contentsline {subsection}{\numberline {C.2}Declarations}{27}
%\contentsline {subsubsection}{\numberline {C.2.1}Elaborating Declarations}{28}
%\contentsline {subsubsection}{\numberline {C.2.2}Elaborating Formal Parameters}{28}
%\contentsline {subsubsection}{\numberline {C.2.3}Elaborating Formal Parameter Lists}{28}
%\contentsline {subsection}{\numberline {C.3}Commands}{29}
%\contentsline {subsection}{\numberline {C.4}Expressions}{29}
%\contentsline {subsubsection}{\numberline {C.4.1}Evaluating Expressions}{30}
%\contentsline {subsubsection}{\numberline {C.4.2}Evaluating Arguments}{30}
%\contentsline {subsubsection}{\numberline {C.4.3}Evaluating Operators}{30}
%\contentsline {section}{\numberline {D}Lexical Syntax}{31}
%\contentsline {subsection}{\numberline {D.1}Identifiers}{31}
%\contentsline {subsection}{\numberline {D.2}Numerals}{31}

\section{Abstract Syntax}

\begin{spec}
\item[\needs] \ide{Lexical Syntax} .
\item[\closed]
\item[\grammar]
%\item[\protects] \ide{Abstract Syntax} . %\ \ \except \ide{Literals} .
\end{spec}

\subsection{Programs}

\begin{spec}
%\item[\needs] \ide{Declarations} , \ide{Commands} .
%\item[\grammar]
\item Program = \[ ``{\tt program}'' Identifier ``{\tt is}'' Declaration ``{\tt in}'' Command ``{\tt end}'' \] .
\end{spec}

\subsection{Declarations}

\begin{spec}
%\settowidth{\wordlength}{ArrayComps}
%\tabset \makebox[\wordlength][r]{ArrayComps} &=&
\tabset {Declaration} &=&
%\item[\needs] \ide{Commands} , \ide{Expressions} , \ide{Types} .
%\item[\grammar]
%\item \tab \makebox[\wordlength][r]{Declaration} &=& 
\item \tab Declaration &=& \[ ``{\tt const}'' Identifier ``{\tt :}'' PrimitiveType ``{\tt =}'' Expression \] \| \=
	\[ ``\verb%var%'' Identifier ``\verb%:%'' PrimitiveType ``\verb%:=%'' Expression \] \| \=
	\[ ``\verb%varray%'' Identifier ``\verb%:%'' ArrayType ``\verb%:=%'' ``{\tt [}'' ArrayComps ``{\tt ]}'' \] \| \=
	\[ ``\verb%proc%'' Identifier ``\verb+(+'' ProcFormals ``{\tt )}'' ``{\tt =}'' Command \] \| \=
	\[ ``\verb+fun+'' Identifier ``\verb+(+'' FunFormals ``{\tt )}'' ``{\tt :}'' ValueType \(``{\tt =}''\\Expression \] \|\)\=
	\tuple{Declaration \tuple{"{\tt ;}" Declaration}\up*} .

%	\[ Declaration ``\verb+;+'' Declaration \] .

%\item \tab \makebox[\wordlength][r]{ArrayComps} &=&
\item ArrayComps = Expression \| \[ Expression ``{\tt ,}'' ArrayComps \] .

%\item \tab \makebox[\wordlength][r]{ProcFormals} &=&
\item ProcFormals = \[ \] \| \[ ProcFormal \] \| \[ ProcFormal ``\verb+,+'' ProcFormals \] .

%\item \tab \makebox[\wordlength][r]{ProcFormal} &=&
\item ProcFormal = \[ Identifier ``\verb+:+'' ValueType \] \| \[ ``{\tt var}'' Identifier ``\verb+:+'' PrimitiveType \] .
%\| \[ \verb'fun' Identifier \verb+:+ Type \] .

%\item \tab \makebox[\wordlength][r]{FunFormals} &=&
\item FunFormals = \[ \] \| \[ FunFormal \] \| \[ FunFormal ``\verb+,+'' FunFormals \] .

%\item \tab \makebox[\wordlength][r]{FunFormal} &=&
\item FunFormal = \[ Identifier ``\verb+:+'' ValueType \] .

\end{spec}
%
\subsection{Commands}

\begin{spec}
%\item[\grammar]
\settowidth{\wordlength}{ProcActuals}
\tabset \makebox[\wordlength][r]{ProcActuals} &=&
\item \tab \makebox[\wordlength][r]{Command} &=&
	\[ Identifier ``\verb%:=%'' Expression \] \| \=
	\[ Identifier ``{\tt [}'' Expression ``{\tt ]}''``\verb%:=%'' Expression \] \| \=
%	\[ ``\verb%if%'' Expression ``\verb%then%'' Command ``\verb%else%'' Command ``{\tt end}'' \] \| \=
	\[ ``\verb%if%'' Expression ``\verb%then%'' Command \tuple{"else" Command}\up? ``{\tt end}'' \] \| \=
	\[ ``\verb%while%'' Expression ``\verb%do%'' Command ``{\tt end}'' \] \| \=
 	\[ ``{\tt call}'' Identifier ``\verb+(+'' ProcActuals ``\verb+)+'' \] \| \=
	\[ ``\verb%local%'' Declaration ``\verb%in%'' Command ``\verb%end%'' \] \| \=
	\tuple{Command \tuple{"{\tt ;}" Command}\up*} .
%	\[ Command \verb%;% Command \] .

\item \tab \makebox[\wordlength][r]{ProcActuals} &=& \[ \] \| \[ ProcActual \] \| \[ ProcActual ``\verb',''' ProcActuals \] .

\item \tab  \makebox[\wordlength][r]{ProcActual} &=& \[ Expression \] \| \[ ``{\tt var}'' Identifier \] .
%\| \[ \verb'fun' Identifier \] .
\end{spec}

\subsection{Expressions}

\begin{spec}
\settowidth{\wordlength}{Expression}
\tabset \makebox[\wordlength][r]{Expression} &=&
%\item[\needs] \ide{Lexical Syntax} .
%\item[\grammar]
\item \tab \makebox[\wordlength][r]{Expression} &=&
	``\verb%true%'' \| \=
	``\verb%false%'' \| \=
	Numeral \| \=
	Identifier \| \=
	\[ Identifier ``\verb+[+'' Expression ``\verb+]+'' \] \| \=
	\[ ``\verb%if%'' Expression ``\verb%then%'' Expression \tuple{``{\tt else}'' Expression}\up? ``{\tt end}'' \] \| \=
	\[ Identifier ``\verb+(+'' FunActuals ``\verb+)+'' \] \| \=
	\[ Expression Operator Expression \] \| \=
	\[ Operator Expression \] \=
        \[ ``\verb%let%'' Declaration ``\verb%in%'' Expression ``\verb%end%'' \] .
%	\[ \verb'(' Expression \verb')' \] .

\item \tab \makebox[\wordlength][r]{FunActuals} &=& \[ \] \| \[ FunActual \] \| \[ FunActual ``\verb',''' FunActuals \] .

\item \tab  \makebox[\wordlength][r]{FunActual} &=& \[ Expression \] .

\item \tab \makebox[\wordlength][r]{Operator} &=&
	``\verb+not+'' \| ``\verb+and+'' \| ``\verb+or+'' \| \= 
	``\verb%~%'' \|``\verb%+%'' \| ``\verb+-+'' \| ``\verb+*+'' \| ``\verb+/+'' \| ``\verb+<+'' \| ``\verb+>+'' \| ``\verb+<=+'' \| ``\verb+>=+'' \| \=
	``\verb+=+'' \| ``\verb+<>+'' .
\end{spec}

\subsection{Type Denoters}

\begin{spec}
\settowidth{\wordlength}{PrimitiveType}
\tabset \makebox[\wordlength][r]{PrimitiveType} &=&
\item \tab \makebox[\wordlength][r]{ValueType}     &=&
	PrimitiveType \| FunctionType .  %\| ``\verb+unit+'' .
\item \tab \makebox[\wordlength][r]{PrimitiveType} &=&
	``\verb+bool+'' \| ``\verb+int+'' .
\item \tab \makebox[\wordlength][r]{FunctionType}  &=&
	\[ ValueType ``{\tt ->}'' ValueType \] \| \=
	\[ ``{\tt (}'' TupleType ``{\tt )}'' ``{\tt ->}'' ValueType \] .
\item \tab \makebox[\wordlength][r]{TupleType} &=&
	\[ \] \| \[ ValueType \] \| \[ ValueType ``{\tt ,}'' TupleType \] .
\item \tab \makebox[\wordlength][r]{ArrayType} &=&
	\[ ``{\tt array}'' ``{\tt [}'' Numeral ``{\tt ]}'' ``{\tt of}'' PrimitiveType \] .
\end{spec}


\section{Semantic Entities}

\begin{spec}
\item[\includes] \ide{Action Notation} .
\end{spec}

\subsection{Values}

\begin{spec}
\item[\introduces] primitive-value , value .
\item primitive-value = truth-value \| integer .
\item value = primitive-value \| function .
\end{spec}

\subsection{Bindings}

\begin{spec}
%\item[\needs] \ide{Data} , \ide{Storage} , \ide{Abstractions} .
\item alpha = lowercase-letter \| uppercase-letter .
\item token = string-of (alpha,(alpha \| digit)*) .
\item bindable = value \| procedure \| cell \| array .
\end{spec}

\subsection{Storage}

\begin{spec}
%\item[\introduces] truth-value-cell , integer-cell .
\item cell = cell [truth-value] \| cell [integer] .
\item storable = primitive-value .
\end{spec}

\subsection{Procedures and Functions}

\begin{spec}
\item[\introduces] \( procedure , proc-argument , proc-argument-list ,\\
		      function , fun-argument , fun-argument-list , fun-result .\)
%\item[\needs] \ide{Data} , \ide{Storage} .
\item 	procedure = abstraction .
\item 	proc-argument = value  \| cell .
\item 	proc-argument-list = list [proc-argument] .
\item 	function = abstraction .
\item 	fun-argument = value .
\item 	fun-argument-list = list [fun-argument] .
\item 	fun-result = value .
\end{spec}

\subsection{Arrays}
\begin{spec}
\item[\introduces] array .
\item	array = list [cell] .
\end{spec}


\section{Semantic Functions}
 
\begin{spec}

\item[\needs] \ide{Abstract Syntax} , \ide{Semantic Entities} .
 
\end{spec}


\subsection{Programs}

\begin{spec}

\item[\introduces] run \_ .

%\item[\needs] \ide{Declarations} , \ide{Commands} .

\item[$\:\bullet$] run \_ :: Program \into action .

\item run \[ ``\verb+program+'' ~I:Identifier ``\verb+is+'' ~D:Declaration ``\verb+in+'' ~C:Command ``\verb+end+'' \] = \=
	\(
	\< elaborate ~D \> \\
	hence \\
	\< execute ~C . \>
	\)
\end{spec}


\subsection{Declarations}

\begin{spec}

\item[\introduces] \( elaborate \_ , elaborate-formals \_ , elaborate-formal \_ ,\\
	           evaluate-array-components \_ . \)

%\item[\needs] \ide{Commands} , \ide{Expressions} , \ide{Types} .

\end{spec}


\subsubsection{Elaborating Declarations}

\begin{spec}

\item[$\:\bullet$]	elaborate \_ :: Declaration \into action .

\item	elaborate \[ ``\verb+const+'' ~I:Identifier ``\verb+:+'' ~T:PrimitiveType ``\verb+=+'' ~E:Expression \] = \=
	evaluate ~E then bind token-of ~I to the primitive-value .

\item	elaborate \[ ``\verb+var+'' ~I:Identifier ``\verb+:+'' ~T:PrimitiveType ``\verb+:=+'' ~E:Expression \] = \=
	\(
	\< \< evaluate ~E then give the primitive-value label \#1 \> \\
	   and \\
	   \< allocate-for-primitive-value ~T then give the cell label \#2 \> 
	\> \\
	then \\
	\< \< bind token-of ~I to the cell\#2 \> \\
	   and \\
	   \< store the primitive-value\#1 in the cell\#2 . \>
        \>
	\)
 
\item	elaborate \[ ``\verb+varray+'' ~I:Identifier ``\verb+:+'' ~T:ArrayType ``\verb+:=+'' ~A:ArrayComps \] = \=
	\(
	\< 
	  \< evaluate-array-components ~A then give the list label \#1 \> \\
	  and \\
	  \< allocate-for-array ~T then give the list label \#2 \>
	\> \\
	then \\
	\< \< unfolding\\
	        \<
	          \< \< check (the list\#1 is empty-list) \> \\
	             and then \\
	             \< complete \>
                  \> \\
	          or \\
	          \< \< check not (the list\#1 is empty-list) \> \\
	             and then \\
	             \< \< store head-of (the list\#1) in head-of (the list\#2) \> \\
			and then\\
			\< \< \< give tail-of (the list\#1) label \#1 \>\\
			      and\\
			      \< give tail-of (the list\#2) label \#2 \>
			   \> \\
			   then\\
			   \< unfold \>
                        \>
                     \>
                  \>
                \>
           \> \\
           and \\
           \< bind token-of ~I to the list\#2 .\> 
        \>
	\)

\item   elaborate \[ ``\verb+proc+'' ~I:Identifier ``{\tt (}'' {\it FS}:ProcFormals ``{\tt )}'' ``\verb+=+'' ~C:Command \] = \=
	\(
	recursively bind token-of ~I to closure abstraction \=
	      \< \< furthermore elaborate-proc-formals {\it FS} \> \\
		 hence \\
		 \< execute ~C . \>
	      \>
	\)

\item   elaborate \[ \(``\verb+fun+'' ~I:Identifier ``{\tt (}'' {\it FS}:FunFormals ``{\tt )}'' ``{\tt :}'' ~T:ValueType ``\verb+=+''\\
				~E:Expression \] =\) \=
	\(
	recursively bind token-of ~I to closure abstraction \=  
	      \< \< furthermore elaborate-fun--formals {\it FS} \> \\
	         hence \\
                 \< evaluate ~E then give the fun-result . \>
	      \>
	\)

\item	elaborate \[ ~D_1:Declaration ``\verb+;+'' ~D_2:Declaration \] = \=
	\(
	\< elaborate ~D_1 \> \\
	before \\
	\< elaborate ~D_2 . \> 
	\)

\end{spec}


\subsubsection{Evaluating Array Components}

\begin{spec}

%\item[\introduces] 	evaluate-array-components \_ .

\item[$\:\bullet$]	evaluate-array-components \_ :: ArrayComps \into action .

\item evaluate-array-components \[ ~E:Expression \] = \=
	evaluate ~E then give list (primitive-value) .

\item evaluate-array-components \[ ~E:Expression {\tt ,} ~A:ArrayComps \] = \=
	\( \< \< evaluate ~E then give list (primitive-value) label \#1 \> \\
              and\\
	      \< evaluate-array-components ~A then give the list label \#2 \>
	   \>\\
	   then\\
           \< give concatenation (the list\#1,the list\#2) .\>
        \)
\end{spec}


\subsubsection{Elaborating Procedure Formal Parameters}

\begin{spec}

%\item[\introduces] 	elaborate-proc-formal \_ .

\item[$\:\bullet$]	elaborate-proc-formals \_ :: ProcFormals \into action .

\item elaborate-proc-formals \[ \] = complete .

\item elaborate-proc-formals \[ ~F:ProcFormal \] = \=
	give head-of (the proc-argument-list) then elaborate-proc-formal ~F .

\item elaborate-proc-formals \[ ~F:ProcFormal ``\verb%,%'' {\it FS}:ProcFormals \] = \=
	\(
	\< give head-of (the proc-argument-list) then elaborate-proc-formal ~F \> \\
	and then \\
	\< give tail-of (the proc-argument-list) then elaborate-proc-formals {\it FS} .\>
	\)
\end{spec}

 
\subsubsection{Elaborating Procedure Formal Parameter}

\begin{spec}

\item[$\:\bullet$]	elaborate-proc-formal \_ :: ProcFormal \into action .

\item elaborate-proc-formal \[ ~I:Identifier ``\verb%:%'' ~T:PrimitiveType \] = \=
	\(
	\< \< give the primitive-value label \#1 \>\\
           and\\
           \< allocate-for-primitive-value ~T then give the cell label \#2 \>
        \> \\
	then \\
	\< bind token-of ~I to the cell\#2 and store the primitive-value\#1 in the cell\#2 .\>
	\)

\item elaborate-proc-formal \[ ~I:Identifier ``\verb%:%'' ~T:FunctionType \] = \=
	bind token-of ~I to the function .

\item elaborate-proc-formal \[ ``\verb+var+'' ~I:Identifier ``\verb%:%'' ~T:Type \] =
	bind token-of ~I to the cell .

\end{spec}


\subsubsection{Elaborating Function Formal Parameters}

\begin{spec}

\item[$\:\bullet$]	elaborate-fun-formals \_ :: FunFormals \into action .

\item elaborate-fun-formals \[ \] = complete .

\item elaborate-fun-formals \[ ~F:FunFormal \] = \=
	give head-of (the fun-argument-list) then elaborate-fun-formal ~F .

\item elaborate-fun-formals \[ ~F:FunFormal ``\verb%,%'' {\it FS}:FunFormals \] = \=
	\(
	\< give head-of (the fun-argument-list) then elaborate-fun-formal ~F \> \\
	and then \\
	\< give tail-of (the fun-argument-list) then elaborate-fun-formals {\it FS} .\>
	\)

\end{spec}


\subsubsection{Elaborating Function Formal Parameter}

\begin{spec}

\item[$\:\bullet$]	elaborate-fun-formal \_ :: FunFormal \into action .

\item elaborate-fun-formal \[ ~I:Identifier ``\verb%:%'' ~T:ValueType \] = \=
	bind token-of ~I to the fun-argument .

\end{spec}


\subsubsection{Allocating Storage}

\begin{spec}
\item[\introduces] allocate-for-primitive-value \_ , allocate-for-array \_ .

\item[$\:\bullet$] allocate-for-primitive-value \_ :: PrimitiveType \into action .

\item allocate-for-primitive-value \[ ``\verb%bool%'' \] = allocate a truth-value-cell .

\item allocate-for-primitive-value \[ ``\verb%int%'' \] = allocate an integer-cell .


\item[$\:\bullet$] allocate-for-array \_ :: ArrayType \into action .

\item allocate-for-array \[ ``{\tt array}'' ``{\tt [}'' ~N:Numeral ``{\tt ]}'' ``{\tt of}'' ~T:PrimitiveType \] = \=
	\(
	\< 
	  \< give valuation-of ~N label \#1 \> \\
	  and \\
	  \< give 1 label \#2 \> \\
          and \\
          \< give empty-list label \#3 \>
	\> \\
	then \\
	\< unfolding\\
           \<
	   \<
	   \< \< check not (the integer\#1 is the integer\#2) \> \\
	      and then \\
	      \< \< give the integer\#1 label \#1 \> \\
	      and \\
              \< give successor (the integer\#2) label \#2 \> \\
	      and \\
	      \< \< allocate-for-primitive-value ~T and give the list\#3 label \#1 \> \\
	         then\\
	         \< give concatenation (the list\#1,list (the cell)) label \#3 \>
	      \> \>
           \> \\
	   then\\
	   \< unfold \>
           \> \\
	   or \\
           \<
	     \< \< check (the integer\#1 is the integer\#2) \> \\
	        and then \\
	        \< allocate-for-primitive-value ~T and give the list\#3 label \#1 \>
             \> \\
	     then\\
	     \< give concatenation(the list\#1,list (the cell)) . \>
           \>
        \>
	\>
	\)
\end{spec}


\subsection{Commands}

\begin{spec}

\item[\introduces] execute \_ , evaluate-actuals \_ , evaluate-actual \_.

%\item[\needs] \ide{Declarations} , \ide{Expressions} , \ide{Literals} .
\end{spec}


\subsubsection{Executing Commands}

\begin{spec}

\item[$\:\bullet$] execute \_ :: Command \into action . 

\item execute \[ ~I:Identifier ``\verb+:=+'' ~E:Expression \] = \=
	\(
	\< evaluate ~E \> \\
	then \\
	\< store the primitive-value in the cell bound to token-of ~I . \>
	\)

\item execute \[ ~I:Identifier ``{\tt [}'' ~E_1:Expression ``{\tt ]}'' ``{\tt :=}'' ~E_2:Expression \] = \=
	\(
	\< 
	  \< evaluate ~E_1 then give the integer label \#1 \> \\
	  and \\
	  \< evaluate ~E_2 then give the primitive-value label \#2 \> \\
	  and \\
	  \< give the list bound to token-of ~I label \#3 \> \\
          and \\
          \< give 1 label \#4 \>
	\> \\
	then \\
	\< unfolding\\
	   \<
	     \< \< check (the integer\#1 is the integer\#2) \> \\
	        and then \\
	        \< store the primitive-value\#2 in head-of (the list\#3) \>
             \> \\
	     or \\
             \<
	       \< check not (the integer\#1 is the integer\#2) \> \\
	       and then \\
	       \< \< \< give the integer\#1 label \#1 \> \\
                     and \\
                     \< give the primitive-value\#2 label \#2 \> \\
		     and \\
		     \< give tail-of (the list\#3) label \#3 \> \\
		     and \\
		     \< give successor (the integer\#4) label \#4 \>
		  \> \\
		  then \\
		  \< unfold . \>
               \>
             \>
           \>
        \>
	\)

\item   execute \[ ``\verb+if+'' ~E:Expression ``\verb+then+'' ~C:Command ``{\tt end}'' \] = \=
        \(
        \< evaluate ~E \> \\
        then \\
        \< 
	   \< execute ~C \> \\
           else \\
           \< complete . \> 
        \>
        \)

\item   execute \[ ``\verb+if+'' ~E:Expression ``\verb+then+'' ~C_1:Command  ``{\tt else}'' ~C_2:Command ``{\tt end}'' \] = \=
        \(
        \< evaluate ~E \> \\
        then \\
        \< 
	   \< execute ~C_1 \> \\
           else \\
           \< execute ~C_2 . \> 
        \>
        \)

\item   execute \[ ``\verb+while+'' ~E:Expression ``\verb+do+'' ~C:Command ``{\tt end}'' \] = \=
	\(
	unfolding \\
	\< 
	  \< evaluate ~E \> \\
	  then \\
	  \< 
	    \< execute ~C and then unfold \> \\
	    else \\
	    \< complete . \>
	  \>
	\>
	\)
 
\item	execute \[ ``{\tt call}'' ~I:Identifier ``\verb+(+'' {\it AS}:ProcActuals ``\verb+)+'' \] = \=
	\( 
	\< evaluate-proc-actuals {\it AS} \> \\
	then \\
	\< enact (the procedure bound to token-of ~I with the proc-argument-list) . \>
	\)

\item   execute \[ ``\verb+local+'' ~D:Declaration ``\verb+in+'' ~C:Command ``\verb+end+'' \] = \=
        \(
        \< furthermore elaborate ~D \> \\
        hence \\
        \< execute ~C . \>
        \)

\item  	execute \[ ~C_1:Command ``\verb+;+'' ~C_2:Command \] = execute ~C_1 and then execute ~C_2 .

\end{spec}

\subsubsection{Evaluating Procedure Actual Parameters}

\begin{spec}

\item[$\:\bullet$] evaluate-proc-actuals \_ :: ProcActuals \into action .

\item 	evaluate-proc-actuals \[ \] = give empty-list .

\item 	evaluate-proc-actuals \[ ~A:ProcActual \] = evaluate-proc-actual ~A then give list (it) .

\item 	evaluate-proc-actuals \[ ~A:ProcActual ``{\tt ,}'' {\it AS}:ProcActuals \] = \=
	\(
	\< \< evaluate-proc-actual ~A then give list (it) label \#1 \> \\
	   and \\
	   \< evaluate-proc-actuals {\it AS} then give it label \#2 \> 
	\> \\
	then \\
	\< \< give concatenation (the list\#1,the list\#2) . \>
        \>
	\)

\end{spec}


\subsubsection{Evaluating Procedure Actual Parameter}

\begin{spec}

\item[$\:\bullet$] evaluate-proc-actual \_ :: ProcActual \into action .

\item 	evaluate-proc-actual \[ ~E:Expression \] = evaluate ~E .

\item 	evaluate-proc-actual \[ ``{\tt var}'' ~I:Identifier \] = give the cell bound to token-of ~I .

\end{spec}


\subsection{Expressions}

\begin{spec}

\item[\introduces] evaluate \_ , apply-operator \_ .

%\item[\needs] \ide{Literals} .

\end{spec}


\subsubsection{Evaluating Expressions}

\begin{spec}

\item[$\:\bullet$] evaluate \_ :: Expression \into action .

\item   evaluate \[ ``{\tt true}'' \] = give true .

\item   evaluate \[ ``{\tt false}'' \] = give false . 

\item   evaluate \[ ~N:Numeral \] = give valuation-of ~N .
 
\item  	evaluate \[ ~I:Identifier \] = \=
	\(
	\< give the value bound to token-of ~I \> \\
%	or \\
%	\< give the function bound to token-of ~I \> \\
	or \\
	\< give the primitive-value stored in the cell bound to token-of ~I . \>
	\)

\item 	evaluate \[ ~I:Identifier ``{\tt [}'' ~E:Expression ``{\tt ]}'' \] = \=
	\(
	\< 
	  \< evaluate ~E then give the integer label \#1 \> \\
	  and \\
	  \< give the list bound to token-of ~I label \#2 \> \\
          and \\
          \< give 1 label \#3 \>
	\> \\
	then \\
	\< unfolding\\
	   \<
	     \< 
                \< check (the integer\#1 is the integer\#3) \> \\
	        and then \\
	        \< give the primitive-value stored in head-of (the list\#2) \>
             \> \\
	     or \\
             \<
	       \< check not (the integer\#1 is the integer\#3) \> \\
	       and then \\
	       \< 
                  \< 
                     \< give the integer\#1 label \#1 \> \\
                     and \\
		     \< give tail-of (the list\#2) label \#2 \> \\
		     and \\
		     \< give successor (the integer\#3) label \#3 \>
		  \> \\
		  then \\
		  \< unfold . \>
               \>
             \>
           \>
        \>
	\)

\item   evaluate \[ ``{\tt if}'' ~E_1:Expression ``{\tt then}'' ~E_2:Expression ``{\tt end}'' \] = \=
        \(
        \< evaluate ~E_1 \> \\
        then \\
        \< \< evaluate ~E_2 \> \\
           else \\
           \< complete . \> \>
        \)

\item   evaluate \[ ``{\tt if}'' ~E_1:Expression ``{\tt then}'' ~E_2:Expression ``{\tt else}'' ~E_3:Expression ``{\tt end}'' \] = \=
        \(
        \< evaluate ~E_1 \> \\
        then \\
        \< \< evaluate ~E_2 \> \\
           else \\
           \< evaluate ~E_3 . \> \>
        \)
 
\item   evaluate \[ ~I:Identifier ``\verb+(+'' {\it AS}:FunActuals ``\verb+)+'' \] = \=
        \(
        \< evaluate-fun-actuals {\it AS} \> \\
        then \\
        \< enact (the function bound to token-of ~I with the fun-argument-list) . \>
        \)

\item   evaluate \[ ~E_1:Expression ~O:Operator ~E_2:Expression \] = \=
        \(
        \< \< evaluate ~E_1 then give the value label \#1 \> \\
           and \\
           \< evaluate ~E_2 then give the value label \#2 \> \> \\
        then \\
        \< apply-operator ~O . \>
        \)

\item   evaluate \[ ~O:Operator ~E:Expression \] = \=
        \(
        \< evaluate ~E then give the value \> \\
        then \\
        \< apply-operator ~O . \>
        \)

\item   execute \[ ``\verb+let+'' ~D:Declaration ``\verb+in+'' ~E:Expression ``\verb+end+'' \] = \=
        \(
        \< furthermore elaborate ~D \> \\
        hence \\
        \< evaluate ~E . \>
        \)

%\item   evaluate \[ \verb'(' ~E:Expression \verb')' \] = evaluate ~E .

\end{spec}


\subsubsection{Evaluating Function Actual Parameters}

\begin{spec}

\item[$\:\bullet$] evaluate-fun-actuals \_ :: FunActuals \into action .

\item 	evaluate-fun-actuals \[ \] = give empty-list .

\item 	evaluate-fun-actuals \[ ~A:Actual \] = evaluate-fun-actual ~A then give list (it) .

\item 	evaluate-fun-actuals \[ ~A:Actual ``{\tt ,}'' {\it AS}:Actuals \] = \=
	\(
	\< \< evaluate-fun-actual ~A then give list (it) label \#1 \> \\
	   and \\
	   \< evaluate-fun-actuals {\it AS} then give it label \#2 \> 
	\> \\
	then \\
	\< \< give concatenation (the list\#1,the list\#2) . \>
        \>
	\)

\end{spec}


\subsubsection{Evaluating Function Actual Parameter}

\begin{spec}

\item[$\:\bullet$] evaluate-fun-actual \_ :: FunActual \into action .

\item 	evaluate-fun-actual \[ ~E:Expression \] = evaluate ~E .

\end{spec}


\subsubsection{Applying Operators}

\begin{spec}

\item[$\:\bullet$] apply-operator \_ :: Operator \into action .

\item apply-operator \[ ``\verb%not%'' \] = give not (the truth-value) .
 
\item apply-operator \[ ``\verb%and%'' \] = give both (the truth-value\#1, the truth-value\#2) .
 
\item apply-operator \[ ``\verb%or%'' \] = give either (the truth-value\#1, the truth-value\#2) .

\item apply-operator \[ ``\verb%~%'' \] = give negation (the integer) .
 
\item apply-operator \[ ``\verb%+%'' \] = give sum (the integer\#1, the integer\#2) .
 
\item apply-operator \[ ``\verb%-%'' \] = give difference (the integer\#1, the integer\#2) .

\item apply-operator \[ ``\verb%*%'' \] = give product (the integer\#1, the integer\#2) .

\item apply-operator \[ ``\verb%/%'' \] = give integer-quotient (the integer\#1, the integer\#2) .

\item apply-operator \[ ``\verb%<%'' \] = give is-less-than (the integer\#1, the integer\#2) .

\item apply-operator \[ ``\verb%>%'' \] = give is-greater-than (the integer\#1, the integer\#2) .

\item apply-operator \[ ``\verb%<=%'' \] = give either (\(is-less-than (the integer\#1, the integer\#2),\\
						      the integer\#1 is the integer\#2) .\)

\item apply-operator \[ ``\verb%>=%'' \] = give either (\(is-greater-than (the integer\#1, the integer\#2),\\
						      the integer\#1 is the integer\#2) .\)

\item apply-operator \[ ``\verb%=%'' \] = give (the primitive-value\#1 is the primitive-value\#2) .

\item apply-operator \[ ``\verb%<>%'' \] = give not (the primitive-value\#1 is the primitive-value\#2) .
\end{spec}


\section{Lexical Syntax}

\begin{spec}
\settowidth{\wordlength}{Identifier}
\tabset \makebox[\wordlength][r]{Identifier} &=&

\item[\introduces] token-of \_ , valuation-of \_ .

\item[closed]

\item[\grammar]

\item \tab \makebox[\wordlength][r]{Identifier} &=&  letter \| Identifier letter \| Identifier digit .

\item \tab \makebox[\wordlength][r]{Numeral} &=& digit \| Numeral digit . 

\item \tab \makebox[\wordlength][r]{digit} &=& \verb+0+ \| \verb+1+ \| \dots \| \verb+9+ .

\item \tab \makebox[\wordlength][r]{letter} &=& \verb+A+ \| \verb+B+ \| \dots \| \verb+Z+ \| \verb+a+ \| \dots \| \verb+z+ .

\end{spec}


\subsection{Identifiers}

\begin{spec}

\item[$\:\bullet$] token-of \_ :: Identifier \into token .

\item token-of \[ ~I \] = ~I .

\end{spec}


\subsection{Numerals}

\begin{spec}
%\tabset  valuation-of \[ ~N ~D \] &=&

\item[$\:\bullet$] valuation-of \_ :: Numeral \into integer .

\item valuation-of \[ \verb+0+ \] = 0 .

\item valuation-of \[ \verb+1+ \] = 1 .
 
\item valuation-of \[ \verb+2+ \] = 2 .
 
\item valuation-of \[ \verb+3+ \] = 3 .
 
\item valuation-of \[ \verb+4+ \] = 4 .
 
\item valuation-of \[ \verb+5+ \] = 5 .
 
\item valuation-of \[ \verb+6+ \] = 6 .
 
\item valuation-of \[ \verb+7+ \] = 7 .
 
\item valuation-of \[ \verb+8+ \] = 8 .
 
\item valuation-of \[ \verb+9+ \] = 9 .
 
\item valuation-of \[ ~N ~D \] = sum (product (valuation-of ~N, 10), valuation-of ~D) .

\end{spec}

%\end{document}
