\section{Informal Description}
%
\specimen\ is a simple imperative programming language. It has two types of
abstractions: procedures and functions, which can be recursive.
Functions are higher-order and free of side effects,
although they can access non-local variables. Integers,
booleans, and arrays are the only data types in the language.
%
%\specimen\ is the largest of a group of four imperative languages used in
%our research on semantics-directed compiler generation.
%(The other three are {\sc nanoSpecimen}, {\sc microSpecimen} and
%{\sc milliSpecimen}.)
%
\subsection{Programs}
\subsection*{Syntax}
\begin{spec}
\item[] Program = \[ ``{\tt program}'' Identifier ``{\tt is}'' Declaration ``{\tt in}'' Command ``{\tt end}'' \] .
\end{spec}
%
\subsection*{Semantics}

\begin{itemize}
\item	A \specimen\ program is a declaration followed by a command.
	The execution of
	a program consists of the elaboration of the declaration,
	followed by the execution of the command using the bindings produced
	by the declaration. These bindings are visible throughout the
	command (global bindings); holes in the scope of global bindings can 
	occur by local declarations of the same global identifier.
\end{itemize}

\subsection*{Examples}

Figure~\ref{fb-8} and \ref{fb-9} show two examples of \specimen\ programs.

\input{fb-8}

\input{fb-9}

\begin{comment}
Figure~\ref{fb-1} shows an (artificial) \specimen\ program that computes the
factorial of 9.
%
\input{fb-1}
%
Program {\it fact9f} in Figure~\ref{fb-2}, which also computes the
factorial of 9,
uses a function instead of a procedure. Note the recursive declaration of
$fact$.

\input{fb-2}
\end{comment}

\subsection{Type Denoters}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection*{Syntax}

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

\subsection*{Semantics}

Types of constants, variables, procedures, functions and arrays must be explicitly declared.
A \specimen\ expression always evaluate to a value of type {\sf ValueType}. Booleans and
integers are primitive values; they have type {\sf PrimitiveValue}. Array components are
primitive values.
\subsection*{Examples}

\begin{itemize}
\item	{\it int} is the type of integer values.
\item	{\bf array} {\tt [20]} {\bf of} {\it bool} is the type of an array of 20 components of type {\it bool}.
\item	{\tt ({\it int},{\it int}) -> {\it bool}} is the type of a function which expects two arguments of
	type {\it int} and returns a result of type {\it bool}.
\item	{\tt {\it bool} -> ({\it int} -> {\it int})} is the type of a function which expects one argument of type
	{\it bool} and returns a function of type {\tt {\it int} -> {\it int}} as its result.
\end{itemize}


\subsection{Declarations}

\subsection*{Syntax}

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

\item ArrayComps = Expression \| \[ Expression ``{\tt ,}'' ArrayComps \] .

\item ProcFormals = \[ \] \| \[ ProcFormal \] \| \[ ProcFormal ``\verb+,+'' ProcFormals \] .

\item ProcFormal = \[ Identifier ``\verb+:+'' ValueType \] \| \[ ``{\tt var}'' Identifier ``\verb+:+'' PrimitiveType \] .

\item FunFormals = \[ \] \| \[ FunFormal \] \| \[ FunFormal ``\verb+,+'' FunFormals \] .

\item FunFormal = \[ Identifier ``\verb+:+'' ValueType \] .
\end{spec}

\subsection*{Semantics}

Declarations allow the programmer to make bindings. \specimen\ has four
types of declarations: constant, variable, procedure and
function declarations. Procedure and function declarations can be 
recursive. A \specimen\ program must have at least one declaration.

\begin{itemize}
\item	A constant declaration ``{\bf const} $I${\tt :}$T${\tt \ =\ }$E$'' binds the
	constant identifier $I$
	to the primitive value yielded by the evaluation of expression $E$.
	$I$ and $E$ have primitive type $T$.

\item	A variable declaration ``{\bf var} $I${\tt :}$T${\tt \ :=\ }$E$'' binds the variable
	identifier $I$ to a newly
	allocated cell. The result of the evaluation of the expression $E$ is
	stored in this cell. $I$ and $E$ have primitive type $T$.

\item	An array declaration ``{\bf varray} $I${\tt :}{\bf array} [$N$] {\bf of} $T${\tt \ :=\ }$E$'' binds the
	array variable identifier $I$ to a list of $N$ newly allocated cell.
	The expression $E$, an array aggregate with $N$ components, is evaluated
	and every resultant component is stored in the correspondent cell.
	$I$ and $E$ have array type ``{\bf array} {\tt [}$N${\tt ]} {\bf of} $T$'', where $T$ is
	a primitive type.

\item	A procedure declaration ``{\tt proc $I$ ($FS$) = $C$}'' binds the
	procedure identifier $I$ to a procedure. A procedure is 
	a {\em command abstraction}. Zero or more formal parameters can
	be defined in the procedure declaration.
	Parameters can be passed by value or by reference (var parameters).
	When passed by value, the argument, a value, is bound to the correspondent
	formal parameter; when passed by reference the argument, a cell, is
	bound to the correspondent formal variable.
	The body of a procedure is just	a command. The command
	is executed in an the same environment of the procedure declaration
	overlaid by the bindings produced by the elaboration of the
	procedure and its formal parameters.
	No result is returned, a procedure works by its side effects only.
	Procedure can be recursive. Procedures cannot be passed as parameters
	(of procedures or functions) or return as result of functions.

\item	A function declaration ``{\tt fun $I$ ($FS$):$T$ = $E$}'' binds the
	function identifier $I$ to a function.
	A function is an {\em expression abstraction}.
	\specimen\ functions can have zero
	or more parameters. Parameters are passed by value only.
	The body of a function is just an expression which is
	evaluated in the same environment of the function declaration
	overlaid by the bindings produced by the elaboration of the
	function and its formal parameters.
	An application of function $I$ always returns a value of
	value type $T$. Functions can be recursive.

\item	The sequential declaration ``{\tt $D_1$ ; $D_2$}'' is elaborated
	by elaborating $D_1$ and then elaborating $D_2$. $D_2$ is elaborated
	in the environment of the sequential declaration overlaid by the
	bindings produced by $D_1$. The resultant bindings are the ones
	produced by $D_1$ overlaid by those produced by $D_2$. 
\end{itemize}

\subsection*{Examples}

\begin{itemize}
\item 	{\bf const} {\it year} {\tt :} {\it int}\/ {\tt = 1991}
\item 	{\bf const} {\it yearPlusOne} {\tt :} {\it int}\/ {\tt =} {\it year} {\tt + 1}
\item 	{\bf const} {\it factOfFour} : {\it int} = {\it fact} {\tt (4)}
\item 	{\bf var} {\it x} {\tt :} {\it bool}{\tt \ :=\ }{\it false}
\item 	{\bf var} {\it y} {\tt :} {\it bool}{\tt \ :=\ }{\it not} {\tt (}{\it x}{\tt )}
\item 	{\bf varray} {\it vec} : {\bf array} [4] {\bf of} {\it int} {\tt := [3,5,9,0]}
\item 	{\bf proc} {\it inc} ({\bf var} {\it x}{\tt \ :\ }{\it int}{\tt )\ =\ }{\it x}{\tt  := }{\it x} {\tt + 1}
\item 	{\bf fun} {\it isGreaterThan} ($a$ : {\it int}, $b$ : {\it int}) : bool {\tt =} {\bf if} $a$ {\tt >} $b$ {\bf then} {\it true} {\bf else} {\it false} {\bf end}
\end{itemize}

\subsection{Commands}

A command is used to update variables. \specimen\ has six types
of commands: assignment, conditional, while, procedure call, block and
sequential.
 
\subsection*{Syntax}

\begin{spec}
\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 \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*} .

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

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

\subsection*{Semantics}

\begin{itemize}
\item	The assignment ``{\tt $I$ := $E$} is the simplest form of command.
	It assigns the value of expression $E$ to variable $I$.
	The expression is evaluated and the resultant value is
	stored in the cell bound to the variable identifier.

\item	The array assignment ``{\tt $I$[$E_1$] := $E_2$}'' updates
	a component of array $I$. The component is the one indexed
	by the result of evalution of $E_1$ which must be a positive
	integer.
	The primitive value resultant from the evaluation of $E_2$
	will be the new component.

\item	The conditional command ``{\bf if} $E$ {\bf then} $C_1$ {\bf else} $C_2$ {\bf end}'' is
	executed as follows: the expression $E$
	is evaluated; if the evaluation result is true then
	command $C_1$ is executed; otherwise command $C_2$
	is executed.

\item	The while command ``{\bf while} $E$ {\bf do} $C$ {\bf end}'' is executed as follows:
	(a) the expression $E$ is 
	evaluated; (b) if its value is true then the subcommand $C$ is 
	executed and then we start from step (a) again; otherwise,
	the while-command is terminated.

\item	A procedure call, ``{\bf call} $I$ {\tt (}$A${\tt )}'', 
	causes the execution of
	the procedure bound to identifier $I$.
	A parameter can be passed by value or by reference (\verb'var' formal).
	By value, ``{\tt $I$ ($E$)}'', the actual parameter expression $E$ 
	is evaluated and its value is bound to the formal paramenter;
	by reference, ``{\tt $I_1$ (var $I_2$)}'', the cell bound to variable
	$I_2$ is bound to the formal parameter.
	In the latter case the actual parameter must be a
	variable so the value  which is bound to the formal paramenter is a cell.
	Functions can be actual parameters of procedures.

\item	The block command ``{\bf local} $D$ {\bf in} $C$ {\bf end}'' is executed as follows.
	The declaration $D$ is elaborated. The command $C$ is then executed
	in the environment of the block command overlaid by the bindings
	produced by $D$.

\item	The sequential command ``{\tt $C_1$ ; $C_2$}'' is executed by first
	executing $C_1$ and then executing $C_2$.
\end{itemize}

\subsection*{Examples}

\begin{itemize}
\item 	{\it i} {\tt := 314}
\item 	{\it x} {\tt :=} {\it x} {\tt + 1}
\item 	{\bf if} $x$ = 0 {\bf then} $x${\tt \ := }$x$ {\tt + 1 }{\bf else} $x$ := $x$ {\tt - 1 }{\bf end}
\item 	{\bf while} $x${\tt \ =\ }{\it true} {\bf do} $x${\tt \ :=\ }{\it true and true} {\bf end}
\item	{\it vec}{\tt [}{\it t}{\tt ] := 345 ;} {\bf call} {\it p} {\tt (3 + 5)}
\item	{\bf local} {\bf var} {\it x} {\tt :} {\it int} {\tt := 2} {\bf in} {\it x} {\tt :=} {\it x} {\tt +} {\it y} {\bf end}
\end{itemize}

\subsection{Expressions}

The evaluation of an expression yields a value (an integer, a boolean,
or a function value).
Expressions are completely free of side effects.
Functions are first class: they can be passed as arguments to procedures
and functions and returned as a result of a function application.

\subsection*{Syntax} 

\begin{spec}
\settowidth{\wordlength}{Expression}
\tabset \makebox[\wordlength][r]{Expression} &=&
\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%'' \] .

\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*{Semantics}

\begin{itemize}
\item	A literal expression is one that does not need additional evaluation
	(it is already in a canonical form). \specimen\ has two types of literal
	expressions: boolean and integer.

\item	An identifier is an expression. Its evaluation gives the primitive value bound
	to it, in the case of a constant; or the function bound
	to it, in the case
	of a function identifier, respectively; or the content
	of the cell bound to it, in the case of a variable.

\item	The expression ``$I${\tt [}$E${\tt ]}'' is evaluated as follows:
	expression $E$ is evaluated and its result, a positive integer,
	say $n$, is used to access the $n$th component of array $I$ which
	is the result of the whole expression.

\item	The conditional expression ``{\bf if} $E_1$ {\bf then} $E_2$ {\bf else} $E_3$ {\bf end}'' is
	evaluates as follows: the expression $E_1$
	is evaluated; if the evaluation result is true then
	$E_2$ is evaluate and the result value is the result of the conditional
	expression; otherwise $E_3$ is evaluate and the result value is the
	result of the conditional expression.

\item	The function application, $I$ {\tt (}$E_1,\ldots,E_n${\tt )}, evaluates as follows:
	each parameter $E_i$ is evaluated and a list of arguments is formed with the
	resultant values. The function bound to $I$ is then applied to the list
	of arguments.
	Each occurrence of the formal parameter inside the function
	body is replaced by the correspondent resultant value; the function body is evaluated
	and its result is returned as the result of the function application.

\item	Constants, variables and functions can be defined locally using
	a let expression. (Procedures can also be defined locally but they
	cannot be used, so in practice there is no sense in defining them.)

\item	Conventional operations on booleans and integers are
	provided. Equality and inequality between primitive values
	are present.
\end{itemize}

\subsection*{Examples}

\begin{itemize}
\item 	{\tt true}
\item 	{\tt 4563738}
\item 	{\it x}
\item 	{\bf if} {\it tag} {\bf then} {\it process} ({\it tag}) {\bf else} {\it unprocess} ({\it tag}) {\bf end}
\item 	{\it g} (x + 3) - {\it f} (x - 3)
\item 	{\tt \verb+~+3}
\item 	{\tt 3 + 4 - 4 * 3 - 9}
\item 	{\tt (3 + 4) - (4 * 3 - 9)}
\end{itemize}


%\section{Static Semantics}
%
%Although we only specified the dynamic semantics, a static semantics
%could also be given.
%Notice that our dynamic semantics implicitly specifies a lot of what
%we expect to find in a static semantics. For example, the semantic equation
%for the {\tt +} operator
%%
%\begin{spec}
%\item[] apply-operator \[ ``\verb%+%'' \] = give sum (the integer\#1, the integer\#2) .
%\end{spec}
%%
%insists that its arguments are integers. Even for commands like
%%
%\begin{center}
%$x$ {\tt :=} $f$
%\end{center}
%%
%where $f$ is a function identifier, our formal description
%gives a correct semantics with respect to what we would
%expect from a static semantics for \specimen.

\begin{comment}
\section{Benchmark Programs}

Figures~\ref{fb-3}-\ref{fb-7} contains the benchmark programs
mentioned in Chapter~\ref{concl}. Program {\it factorial}
calculates the factorial of 10 using the {\it fact} recursive
procedure.
%
Program {\it fibonacci} (Figure~\ref{fb-4}) calculates
50 times the 22th element of the Fibonacci series.
%
Program {\it GCD} (Figure~\ref{fb-5}) calculates the
GCD of two positive integers using Euclid's algorithm.
%
Program {\it sieve} finds prime numbers using
Erathosthenes' sieve algorithm.
%
Finally, the {\it bubble} program sorts a sequence
of numbers using the bubble sort algorithm

\input{fb-3.tex}		% factorial

\input{fb-4.tex}		% fibonacci

\input{fb-5.tex}		% mcd

\input{fb-6.tex}		% sieve

\input{fb-7.tex}		% bubble
\end{comment}
