\section{Informal Description}
%
{\sc microSpecimen} is a simple imperative programming language. It has two types of
abstractions: procedures and functions. Functions are free of side effects,
although they can access non-local variables. Integers and
booleans are the only data types in the language. {\sc microSpecimen}
is a member of a group of four imperative languages used in research on
semantics-directed compiler generation.
(The others three are {\sc nanoSpecimen}, {\sc milliSpecimen} and
{\sc Specimen}.)
%
\subsection{Programs}
\subsection*{Syntax}
\begin{spec}
\item[] Program = \verb%program% Identifier \verb'=' Declaration \verb%in% Command \verb%end%
\end{spec}
%
\subsection*{Semantics}
A {\sc microSpecimen} program is a declaration (sequence)
followed by a command (sequence). The execution of
a program consists of the elaboration of the declaration and
then 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.
%
\subsection*{Examples}
We show below a {\sc microSpecimen} program that computes the
factorial of 4.
%
\begin{verbatim}
program fact4 =
    var x : int := 4;
    proc fact (var n : int) =
        local
            var temp : int = 1
        in
            while not (n = 1)
                do
                    temp := temp * n;
                    n := n - 1
                end;
            n := temp
        end
in
    fact (var x)
end
\end{verbatim}
%
The following program, which also computes the factorial of 9, uses a
function instead of a procedure. Note the recursive declaration of \verb+fact+.
%
\begin{verbatim}
program fact9 =
    var x : int = 9;
    fun fact n : int -> int = if n = 0 then 1 else n * fact (n - 1)
in
    x := fact x
end
\end{verbatim}
%
%
\subsection{Declarations}
%
\subsection*{Syntax}
\begin{spec}\tabset Declaration &=&
\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*{Semantics}
Declarations allow the programmer to make bindings. {\sc microSpecimen} has four
types of declarations (bindings): constant, variable, procedure and
function declaration. Procedures and functions declarations can be 
recursive.

A constant declaration binds an identifier to a constant value. If possible,
this value can be evaluated at compile-time.

A variable declaration binds an identifier to a cell. The contents
of the cell is the result of the evaluation of the expression.

A procedure declaration binds an identifier to a procedure. A procedure is 
a command abstraction. Zero or one formal parameter can
be defined in the procedure declaration. The body of a procedure is just
a command. No result is returned, a procedure works
by its side effects only.

A function declaration binds an identifier to a function. A function
is an expression abstraction. All {\sc microSpecimen} functions are unary
(have just one argument). The body of a function is just an
expression. Functions always return a value.
%
\subsection*{Examples}
\begin{itemize}
\item \verb'const year : int = 1991'
\item \verb'const yearPlusOne : int = year + 1'
\item \verb'const factOfFour : int = fact 4'
\item \verb'var x : bool = false'
\item \verb'var y : bool = not x'
\item \verb'proc inc (var x : int) = x := x + 1 end'
\item \verb'fun isTrue b : bool -> bool = if b then true else false'
\end{itemize}
%
\subsection{Commands}
A command is used to update variables. {\sc microSpecimen} has five types
of commands: assignment, conditional, while, procedure call, and block.
% 
\subsection*{Syntax}
\begin{spec}\tabset Proc Argument &=&
\item[] \tab Command &=&
        Identifier \verb%:=% Expression \| \=
        \verb%if% Expression \verb%then% Command \verb%else% Command \| \=
        \verb%while% Expression \verb%do% Command {\verb+end+} \| \=
        \verb%local% Declaration \verb%in% Command \verb%end% \| \=
        Identifier \verb'()' \| \=
        Identifier \verb%(% Proc Argument \verb%)% \| \=
        Command \verb%;% Command
%
\item[] \tab Proc Argument &=& Expression \| \=
                           \verb'var' Identifier
\end{spec}
%
\subsection*{Semantics}
The assignment is the simplest form of a command. It assigns the value
of an expression
to a variable. The expression is evaluated and the resultant value is
assigned to the cell bound to the variable (identifier).

The conditional command is executed as follows: the expression
is evaluated; if the evaluation result is true then the \verb'then' branch
command is executed otherwise the \verb'else' branch command is executed.

The while-command is executed as follows: (a) the expression is 
evaluated; (b) if its value is true then the subcommand is 
executed and then we start from step (a) again; else, if the value is false,
the while-command is terminated.

A procedure call, $P$\verb'('$A$\verb')', causes the execution of the procedure
bound to $P$. A parameter can be passed
by value or by reference (\verb'var' formal). By value, $P$\verb'('$E$\verb')',
the actual parameter 
is evaluated and its value is bound to the formal argument;
by reference, $P$\verb'(var '$I$\verb')', the
actual parameter is evaluated and its l-value is bound to the formal
parameter. In this case the actual parameter must be a variable and
the value passed is a cell. Neither procedures nor functions can be
passed as parameters. 
%
\subsection*{Examples}
\begin{itemize}
\item \verb'i := 314'
\item \verb'x := x + 1'
\item \verb'if x = 0 then x := x + 1 else x := x - 1'
\item \verb'while x = true do x := true and true end'
\item \verb'if tag then process(true) else process(false)'
\end{itemize}
%
\subsection{Expressions}
Expressions are evaluated yielding a value (an integer or a boolean).
Expressions are completely free of side effects.
%
\subsection*{Syntax} 
\begin{spec}\tabset Argument &=&
\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*{Semantics}
A literal expression is one that does not need additional evaluation
(it is still in normal form). {\sc microSpecimen} has two types of literal
expressions: boolean and integer.

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

The conditional expression has a semantics very similar to the
conditional command, except that the \verb'then' and \verb'else' branches are
expressions instead of commands.

The function application, $I E$, evaluates as follows: $E$ is
evaluated; each occurrence of the formal parameter inside the function
body is replaced by the resultant value; the function body is evaluated
and its result is returned as the result of the function application.

Operators...
%
\subsection*{Examples}
\begin{itemize}
\item \verb'true'
\item \verb'45637384746'
\item \verb'x'
\item \verb'if tag then process tag else un process tag'
\item \verb'g (x + 3) - f (x - 3)'
\item \verb'- 3'
\item \verb'3 + 4 - 4 * 3 - 9'
\item \verb'(3 + 4) - (4 * 3 - 9)'
\end{itemize}
%
\subsection{Types}
%
{\sc microSpecimen} has only two types: \verb'int' and \verb'bool'. Types of all
constants, variables, procedures and functions must be explicitly declared.
%
\subsection{Types and Contextual Constraints}
Although we only specified the dynamic semantics (a static semantics
will be given later), we are going to state informally some types
and contextual constraints that help the user to write valid {\sc microSpecimen}
programs.
