%
%\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 = \[ \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 \verb+(+ Formals \verb+) =+ Command \verb%end% \] \| \=
			   \[ \verb+fun+ Identifier \verb+(+ Formals \verb+) :+ Type \verb+=+ Expression \] \| \=
			   \[ Declaration \verb+;+ Declaration \] .

\item \tab     Formals &=& \[ \] \| \=
			   \[ Formal \] \| \=
			   \[ Formal \verb+,+ Formals \] .

\item \tab      Formal &=& \[ Identifier \verb+:+ Type \] \| \=
		   	   \[ \verb'var' Identifier \verb+:+ Type \] \| \=
	       		   \[ \verb'fun' Identifier \verb+:+ Type \] .

\end{spec}
%
\subsection{Commands}
\begin{spec}
%\item[\grammar]
\tabset Command &=&
\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+(+ Actuals \verb+)+ \] \| \=
		       \[ Command \verb%;% Command \] .

\item \tab Actuals &=& \[ \] \| \=
		       \[ Actual \] \| \=
		       \[ Actual \verb',' Actuals \] .

\item \tab  Actual &=& \[ Expression \] \| \=
		       \[ \verb'var' Identifier \] \| \=
		       \[ \verb'fun' Identifier \] .
\end{spec}

\subsection{Expressions}

\begin{spec}
\tabset ArrayComponents &=&
%\item[\needs] \ide{Lexical Syntax} .
%\item[\grammar]
\item \tab Expression &=& \verb%true% \| \=
		          \verb%false% \| \=
		          Numeral \| \=
		          \[ \verb+[+ ArrayComponents \verb+]+ \] \| \=
		          Identifier \| \=
		          \[ \verb%if% Expression \verb%then% Expression \verb%else% Expression \] \| \=
		          \[ Identifier \verb+(+ Actuals \verb+)+ \] \| \=
		          \[ Expression Operator Expression \] \| \=
		          \[ Operator Expression \] \| \=
		          \[ \verb'(' Expression \verb')' \] .

\item \tab ArrayComponents &=& Expression \| \=
		    	       \[ Expression \verb',' ArrayComponents \] .

\item \tab Operator &=& \verb+not+ \|
		     	\verb+and+ \|
		     	\verb+or+ \| 
		     	\verb%+% \| 
		     	\verb+-+ \| 
		     	\verb+*+ \| 
		     	\verb+/+ \| \verb+=+ \| \verb+>+ \| \verb+<+ .
\end{spec}
%
\subsection{Type Denoters}

\begin{spec}
\tabset Type &=&
\item \tab Type &=& \verb+bool+ \| \=
		    \verb+int+ \| \=
		    \verb+array [+ Numeral \verb+] of + Type \| \=
		    Type \verb+->+ Type \| \=
		    \verb+(+ Type \verb+,+ Type \verb+)+ \| \=
		    \verb+unit+ .
\end{spec}
%
\section{Semantic Entities}
\begin{spec}
\item[\includes] \ide{Action Notation} .
\end{spec}

\subsection{Data}

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

\subsection{Bindings}
\begin{spec}
%\item[\needs] \ide{Data} , \ide{Storage} , \ide{Abstractions} .
\item token = symbol .
\item bindable(~T:token) = value \| procedure \| cell .
\end{spec}
%
\subsection{Storage}
\begin{spec}
\item[\introduces] truth-value-cell , integer-cell , array-cell , allocate-a-cell-for \_ .
\item cell = truth-value-cell \| integer-cell \| array-cell .
\item storable(~C:truth-value-cell) = truth-value .
\item storable(~C:integer-cell) = integer .
\item storable(~C:array-cell) = array .
\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 .
\item allocate-a-cell-for \[ \verb%array% ~N \verb%of% ~T\] = allocate ... .
\end{spec}

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

\subsection{Arrays}
\begin{spec}
\item	\hole .
\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:Identifier \verb+=+ ~D:Declaration \verb+in+ ~C :Command \verb+end+ \] = \=
	\(
	\< elaborate ~D \> \\
	hence \\
	\< execute ~C . \>
	\)
\end{spec}


\subsection{Declarations}

\begin{spec}

\item[\introduces] elaborate \_ , elaborate-proc-formals \_ , elaborate-fun-formals \_ .

%\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:Identifier \verb+:+ ~T:Type \verb+=+ ~E:Expression \] = \=
	\(
	\< evaluate ~E \> \\
	then \\
	\< bind token-of ~I to the value . \>
	\)

\item	elaborate \[ \verb+var+ ~I:Identifier \verb+:+ ~T:Type \verb+:=+ ~E:Expression \] = \=
	\(
	\< \< 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:Identifier ~FS:Formals \verb+=+ ~C:Command \verb'end' \] = \=
	\(
	recursively bind token-of ~I to closure abstraction \=
	      \< \< furthermore elaborate-proc-formals ~FS \> \\
		 hence \\
		 \< execute ~C . \>
	      \>
	\)

\item   elaborate \[ \verb+fun+ ~I:Identifier ~FS:Formals \verb':' ~T:Type \verb+=+ ~E:Expression \] = \=
	\(
	recursively bind token-of ~I to closure abstraction \=  
	      \< \< furthermore elaborate-fun-formals ~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{Elaborating Procedure Formal Parameters}

\begin{spec}

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

\item[\ $\bullet$]	elaborate-proc-formals \_ :: Formals \into act .

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

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

\item elaborate-proc-formals \[ ~F:Formal \verb%,% ~FS:Formals \] = \=
	\(
	\< give head-of (the argument-list) then elaborate-proc-formal ~F \> \\
	and then \\
	\< give tail-of (the argument-list) then elaborate-proc-formals ~FS .\>
	\)
 

\item[\ $\bullet$]	elaborate-proc-formal \_ :: Formal \into act .

\item elaborate-proc-formal \[ ~I:Identifier \verb%:% ~T:Type \] = \=
	\(
	\< give the value label \#1 and allocate-a-cell-for ~T \> \\
	then \\
	\< bind token-of ~I to it and store the value\#1 in it .\>
	\)
 
\item elaborate-proc-formal \[ \verb+var+ ~I:Identifier \verb%:% ~T:Type \] =
	bind token-of ~I to the cell .

\item elaborate-proc-formal \[ \verb+fun + ~I:Identifier \verb%:% ~T:Type \] =
	bind token-of ~I to the function .
\end{spec}


\subsubsection{Elaborating Function Formal Parameters}

\begin{spec}

\item[\introduces] 	elaborate-fun-formal \_ .

\item[\ $\bullet$]	elaborate-fun-formals \_ :: Formals \into act .

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

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

\item elaborate-fun-formals \[ ~F:Formal \verb%,% ~FS:Formals \] = \=
	\(
	\< give head-of (the argument-list) then elaborate-fun-formal ~F \> \\
	and then \\
	\< give tail-of (the argument-list) then elaborate-fun-formals ~FS .\>
	\)


\item[\ $\bullet$]	elaborate-fun-formal \_ :: Formal \into act .

\item elaborate-fun-formal \[ ~I:Identifier \verb%:% ~T:Type \] = \=
	\(
	\< give the value label \#1 and allocate-a-cell-for ~T \> \\
	then \\
	\< bind token-of ~I to it and store the value\#1 in it .\>
	\)
 
\item elaborate-fun-formal \[ \verb+var+ ~I:Identifier \verb%:% ~T:Type \] =
	bind token-of ~I to the cell .

\item elaborate-fun-formal \[ \verb+fun + ~I:Identifier \verb%:% ~T:Type \] =
	bind token-of ~I to the function .
\end{spec}


\subsection{Commands}

\begin{spec}

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

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


\subsubsection{Executing Commands}

\begin{spec}

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

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

\item   execute \[ \verb+if+ ~E:Expression \verb+then+ ~C_1:Command \verb+else+ ~C_2:Command \] = \=
        \(
        \< evaluate ~E \> \\
        then \\
        \< \< check (it is true) and then execute ~C_1 \> \\
           or \\
           \< check (it is false) and then execute ~C_2 . \> \>
        \)

\item   execute \[ \verb+while+ ~E:Expression \verb+do+ ~C:Command \] = \=
	\(
	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:Declaration \verb+in+ ~C:Command \verb+end+ \] = \=
        \(
        \< furthermore elaborate ~D \> \\
        hence \\
        \< execute ~C . \>
        \)

\item	execute \[ ~I \verb+(+ $AS$ \verb+)+ \] = \=
	\( 
	\< evaluate-proc-actuals $AS$ \> \\
	then \\
	\< enact (the procedure bound to token-of ~I with the proc-argument) . \>
	\)

\item  	execute \[ ~C_1 \verb+;+ ~C_2 \] = execute ~C_1 and then execute ~C_2 .

\end{spec}

\subsubsection{Evaluating Procedure Actual Arguments}

\begin{spec}

\item[\ $\bullet$] evaluate-proc-actuals \_ :: Actuals \into act .

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

\item 	evaluate-proc-actuals \[ ~A:Actual \] = 
		elaborate-proc-actual ~A .

\item 	evaluate-proc-actuals \[ ~A:Actual \verb',' $AS$:Actuals \] = \=
	\(
	\< \< elaborate-proc-actual ~A then give it label \#1 \> \\
	   and \\
	   \< eaborate-proc-actuals $AS$ then give it label \#2 \> 
	\> \\
	then \\
	\< \< give concatenation (the list\#1,the list\#2) . \>
        \>
	\)

\end{spec}

\subsubsection{Evaluating a Procedure Actual Argument}

\begin{spec}

\item[\ $\bullet$] evaluate-proc-actual \_ :: Actual \into act .

\item 	evaluate-proc-actual \[ ~E:Expression \] = 
		evaluate ~E then give list(it) .

\item 	evaluate-proc-actual \[ \verb'var' ~I:Identifier \] = 
		give list (the cell bound to token-of ~I) .

\item elaborate-proc-formal \[ \verb+fun+ ~I:Identifier \] =
	        give list (the function bound to token-of ~I) .
\end{spec}


\subsection{Expressions}

\begin{spec}

\item[\introduces] evaluate \_ , evaluate-fun-actuals \_ , 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:Numeral \] = give valuation-of ~N .
 
\item  	evaluate \[ ~I:Identifier \] = \=
	\(
	\< 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:Expression \verb+then+ ~E_1:Expression \verb+else+ ~E_2:Expression \] = \=
        \(
        \< evaluate ~E \> \\
        then \\
        \< \< check (it is true) and then evaluate ~E_1 \> \\
           or \\
           \< check (it is false) and then evaluate ~E_2 . \> \>
        \)
 
\item   evaluate \[ ~I:Identifier \verb+(+ $AS$:Actuals \verb+)+ \] = \=
        \(
        \< evaluate-fun-actuals ~AS \> \\
        then \\
        \< enact (the function bound to token-of ~I with the 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   evaluate \[ \verb'(' ~E:Expression \verb')' \] = evaluate ~E .

\end{spec}

\subsubsection{Evaluating Function Actual Arguments}

\begin{spec}

\item[\ $\bullet$] evaluate-proc-actuals \_ :: Actuals \into act .

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

\item 	evaluate-fun-actuals \[ ~A:Actual \] = 
		elaborate-fun-actual ~A .

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

\end{spec}

\subsubsection{Evaluating a Function Actual Argument}

\begin{spec}

\item[\ $\bullet$] evaluate-fun-actual \_ :: Actual \into act .

\item 	evaluate-fun-actual \[ ~E:Expression \] = 
		evaluate ~E then give list(it) .

\item 	evaluate-fun-actual \[ \verb'var' ~I:Identifier \] = \=
		give list (the value stored in the cell bound to token-of ~I) .

\item elaborate-fun-formal \[ \verb+fun+ ~I:Identifier \] =
	        give list (the function bound to token-of ~I) .
\end{spec}


\subsubsection{Evaluating Operators}

\begin{spec}

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

\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}
\tabset Identifier &=&

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

\item[closed]

\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}
\tabset  valuation-of \[ ~N ~D \] &=&

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

\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}
