%
%\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] \ide{Abstract Syntax} . %\ \ \except \ide{Literals} .
\end{spec}
%
\subsection{Programs}
\begin{spec}
\item[\needs] \ide{Declarations} , \ide{Commands} .
\item[\grammar]
\item Program = \verb%program% Identifier \verb'=' Declaration \verb%in% Command \verb%end% .
\end{spec}
%
\subsection{Declarations}
\begin{spec}\tabset Declaration &=&
\item[\needs] \ide{Commands} , \ide{Expressions} , \ide{Types} .
\item[\grammar]
\item \tab Declaration &=& 
\verb%const% Identifier \verb%:% Type \verb%=% Expression \| \=
\verb%var% Identifier \verb%:% Type \verb%:=% Expression \| \=
\verb%proc% Identifier ProcFormal = Command \verb%end% \| \=
\verb+fun+ Identifier Identifier \verb+:+ Type \verb'->' Type \verb+=+ Expression \| \=
Declaration \verb+;+ Declaration .
%
\item \tab	ProcFormal &=& \verb'()' \| \=
			     \verb'(' Identifier \verb+:+ Type \verb')' \| \=
			     \verb'( var' Identifier \verb+:+ Type \verb')' .
\end{spec}
%
\subsection{Commands}
\begin{spec}
\item[\grammar]\tabset ProcArgument &=&
\item \tab Command &=& 
	Identifier \verb%:=% Expression \| \=
	\verb%if% Expression \verb%then% Command \verb%else% Command \| \=
	\verb%while% Expression \verb%do% Command {\bf\verb+end+} \| \=
	\verb%local% Declaration \verb%in% Command \verb%end% \| \=
	Identifier \verb'()' \| \=
 	Identifier \verb%(% ProcArgument \verb%)% \| \=
	Command \verb%;% Command .
%
\item \tab ProcArgument &=& Expression \| \=
			 \verb'var' Identifier .
\end{spec}
%
\subsection{Expressions}
\begin{spec}\tabset Argument &=&
%\item[\needs] \ide{Lexical Syntax} .
\item[\grammar]
\item \tab Expression &=&
	\verb%true% \| \=
	\verb%false% \| \=
	Numeral \| \=
	Identifier \| \=
	\verb%if% Expression \verb%then% Expression \verb%else% Expression \| \=
	Identifier Expression \| \=
	Expression Operator Expression \| \=
	Operator Expression \| \=
	\verb'(' Expression \verb')' .

\item \tab Operator &=& \verb+not+ \|
		     \verb+and+ \|
		     \verb+or+ \| 
		     \verb%+% \| 
		     \verb+-+ \| 
		     \verb+*+ \| 
		     \verb+/+ \| \verb+=+ \| \verb+<+ .
\end{spec}
%
\subsection{Types}
\begin{spec}\tabset Type &=&
\item[\grammar]
\item \tab Type &=& \verb+bool+ \| \verb+int+ .
\end{spec}
%
\section{Semantic Entities}
\begin{spec}
\item[\needs] \ide{Standard} .
\end{spec}
%
\subsection{Data}
\begin{spec}
\item[\introduces] value .
\item value = truth-value \| integer .
\end{spec}
%
\subsection{Bindings}
\begin{spec}
\item[\needs] \ide{Data} , \ide{Storage} , \ide{Abstractions} .
\item token = symbol .
\item bindable(~T:token) = value \| procedure \| function \| cell .
\end{spec}
%
\subsection{Storage}
\begin{spec}
\item[\introduces] truth-value-cell , integer-cell , allocate-a-cell-for \[ \_ \] .
\item cell = truth-value-cell \| integer-cell .
\item storable(~C:truth-value-cell) = truth-value .
\item storable(~C:integer-cell) = integer .
\item[\ $\bullet$] allocate-a-cell-for \[ \_ \] :: Type \into act .
\item allocate-a-cell-for \[ \verb%bool% \] = allocate a truth-value-cell .
\item allocate-a-cell-for \[ \verb%int% \] = allocate an integer-cell .
\end{spec}
%
\subsection{Abstractions}
\begin{spec}
\item[\introduces] procedure , function , proc-argument , fun-argument , 
                   fun-result .
\item[\needs] \ide{Data} , \ide{Storage} .
\item procedure = abstraction .
\item function = abstraction .
\item proc-argument = value \| cell .
\item fun-argument = value .
\item fun-result = value .
\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 act .
\item run \[ \verb+program+ ~I \verb+=+ ~D \verb+in+ ~C \verb+end+ \] = 
	\(
	\< elaborate \[ ~D \] \> \\
	hence \\
	\< execute \[ ~C \] . \>
	\)
\end{spec}
%
\subsection{Declarations}
\begin{spec}
\item[\introduces] \( elaborate \[ \_ \] , \\
	              elaborate-proc-formal \[ \_ \] .
		   \)
\item[\needs] \ide{Commands} , \ide{Expressions} , \ide{Types} .
\end{spec}
%
\subsubsection{Elaborating Declarations}
\begin{spec}
\item[\ $\bullet$]	elaborate \[ \_ \] :: Declaration \into act .
\item	elaborate \[ \verb+const+ ~I \verb+:+ ~T \verb+=+ ~E \] = \=
	\(
	\< evaluate \[ ~E \] \> \\
	then \\
	\< bind token-of \[ ~I \] to the value . \>
	\)
\item	elaborate \[ \verb+var+ ~I \verb+:+ ~T \verb+=+ ~E \] = \=
	\(
	\< \< evaluate \[ ~E \] then give the value label \#1 \> \\
	   and \\
	   \< allocate-a-cell-for \[ ~T \] then give it label \#2 \> 
	\> \\
	then \\
	\< \< bind token-of \[ ~I \] to the cell\#2 \> \\
	   and \\
	   \< store the value\#1 in the cell\#2 . \>
        \>
	\) 
\item   elaborate \[ \verb+proc+ ~I ~F \verb+=+ ~C \verb'end' \] = \=
	\(
	recursively bind token-of \[ ~I \] to closure abstraction \=
	      \< \< rebind moreover elaborate-proc-formal \[ $F$ \] \> \\
		 hence \\
		 \< execute \[ ~C \] . \>
	      \>
	\) 
\item   elaborate \[ \verb+fun+ ~I_1 ~I_2 \verb':' ~T_1 \verb'->' ~T_2 \verb+=+ ~E \] = \=
	\(
	recursively bind token-of \[ ~I_1 \] to closure abstraction \=  
	      \< \< rebind moreover bind token-of \[ ~I_2 \] to the fun-argument \> \\
	         hence \\
                 \< evaluate \[ ~E \] then give the fun-result . \>
	      \>
	\)
\item	elaborate \[ ~D\on1 \verb+;+ ~D\on2 \] = \=
	\(
	\< elaborate \[ ~D\on1 \] \> \\
	before \\
	\< elaborate \[ ~D\on2 \] . \> 
	\)
\end{spec}
%
\subsubsection{Elaborating Procedure Formal Parameter}
\begin{spec}
\item[\ $\bullet$]	elaborate-proc-formal \[ \_ \] :: ProcFormal \into act .
\item elaborate-proc-formal \[ \verb'()' \] = complete .
\item elaborate-proc-formal \[ ~I \verb%:% ~T \] = \=
	\(
	\< give the value label \#1 and allocate a cell\> \\
	then \\
	\< bind token-of \[ ~I \] to it and store the value\#1 in it .\>
	\) 
\item elaborate-proc-formal \[ \verb+var+ ~I \verb%:% ~T \] =
bind token-of \[ ~I \] to the cell . 
\end{spec}
%
\subsection{Commands}
\begin{spec}
\item[\introduces] execute \[ \_ \] ,
		   evaluate-proc-argument \[ \_ \] .
\item[\needs] \ide{Declarations} , \ide{Expressions} , \ide{Literals} .
\end{spec}
\subsubsection{Executing Commands}
\begin{spec}
\item[\ $\bullet$] execute \[ \_ \] :: Command \into act . 
\item execute \[ ~I \verb+:=+ ~E \] = \=
	\(
	\< evaluate \[ ~E \] \> \\
	then \\
	\< store the value in the cell bound to token-of \[ ~I \] . \>
	\)
\item   execute \[ \verb+if+ ~E \verb+then+ ~C\on1 \verb+else+ ~C\on2 \] = \=
        \(
        \< evaluate \[ ~E \] \> \\
        then \\
        \< \< check (it is true) and then execute \[ ~C\on1 \] \> \\
           or \\
           \< check (it is false) and then execute \[ ~C\on2 \] . \> \>
        \) 
\item   execute \[ \verb+while+ ~E \verb+do+ ~C \] = \=
	\(
	unfolding \\
	\< \< evaluate \[ ~E \] \> \\
	then \\
	\< \< check the truth-value and then execute \[ ~C \] and then unfold \> \\
	   or \\
	   \< check not the truth-value . \>
	\>
	\>
	\) 
\item   execute \[ \verb+local+ ~D \verb+in+ ~C \verb+end+ \] = \=
        \(
        \< rebind moreover elaborate \[ ~D \] \> \\
        hence \\
        \< execute \[ ~C \] . \>
        \)
\item   execute \[ ~I \verb'()' \] = \= 
	enact the procedure bound to token-of ~I .
\item	execute \[ ~I \verb%(% $A$ \verb%)% \] = \=
	\( 
	\< evaluate-proc-argument \[ ~A \] \> \\
	then \\
	\< enact (the procedure bound to token-of \[ ~I \] with the proc-argument) . \>
	\) 
\item  	execute \[ ~C\on1 \verb+;+ ~C\on2 \] = execute \[ ~C\on1 \] and then execute \[ ~C\on2 \] .
\end{spec}
%
\subsubsection{Evaluating a Procedure Argument}
\begin{spec}
\item[\ $\bullet$]	evaluate-proc-argument \[ \_ \]  :: ProcArgument \into act .

\item 	evaluate-proc-argument \[ ~E\verb':'Expression \] = 
		evaluate ~E .

\item 	evaluate-proc-argument \[ \verb'var' ~I\verb':'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 act .
\item   evaluate \[ \verb%true% \] = give true .
\item   evaluate \[ \verb%false% \] = give false . 
\item   evaluate \[ ~N \] = give valuation-of \[ ~N \] . 
\item  	evaluate \[ ~I \] = \=
	\(
	\< give the value bound to token-of \[ ~I \] \> \\
	or \\
	\< give the value stored in the cell bound to token-of \[ ~I \] . \>
	\)
\item   evaluate \[ \verb+if+ ~E \verb+then+ ~E\on1 \verb+else+ ~E\on2 \] = \=
        \(
        \< evaluate \[ ~E \] \> \\
        then \\
        \< \< check (it is true) and then evaluate \[ ~E\on1 \] \> \\
           or \\
           \< check (it is false) and then evaluate \[ ~E\on2 \] . \> \>
        \)  
\item   evaluate \[ ~I ~E \] = \=
        \(
        \< evaluate \[ ~E \] \> \\
        then \\
        \< enact (the function bound to token-of \[ ~I \] with the fun-argument) . \>
        \)
\item   evaluate \[ ~E\on1 ~O ~E\on2 \] = \=
        \(
        \< \< evaluate \[ ~E\on1 \] then give the value label \#1 \> \\
           and \\
           \< evaluate \[ ~E\on2 \] then give the value label \#2 \> \> \\
        then \\
        \< apply-operator \[ ~O \] . \>
        \)
\item   evaluate \[ ~O ~E \] = \=
        \(
        \< evaluate \[ ~E \] then give the value \> \\
        then \\
        \< apply-operator \[ ~O \] . \>
        \)
\item   evaluate \[ \verb'(' ~E \verb')' \] = evaluate \[ ~E \] .
\end{spec}
%
\subsubsection{Evaluating Operators}
\begin{spec}
\item[\ $\bullet$]	apply-operator \[ \_ \]  :: Operator \into act .
\end{spec}
\begin{spec}
\item apply-operator \[ \verb%not% \] = give not (the truth-value) . 
\item apply-operator \[ \verb%and% \] =
	give conjunction (the truth-value\#1, the truth-value\#2) . 
\item apply-operator \[ \verb%or% \] =
	give disjunction (the truth-value\#1, the truth-value\#2) . 
\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 quotient (the integer\#1, the integer\#2) .
\item apply-operator \[ \verb%=% \] = give (the value\#1 is the value\#2) .
\item apply-operator \[ \verb%<% \] = 
	give is-less-than (the integer\#1, the integer\#2) .
\end{spec}
%
\section{Lexical Syntax}
\begin{spec}
\item[\introduces] token-of \[ \_ \] , valuation-of \[ \_ \] .
\end{spec}
\begin{spec} \tabset Identifier &=&
\item[\grammar]
\item \tab Identifier &=&  letter \| \=
                        Identifier letter \| \=
			Identifier digit .
\item \tab Numeral &=& digit \| \=
        	    Numeral digit . 
\item \tab digit  &=& \verb+0+ \| \verb+1+ \| \dots \| \verb+9+ .
\item \tab 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}
\item[\ $\bullet$] valuation-of \[ \_ \] :: Numeral \into integer .
\end{spec}
\begin{spec} \tabset valuation-of \[ ~N ~D \] &=&
\item \tab valuation-of \[ \verb+0+ \] &=& 0 . 
\item \tab valuation-of \[ \verb+1+ \] &=& 1 . 
\item \tab valuation-of \[ \verb+2+ \] &=& 2 . 
\item \tab valuation-of \[ \verb+3+ \] &=& 3 . 
\item \tab valuation-of \[ \verb+4+ \] &=& 4 . 
\item \tab valuation-of \[ \verb+5+ \] &=& 5 . 
\item \tab valuation-of \[ \verb+6+ \] &=& 6 . 
\item \tab valuation-of \[ \verb+7+ \] &=& 7 . 
\item \tab valuation-of \[ \verb+8+ \] &=& 8 . 
\item \tab valuation-of \[ \verb+9+ \] &=& 9 . 
\item \tab valuation-of \[ ~N ~D \] &=&
	sum (product (valuation-of \[ ~N \], 10), valuation-of \[ ~D \]) .
\end{spec}
%
\end{document}




