% (C) Copyright International Business Machines Corporation 23 January
% 1990.  All Rights Reserved. 
%  
% See the file USERAGREEMENT distributed with this software for full 
% terms and conditions of use. 
% File: quick-ref.tex
% SCCS Info: @(#)quick-ref.tex	1.2 3/3/92

% A quick-reference guide to the Hermes language

\documentstyle[fullpage,twoside]{article}

\def\theenumi{\Roman{enumi}}
\def\theenumii{\Alph{enumii}}
\def\labelenumii{\theenumii.}
\def\theenumiii{\arabic{enumiii}}
\def\theenumiv{\roman{enumiv}}
\makeatletter
\def\p@enumii{\theenumi.}
\def\p@enumiii{\p@enumii\theenumii.}
\def\p@enumiv{\p@enumiii\theenumiii.}
\def\enumlabel{}
\def\setenumlabel{\xdef\enumlabel{\ifcase\@enumdepth\or
  \theenumi
  \or\p@enumii\theenumii
  \or\p@enumiii\theenumiii
  \or\p@enumiv\theenumiv\fi}}
\makeatother
\begin{document}

\makeatletter
\pagestyle{headings}
\def\@evenhead{\rm\thepage{} \sl\enumlabel\hfil\setenumlabel}
\def\@oddhead{\hfil\sl\enumlabel{} \rm\thepage\setenumlabel}
\def\ps@myplain{\ps@plain\setenumlabel}
\makeatother
\thispagestyle{myplain}

\centerline{\bf Hermes in \pageref{lastpage} Pages}

\bigskip

\begin{enumerate}
\item Program Skeletons
\begin{enumerate}
\item Definitions Module named {\bf foo}
\begin{verbatim}
foo: using (...)        -- fill in names of imported def modules
definitions
  ...                   -- fill in type definitions
end definitions
\end{verbatim}
\item Program Module named {\bf foo}\label{process-module-skeleton}
\begin{verbatim}
foo: using (...)        -- fill in names of imported def modules
  linking (...)         -- fill in names of statically linked process modules
process (...)           -- fill in declaration of init port, e.g. process(q: mainQ)
  declare
    ...                 -- fill in program-wide variable declarations
  begin
    ...                 -- fill in program statements
  on (...)              -- fill in exception name(s)
    ...                 -- fill in statements of exception handler
  on exit(...)          -- fill in exit name(s)
    ...                 -- fill in statements of exit handler
  on ...                -- additional exception/exit handlers
end process
\end{verbatim}
\end{enumerate}
\item Type Definitions\par A {\em type definition} creates a new type,
which can thereafter be used in variable declarations (see
item~\ref{declarations} below).  Variables of two different types are
never interchangeable, even if they are structurally identical.  For
example, if two integer types, {\bf apple} and {\bf orange} have been
defined, then a variable of type {\bf apple} can never be added to or
compared with a variable of type {\bf orange}.

\begin{enumerate}
\item Scalar Types
\begin{enumerate}
\item Integer Types\par New integer types are defined
readily:\footnote{The {\tt predefined} definitions module defines an
integer type named {\tt integer}.}
\begin{verbatim}
apple: integer;
orange: integer;
\end{verbatim}

\item Real Types\par A real type definition includes an accuracy
constraint, represented as a fraction providing (roughly) the maximum
relative error allowed for operations yielding values of the
associated type.
\begin{verbatim}
imprecise: real of accuracy 1/10;
medium: real of accuracy 1/1000;
precise: real of accuracy 1/1000000;
\end{verbatim}

\item Enumeration Types\par An enumeration type defines a collection
of named literals (delimited by single-quotes) that make up the set of
possible values for variables of the type.  If the type is {\em
ordered}, then values of the type can be compared according to the
order in which they are listed in the type definition.  Ordered
enumeration values can also be {\em converted} to other scalar types:
the converted value of the first enumeration value is zero, the value
of the second is one, and so on.

The {\tt predefined} module defines two commonly used enumeration
types: {\tt char} and {\tt empty}.  {\tt Char} is an ordered
enumeration containing one value named for each of the 128 ASCII
characters.  Values corresponding to control characters have names
with more than one character, such as {\tt 'BS'} in position 8 (the
``Backspace'' or ``Control-H'' character).  {\tt Empty} is a
surprisingly useful enumeration type that includes zero named
literals.  A variable of this type can never be initialized.  It is
frequently used as the data part of variant components for which no
data is really appropriate.  See examples of its use in the {\tt
predefined} definitions module.

\begin{verbatim}
colors: enumeration ('red', 'black', 'green', 'yellow');
weekdays: ordered enumeration ('sunday', 'monday', 'tuesday',
  'wednesday', 'thursday', 'friday', 'saturday');
\end{verbatim}
\item Boolean Types\par A boolean type definition defines two named
literals, one to stand for {\em true} and another to stand for {\em
false}.\footnote{The {\tt predefined} definitions module defines a
boolean type named {\tt boolean} with named literals {\tt 'true'} for
{\em true} and {\tt 'false'} for {\em false}.}
\begin{verbatim}
switch: boolean (true: 'on', false: 'off');
screwyBoolean: boolean (false: 'true', true: 'false');
\end{verbatim}
\item Nominal Types\par A value of a nominal type can be copied and
compared for equality with other nominal values.  New nominals are
created with the {\tt unique} operation (see item~\ref{unique}).  Two
nominals are equal if and only if they are copies of each other.
Nominals are thus useful, e.g., as unique identifiers for things that
will be stored in tables and must be retrieved later.
\begin{verbatim}
graphNodeID: nominal;
connectionID: nominal;
\end{verbatim}
\end{enumerate}
\item Aggregate Types
\begin{enumerate}
\item Records\par A record type includes named components, each of a
specific type.  A variable of a record type is a container that can
hold one value for each component.
\begin{verbatim}
address: record (
  line1: charstring,
  line2: charstring,
  line3: charstring,
  city: charstring,
  state: state,         -- an enumeration contiaining, e.g., 'NY'
  zip: integer
);
\end{verbatim}
\item Variants\label{variant-typedef}\par A variant type, like a
record type, includes named components, each of a specific type.
Unlike with records, a variable of a variant type is a container that
can hold a value for at most one of the components at any given time.
Each component is associated with one of the values in an enumeration
type associated with the variant type.  Also associated with each
component is the {\em typestate} (see item~\ref{typestates}) that the
component will be in whenever the containing variant is {\em hidden}
(see
\label{lisptypeexample}
item~\ref{hide}).
\begin{verbatim}
lispValue: variant of lispType (
  'pair' -> pair: lispPair {full},
  'atom' -> name: charstring {full},
  'nil' -> nil: empty {}
);

lispType: enumeration ('pair', 'atom', 'nil');
lispPair: record (
  car: lispValue,
  cdr: lispValue
);
\end{verbatim}
\item Tables\label{table-typedef}\par A variable of a table type can
hold a homogeneous collection of values.  Each element in the table
must be of the type and in the typestate appearing in the table type
definition.  Any program that attempts to insert into a table a value
whose typestate is too low will be rejected by the compiler.  If a
value to be inserted has a higher typestate than that appearing in the
table definition, it will be coerced down prior to the insertion (see
item~\ref{coercions} for a discussion of coercions).

A table type definition may specify that tables are {\em ordered}.
This simply means that the elements are maintained in some ordering
relative to each other.  It makes sense to speak of the ``first
element'' in an ordered table; no such concept applies to unordered
tables.  The order of the elements in an ordered table has nothing to
do with any notion of sortedness.  Each element assumes a position
relative to the other table elements when it is first inserted into
the table (that position is determined by the manner in which the
insertion is performed).  The relative position of this element with
respect to any other table element thereafter remains unchanged until
one or the other is removed from the table.

A table type definition may also specify one or more {\em keys}.  Each
key represents some specified portion of a table element.  Keyed
table types disallow two elements that are identical with respect to
any of the declared keys from ever coexisting in the same table.

Here are types to represent a simple collection of integers, and a
simple collection of those collections.
\begin{verbatim}
integerBag: table of integer {init};
integerBags: table of integerBag {init};
\end{verbatim}
Here's how the {\tt charstring} type (from the {\tt predefined}
definitions module), in which it's important for characters to
maintain their relative positions, is defined:
\begin{verbatim}
charstring: ordered table of char {init};
\end{verbatim}
Here's how one might define types to represent a graph:
\begin{verbatim}
nodeID: nominal;
node: record (
  id: nodeID,
  data: nodeData
);
nodeData: record (
 ...
);
edge: record (
  from: nodeID,
  to: nodeID
);
nodeSet: table of node {full} keys (id);
edgeSet: table of edge {full} keys (*);
graph: record (
  nodes: nodeSet,
  edges: edgeSet
);
\end{verbatim}
The key specification for {\tt nodeSet} prevents two nodes with the
same {\tt id} value from ever appearing in the same {\tt nodeSet}
table.  The key specification for {\tt edgeSet} prevents two identical
edges from ever appearing in the same {\tt edgeSet} table.  In the
following, {\tt linearGraph} describes graphs that can only contain
disjoint components that are simple cycles or linear sequences of
nodes.  This is because a variable of type {\tt linearEdgeSet} can
never contain two edges with the same source or two edges with the
same destination.
\begin{verbatim}
linearEdgeSet: table of edge {full} keys (from) (to);
linearGraph: record (
  nodes: nodeSet,
  edges: linearEdgeSet
);
\end{verbatim}
\end{enumerate}
\item Communication Types\par Most commonly, when an interface is
required to support calls from one process to another, the interface
definition comes in the form of three related type definitions: a {\em
callmessage} type that defines the arguments of the call, their types,
and typestate requirements at return points; an {\em inport} type that
defines typestate requirements at call points; and an {\em outport}
type.  Calls are made on values of the outport type and are received
on values of the inport type.  Although it is possible to define
multiple inport types for the same callmessage type, and multiple
outport types for the same inport type, this is uncommon in practice.

\begin{enumerate}
\item Callmessages\label{callmessage-typedef}\par A variable of a
callmessage type is a container that can hold the arguments of a call
currently being made by some other process.  A callmessage value can
be returned, meaning that the arguments are moved back into variables
owned by the calling process, and that process is resumed.  The
process that returns a callmessage need not be the one that originally
returned it, and a process may receive multiple callmessages and
return them in any desired order.  Callmessage type definitions have
the following structure:
\begin{verbatim}
cmType: callmessage (
    ...                 -- fill in component declarations, as for records
  )
  constant (...)        -- fill in components that are constant on this interface
  exit {...}            -- fill in typestate for normal return
  minimum {...}         -- fill in minimum typestate for this callmessage
  exception xxx {...}   -- fill in typestate for xxx exception return
  exception ...         -- other exception return specifications
  ;
\end{verbatim}
Some of the features in the above skeleton are:
\begin{itemize}
\item {\tt constant (...)}\\This portion of the definition may be
omitted altogether.  If it is present, each of the callmessage
components listed will be considered unmodifiable.  Any program that
could potentially modify a constant component of a callmessage will be
rejected by the compiler.
\item {\tt exit \{...\}}\\This portion of the definition is required.
It defines the typestate that all the callmessage components will be
in whenever the callmessage is returned without an exception.  Any
program that attempts to return a callmessage with a component in a
lower typestate than given here will be rejected by the compiler.  If
a program attempts to return a callmessage when a component's
typestate is higher than specified here, the component will be coerced
down to the specified typestate before the return (see
item~\ref{coercions}).
\item {\tt minimum \{...\}}\\This portion of the definition may be
omitted.  If present, it specifies the lowest typestate that will be
allowed for each callmessage component.  If any program attempts to
perform an operation that would lower a component of an initialized
callmessage below its minimum typestate, the program will be rejected
by the compiler.  If the minimum typestate is not specified, it
defaults to one in which each constant component is fully initialized
and all other components are uninitialized.
\item {\tt exception xxx \{...\}}\\This portion of definition may
appear zero, once, or many times (the exception names, {\tt xxx} in
this case, must all be different).  A program owning a callmessage of
the defined type can return the callmessage with the named exception
(see item~\ref{return-exception}).  The typestate appearing in the
exception specification indicates what typestate each component will
be in if the associated exception return is ever performed.  This
typestate is enforced by the compiler in the same manner as is the
normal exit typestate for normal returns.
\end{itemize}
An exception named {\tt Discarded} is automatically defined for every
callmessage; its associated typestate is the callmessage's minimum
typestate.  Discarding a callmessage is exactly the same as returning
it with its {\tt Discarded} exception.
\item Inports\label{inport-typedef}\par A variable of an inport type
is capable of receiving messages of an associated message type.  Most
commonly, the message type is some callmessage type, but this is not
required.  The inport definition specifies the minimum typestate
required of any message sent to the inport.  If a program attempts to
send (via a {\tt call} or {\tt send} operation) a message to an inport
when the message's typestate is below that required in the inport
definition, the program will be rejected by the compiler.  If the
message typestate is too high, it will be coerced down prior to the
{\tt call}/{\tt send}\footnote{Constant components of callmessages are
an exception: they are never coerced down.}
\begin{verbatim}
foo: callmessage (...);
fooQ: inport of foo {full};
charQ: inport of char {init};
\end{verbatim}
\item Outports\par A variable of an outport type can be used to transmit
messages to a connected inport of an associated inport type.  If the
message type associated with that inport type is a callmessage type,
then messages can be sent on the outport via either the {\tt call} or
{\tt send} statement.  Otherwise, only {\tt send} can be used.
\begin{verbatim}
fooFn: outport of fooQ;
charPort: outport of charQ;
\end{verbatim}
Note that outports are first-class values: they can be sent to other
processes, copied, stored in variables and tables, and so on.  The
only way a process can communicate with another process is via an
outport connected to an inport owned by that other process.
\end{enumerate}
\item Polymorph Types\par A variable of a polymorph type is a
container for values of other types (see the {\tt wrap} and {\tt
unwrap} statements, items~\ref{wrap} and~\ref{unwrap}).  They provide
a way to defer type and typestate checking until run-time, allowing
things like heterogeneous tables, polymorphic interfaces,
etc.\footnote{The {\tt common} definitions module defines a polymorph
type named {\tt polymorph}.}
\begin{verbatim}
arbitraryValue: polymorph;
anything: polymorph;
\end{verbatim}
\end{enumerate}
\item Declarations\label{declarations}\par Every variable used in a
Hermes program must be declared, either in the outer declarations list
appearing in the program module skeleton, in or a block
statement.\footnote{There are also some constructs that implicitly
declare additional variables, such as selectors.} In addition
component declarations appear in record, variant, and callmessage type
definitions.  In all cases a declaration consists of a variable name
and a typename separated by a colon.  Some examples are:
\begin{verbatim}
x: integer;
foo_table: fooTable;
myBool: private!boolean;
\end{verbatim}
The typename appearing in a declaration must correspond to the name of
a type defined in one of the definitions modules imported by the
module in which the declaration appears.\footnote{The {\tt predefined}
definitions module is implicitly imported by every module, and need
never be listed in a {\tt using(...)} list.} If more than one imported
module contains a type with the same name, a {\em qualified} typename,
consisting of the module name and the typename separated by an
exclamation mark ({\tt !}), must be used to disambiguate the
reference.

In Hermes, unlike in many other language, a variable declaration is
not allowed to ``hide'' a declaration for a variable of the same name
appearing in some outer block.  For example, a program containing the
following would be rejected by the Hermes compiler:
\begin{verbatim}
block declare
  x: integer;
begin
  ...
  block declare
    x: charstring;
  begin
    ...
  end block;
  ...
end block;
\end{verbatim}
\item Statements and Expressions
\begin{enumerate}
\item Assignment\label{assignment}\par Two forms of assignment are
provided.  If variables are thought of as boxes that can hold values,
the {\em move} operator ({\tt <-}) takes the value out of one box and
drops it into another, leaving the original box empty (i.e. the source
variable is left uninitialized); the {\em copy} operation ({\tt :=})
makes a copy of the value found in one box and puts the copy into the
other box, leaving the value in the first box undisturbed.  Here are
examples:
\begin{verbatim}
x <- y;                 -- y becomes uninitialized
x := y;                 -- y retains its original value
x <- 5 * z;             -- there is an unnamed temporary variable created by
                        -- the compiler to hold the value 5 * z; this temporary
                        -- variable becomes uninitialized with this statement
x := 5 * z;             -- the temporary variable retains its value (this is
                        -- not generally very useful, though harmless)
\end{verbatim}
\item Arithmetic\par The following binary operators all operate on the
numeric types (all integer and real types).  All operands, including
the result, must be of the same type (use the {\tt convert of}
operation, described in item~\ref{convert}, if you need to mix operand
types).
\begin{itemize}
\item {\tt +} (Addition)
\item {\tt -} (Subtraction, also negation as a unary operator)
\item {\tt *} (Multiplication)
\item {\tt /} (Division, truncating toward zero with integer operands).
\end{itemize}
The following binary operators operate on all integer types.  Given
two operand values $a$ and $b$, each computes a value $c$ such that
$|c| < |b|$ and there exists an integer $n$ with $a = c + nb$.  The
two operands differ in how they determine the sign of the result $c$.
\begin{itemize}
\item {\tt rem}: The result value $c$ is chosen to be zero or to have
the same sign as $a$.
\item {\tt mod}: The result value $c$ is chosen to be zero or to have
the same sign as $b$.
\end{itemize}
\item Comparisons\par The following comparison operators operate on
any Hermes types and can produce a result of any boolean type.  The
source operands must be of the same type.  The type of the result
operand is determined from context (e.g. if the result is assigned to
a variable of type {\tt predefined!boolean}, that will be the type of
the result, rather than some other boolean type).
\begin{itemize}
\item {\tt =} (test for equality)
\item {\tt <>} (test for inequality)
\end{itemize}
The following comparison operators can be applied to any ordered
scalar type (integer types, real types, and ordered enumeration
types).  They can yield a result of any boolean type.
\begin{itemize}
\item {\tt <} (less than)
\item {\tt >} (greater than)
\item {\tt <=} (less than or equal to)
\item {\tt >=} (greater than or equal to)
\end{itemize}
\item Logical Operations\par The following operators can be applied to
any boolean type and yield a result of the same boolean
type:\footnote{Although the {\tt convert of} operator cannot be
applied to boolean types, booleans can easily be converted using the
following trick.  Suppose, for example, that a variable {\tt pb} of
type {\tt predefined!boolean} needs to be stored into a variable {\tt
mb} of type {\tt mybool}.  The following would do the trick:\par
\centerline{\tt mb <- pb = 'true';}}
\begin{itemize}
\item {\tt and} (binary operator yields {\em true} iff both source
operands are {\em true})
\item {\tt or} (binary operator yields {\em false} iff both source
operands are {\em false})
\item {\tt not} (unary operator yields {\em true} if the source
operand is {\em false}; otherwise it yields {\em false})
\end{itemize}
\item Scalar Conversions\label{convert}\par The {\tt convert of}
operator converts among variables of ordered scalar types (integers,
reals, and ordered enumerations).  In many languages, this operation
is automatically inserted by the compiler and is known as a {\em type
coercion}.  In Hermes it must be explicitly programmed.  Assume {\tt
i}, {\tt r}, and {\tt oe} are variables of some integer type, real
type, and ordered enumeration type, respectively.  Following are the
possible conversions:
\begin{itemize}
\item {\tt i <- convert of r;}\\The integer value nearest the value of
{\tt r} is stored in {\tt i} (if there are two equally close integers,
e.g. if {\tt r} contains the value 1.5, either integer may be
chosen).
\item {\tt i <- convert of oe;}\\The position of the current value of
{\tt oe} in the list of enumeration values appearing in the
corresponding type definition, is stored in {\tt i}.  The first
enumeration value in the list is converted to zero, the next is
converted to one, and so on.
\item {\tt r <- convert of i;}\\The safe number in the domain of {\tt
r} nearest the current value of {\tt i} is stored in {\tt r}.  If
there are two equally close safe numbers, either may be chosen.
\item {\tt r <- convert of oe;}\\The value in {\tt oe} is converted to
an integer as described above, then that value is converted to a safe
number and stored in {\tt r}.
\item {\tt oe <- i}\\The enumeration value appearing in the position
given by the value of {\tt i}, in the list of enumeration values
given in the enumeration type definition, is stored in {\tt oe}.
\item {\tt oe <- r}\\The value in {\tt r} is converted to an integer
as described above, then that value is converted to an enumeration
value.
\end{itemize}
The {\tt convert of} operator can also be used to convert between two
integer types, two real types, or two ordered enumeration types, as
well.  The integer-to-integer case cannot result in a value change.
For the real-to-real case, because the two safe number domains may not
be identical, the value may actually change: the safe number in the
target domain that is closest to the source value is chosen.  For
enumeration-to-enumeration conversions, the source value is first
converted to an integer, then that value is converted to a value in
the destination enumeration type.
\item Table Operations
\begin{enumerate}
\item Selectors\par Many of the Hermes table manipulation operations
make use of a common construct called a {\em selector}, which serves
to identify which elements of a table are to participate in the
operation.  The selection criterion can be anything involving the
values of the table elements or, in the case of ordered tables, their
positions within the table.  A selector has the following general
form, where {\tt t} is the table variable on which the operation is
being performed, and {\tt x} is a variable representing an element of
the table.
\begin{verbatim}
x in t where (...)
\end{verbatim}
The variable {\tt x}, which is automatically declared to be whatever
type is required to hold elements of {\tt t}, can be used within the
selector expression.\footnote{But remember that since no variable
declaration can hide another, {\tt x} is not allowed to be a variable
that is declared in some outer scope containing the selector.}  The
selector operates by applying the selector expression to each table
element.  The elements for which the selector expression evaluates to
{\em true} will participate in the table operation; the others will
not.
\item Creating Tables\par A new, empty table is created with the {\tt
new} statement:
\begin{verbatim}
new t;
\end{verbatim}
\item Inserting New Elements\par The {\tt insert} statement is used to
insert a new element into a table.  The element value is {\em moved}
into the table, i.e. the variable from which it came is left
uninitialized.  If the table is ordered, the position at which the new
element is inserted may be specified; it defaults to the end of the
table.
\begin{verbatim}
insert x into t;
insert y into t at 0;
\end{verbatim}
The {\tt merge} statement can be used to add all the elements of one
table into another table of the same type.  As with {\tt insert}, the
variable originally holding the merged table is left uninitialized.
If the tables are ordered, the position in the destination table where
the first source element is inserted may be specified; it defaults to
the end of the table.
\begin{verbatim}
merge t1 into t2;
merge t2 into t3 at pos - 1;
\end{verbatim}
\item Removing Elements\label{remove}\par The {\tt remove} statement
applies a selector to a table and removes one of the selected
elements, leaving it in the indicated variable.  If the table is
ordered, the first selected element is removed; otherwise the choice
is unpredictable.
\begin{verbatim}
remove redItem from x in t where (x.color = 'red');
remove smallAndShort from y in t where (y.area < 100 and y.width > y.height);
\end{verbatim}
The {\tt extract} statement applies a selector to a table and removes
{\em all} the selected elements from that table.  They are all
collected to form another table of the same type.  If the table is
ordered, the extracted elements will be in the same order relative to
each other in the extract as they were in the original table.
\begin{verbatim}
extract nonCircles from x in t where (x.shape <> 'circle');
\end{verbatim}
\item Copying Out Elements\label{selector-expression}\par A selector
used by itself as an expression evaluates to a {\em copy} of one of
the selected table elements; the table remains unchanged.  If the
table is ordered, the first selected element is copied out.  Otherwise
the choice is unpredictable.
\begin{verbatim}
redItem <- x in t where (x.color = 'red');
smallAndShort <- y in t where (y.area < 100 and y.width > y.height);
\end{verbatim}
The {\tt every of} operator applies a selector and then builds a new
table containing {\em copies} of all the selected elements; the
original table remains unchanged.  If the table is ordered, the copied
elements will appear in the same relative order in the new table as
they did in the original.
\begin{verbatim}
nonCircles <- every of x in t where (x.shape <> 'circle');
\end{verbatim}
\item Inspecting Elements\label{inspect-table}\par The {\tt inspect}
selector statement applies a selector to a table and then executes a
body of code with the selector variable containing a {\em constant}
copy of one of the selected table elements.  The table remains
unchanged, unless some statement within the body of the {\tt inspect}
statement changes it.  In any case, the element variable cannot be
changed within the statement body.  If the table is ordered, the first
selected table element will be inspected.  Otherwise the choice is
unpredictable.
\begin{verbatim}
inspect redItem in t where (redItem.color = 'red') begin
  ...                   -- use, but do not change, the value of redItem
end inspect;
\end{verbatim}
The {\tt for ... inspect} statement applies a selector to a table and
then inspects each selected element in turn.  Within the body of the
{\tt for  ... inspect}, the inspected element cannot be modified.  The
table may be modified, however no modifications made to the table
within the statement body will affect the sequence of elements
inspected.  In particular, removing a selected element before it is
inspected will not prevent its being inspected when its turn arrives.
If the table is ordered, the elements will be inspected in the order
in which they appear in the table; otherwise the order is
unpredictable.
\begin{verbatim}
for redItem in t where (redItem.color = 'red') inspect
  ...                   -- use, but do not change, the value of redItem
end for;
\end{verbatim}
\item Quantifiers\par The {\tt forall of} operations test to see
whether a selector results in all of the table elements being selected
(i.e. they all satisfy the selector expression).  The {\tt exists of}
determines whether there is at least one selected element.
\begin{verbatim}
allPositive <- forall of i in t where (i > 0);
notAllPositive <- exists of i in t where (i <= 0);
\end{verbatim}
\item Miscellaneous Table Operations
\begin{enumerate}
\item Table Size\par The {\tt size of} operator returns the number of
elements in a table:
\begin{verbatim}
n <- size of t;
\end{verbatim}
\item Position of an Element\label{position-of-selector}\par The {\tt
position of} operation can be used only with ordered tables.  It can
be applied to a selector, to a selector variable within a selector
expression, or to an inspect variable inside the body of an {\tt
inspect} or {\tt for ... inspect} statement.

When {\tt position of} is used with a selector, the selector is
applied to the table and the position of the first selected element is
returned (the position of the first element in a table is always
zero).
\begin{verbatim}
firstPeriod <- position of c in string where (c = '.');
\end{verbatim}
{\tt Position of} can be used within selector expressions to obtain
the position within the table of the element to which the selector
expression is currently being applied.
\begin{verbatim}
remove first from x in t where (position of x = 0);
everyOtherElement <- every of x in t where (position of x mod 2 = 0);
\end{verbatim}
{\tt Position of} can also be applied to the inspect variable within
an {\tt inspect} or {\tt for ... inspect} statement.  It yields the
position within the table of the element currently being inspected
{\em not counting any changes that may have been made to the table
within the body of the statement}.
\begin{verbatim}
inspect max in t where (not exists of x in t where (x > y)) begin
  maxPos <- position of max;
end inspect;

new dotPositions;
for c in string where (c = '.') inspect
  insert position of c into dotPositions;
end for;
\end{verbatim}
\end{enumerate}
\item Selector Abbreviations\par An alternate syntax for selectors is
available in certain contexts.  They are as follows:
\begin{itemize}
\item {\tt t[]}\par This is equivalent to the selector expression {\tt
x in t where ('true')}.  It selects every element of the table.
Examples:
\begin{verbatim}
first <- t[];                   -- assuming t is ordered
nonEmpty <- exists of t[];      -- comparing size to zero tests this too
\end{verbatim}
\item {\tt t[{\em pos}]}\par If {\tt t} is an ordered table, {\em pos}
must be an integer valued expression, and the selector is equivalent
to {\tt x in t where (position of x = {\em pos})}.  Example:
\begin{verbatim}
fifth <- t[4];                  -- remember first position is zero
\end{verbatim}
\item {\tt t[{\em expr}, {\em expr}, $\ldots$]}\par The number of
expressions must correspond to the number of components listed in
exactly one of the key specifications in the table type definition.
This selector is an abbreviation of one in which each key component
must equal the value of the corresponding expression.  If the table is
ordered, this abbreviation may only be used for keys with more than
one component, since otherwise the positional interpretation described
above is used.  If there are multiple key sets with the right number
of components, this syntax is ambiguous and cannot be used; the
full-blown selector expression must be used in those cases.  Examples:
\begin{verbatim}
employeeRec <- employeeTable[ssn];      -- must not be an ordered table
employeeRec <- employeeTable["Doe", "John"]; -- keyed on last and first names
\end{verbatim}
\end{itemize}
Note that both the positional and keyed interpretations result in
selectors that are capable of selecting at most one table element.  For
positional selectors, this is clear because only one element can
occupy any given position.  For the keyed interpretation, this is
still true because no two table elements can be identical with respect
to any of the key specifications for the table.
\end{enumerate}
\item Records and Variants
\begin{enumerate}
\item Creating Records\par A new record is created via the {\tt new}
operation.  None of the record components is given a value as the
result of this operation, so after the {\tt new} operation they are
all uninitialized.  Record components are initialized individually
just like any other variables:
\begin{verbatim}
new employeeRec;
employeeRec.line1 <- getInputLine("Address Line 1: ");
employeeRec.line2 <- getInputLine("Address Line 2: ");
...
\end{verbatim}
\item Creating and Destroying Variants\par A variant is initialized
and placed in one its cases via the {\tt unite} operation.  For
example, the following sequence would create a value of type {\tt
lispValue} (see item~\ref{lisptypeexample}) representing the list {\tt
(xxx)}:
\begin{verbatim}
new lispPair;
unite lispPair.car.name from "xxx";
unite lispPair.cdr.nil from empty;
unite lispValue.pair from lispPair;
\end{verbatim}
The first operand in a {\tt unite} operation is one of the components
of the variant variable being initialized.  The second operand is an
expression which must evaluate to a value of the type and in a
typestate at least as high as indicated in the declaration of that
component in the variant's type definition.  The expression's
typestate may be higher than required, and if so, it will not be
coerced down as a result of the {\tt unite} operation (but see the
{\tt hide} operation below).
\item Hiding and Revealing Variants\label{hide}\par The {\tt hide} operation
causes the compiler to ``forget'' which case a variant is in.  No
reference to the corresponding variant component may thereafter be
made until a {\tt reveal} statement has been performed to reestablish
the variant's case.
\begin{verbatim}
hide lispValue;
insert lispValue into t;
...
remove lispValue from v in t where (...);
reveal lispValue.pair;
\end{verbatim}
The example above illustrates on of the reasons for hiding variants,
namely so they can be stored in a table with other variants that are
not necessarily in the same case.  The element typestate appearing in
the type definition for such a table will necessarily omit any
restrictions on the case of the variant values it contains (else it
would only be capble of holding values in the indicated case).
Therefore, any known case information must be coerced away prior to
inserting a new value into the table.  Similar remarks apply to
interfaces that allow variants in unknown cases to be transmitted.
Note that in both cases, the {\tt hide} statement will be inserted
automatically by the compiler in order to coerce away the case
information as needed; the {\tt hide} statement rarely need be coded
explicitly.
\item Querying the Case of a Variant\par The {\tt case of} operation
applied to a variant (hidden or revealed) will return the enumeration
value corresponding to the case in which the variant currently exists.
The following example illustrates a common paradigm that uses this
operation to handle a variant value according to its case:
\begin{verbatim}
select case of lispValue
  where ('pair')
    reveal lispValue.pair;
    ...                 -- handle the case of a pair
  where ('atom')
    reveal lispValue.name;
    ...                 -- handle the case of an atom
  where ('nil')
    reveal lispValue.nil;
    ...                 -- handle the case of a nil value
  otherwise
    -- can't happen
end select;
\end{verbatim}
Note in the above that the compiler is not intelligent enough to
figure out the necessary {\tt reveal} statements for you.  Perhaps in
some future release...
\end{enumerate}
\item Polymorphs
\begin{enumerate}
\item Wrapping and Unwrapping Values\label{wrap}\label{unwrap}\par An
arbitrary value can be wrapped in a polymorph by means of the {\tt
wrap} statement:
\begin{verbatim}
wrap x as arb;
\end{verbatim}
The resulting polymorph value ({\tt arb} in the example) contains the
wrapped value, as well as its type and typestate.  The variable whose
value was wrapped ends up unitialized.

Wrapping a value in a polymorph allows it to be stored in tables of
polymorphs, perhaps with other wrapped values of completely different
types or typestates.  Likewise, polymorphs can be used in interface
definitions to allow arbitrary values to be transmitted over the
interface.

The holder of a polymorph value can retrieve the value wrapped therein
by means of the {\tt unwrap} operation, as in:
\begin{verbatim}
unwrap x from arb {init};
\end{verbatim}
The value wrapped in the polymorph must be of the same type as the
variable into which it is being unwrapped.  Furthermore, the typestate
of the wrapped value must be at least as high as that specified in the
{\tt unwrap} statement.  If the wrapped typestate is higher, the value
is coerced down to the indicated typestate.  The variable that held
the polymorph value is left unitialized following an {\tt unwrap}
operation.
\item Inspecting a Wrapped Value\label{inspect-polymorph}\par A
polymorph can be inspected without actually unwrapping it via the {\tt
inspect {\em polymorph}} statement, as in:
\begin{verbatim}
inspect x:integer from arb {init} begin
  ...                   -- use (but do not change) the value of x
end inspect;
\end{verbatim}
Within the body of the inspect, the indicated variable refers to a
constant copy of the value wrapped in the polymorph.  The polymorph
itself remains unchanged.  The wrapped value must be of the indicated
type, and must be in a typestate at least as high as that given in the
{\tt inspect} statement.
\end{enumerate}
\item Control Statements
\begin{enumerate}
\item If-Then-Else\par The {\tt if-then-else} statement is used to
control program flow based on the value of some boolean expression, as
in:
\begin{verbatim}
if x < 10 then
  ...
else
  ...
end if;
\end{verbatim}
The {\tt else} clause can be omitted entirely, as in:
\begin{verbatim}
if x < 10 then
  ...
end if;
\end{verbatim}
\item While-Repeat\par The {\tt while} statement is used to repeat a
body of code as long as a specified boolean expression yields a {\em
true} value:
\begin{verbatim}
while x < 10 repeat
  ...
  x <- x + 1;
end while;
\end{verbatim}
\item Select\par The {\tt select} statement transfer control to one of
several bodies of code (called {\em clauses}), depending on the state
of {\em guards} associated with the clauses.  There are a number of
different forms, as follows:
\begin{enumerate}
\item Boolean Guards\par Each guard can be a simple boolean
expression, allowing a conditional choice with more than two
``prongs'' (this is thus a generalization of the {\tt if-then-else}
statement).  Each guard, introduced by the word {\tt where}, is a
boolean expression.  If any guard evaluates to a {\tt true} value, one
of the corresponding clauses (it could be any of them) is executed.
Otherwise, the {\tt otherwise} clause is executed.
\begin{verbatim}
select
  where (x < 10)
    ...
  where (x < 100)
    ...
  where (x < 1000)
    ...
  otherwise
    ...
end select;
\end{verbatim}
Note that if {\tt x} has a value of {\tt 5}, the above statement could
result in {\em any} of the first three clauses being executed, since
all three guards evaluate to {\em true}.  This indeterminacy would
disappear if the second guard were rewritten as {\tt where (x >= 10 and x
< 100)} and likewise for the third guard.  Note that the {\tt
otherwise} guard is {\em not} subject to this indeterminacy; it is
chosen only if all other clauses are disabled due to guards which
evaluate to {\em false}.
\item Shorthand for Equality Tests\par If all the boolean guards in
the above form of the {\tt select} statement consist of equality tests
with a common expression, a shorthand notation is available as
in the following example:
\begin{verbatim}
select x.color
  where ('red')
    ...
  where ('blue')
    ...
  ...
  otherwise
    ...
end select;
\end{verbatim}
In this case, each clause is enabled or disabled according to whether
the value appearing in its {\tt where} guard is equal to the value of
the expression appearing immediately after the word {\tt select}.
Note that the compiler is not intelligent enough to realize when
you've listed all possible cases explicitly; an {\tt otherwise}
clauses is {\em always} required in a {\tt select} statement, though
it may be empty.
\item Waiting for Messages\par The guards in a {\tt select} statement
can name inports rather than specify boolean conditions.  In this
case, the {\tt select} statement waits for a message to be available
on one of the indicate inports and then executes the associated
clause.  This is frequently used for a server process that provides
multiple services to clients via multiple input ports, as in:
\begin{verbatim}
select
  event pushQ
    receive pushRequest from pushQ;
    ...
  event popQ
    receive popRequest from popQ;
    ...
  otherwise
end select;
\end{verbatim}
Note again that, even though the {\tt otherwise} clause can never be
executed, it must nevertheless appear.  Note also that when a clause
is executed by this select statement, the incoming message that
triggered the clause must still be explicitly received, as it is still
queued on the inport.
\item Combining Boolean and Event Guards\par In its most general form
the {\tt select} statement can include clauses with boolean guards,
clauses with event guards, and clauses with both, all mixed in a
single {\tt select} statement.  When such a statement is executed,
first all the boolean guards are evaluated to decide which of the
clauses are ``enabled;''  clauses without boolean guards are
implicitly enabled.  If any clauses are enabled, then either an
enabled clause without an event guard is executed, or the {\tt select}
statement waits for a message to arrive on one of the inports named in
an event guard of an enabled clause.  In the latter case the
corresponding clause is executed.  If {\em none} of the clauses is
enabled as a result of the initial evaluation of the boolean guards,
the {\tt otherwise} clause is executed.  Here's an example:
\begin{verbatim}
select
  event pushQ and where (size of stack < limit)
    receive pushRequest from pushQ;
    ...
  event popQ and where (size of stack > 0)
    receive popRequest from popQ;
    ...
  otherwise
    -- must have limit = 0 for this to ever be executed... 
    -- probably you have your limit set wrong
end select;
\end{verbatim}
Again, as always, the {\tt select} statement requires an {\tt
otherwise} clause, even if it can be proven to be unreachable.
\end{enumerate}
\item Blocks\label{block-statements}\par A {\tt block} statement
serves two purposes: (1) it introduces new variable declarations,
local to the body of the block; and (2) it attaches {\em exception
handlers} to the code in the block.  Exceptions are run-time
conditions that cause a break in the normal flow of control in a
program.  When an exception condition is detected (we say the
exception is {\em raised}), the currently executing Hermes statement
is interrupted, and execution resumes with the innermost exception
handler that handles the exception being raised.  See
item~\ref{exceptions} for a discussion of the various types of
exceptions that can occur.

The {\tt block} statement has the following general form, which is
nearly identical to the form of the program skeleton shown in
item~\ref{process-module-skeleton}:
\begin{verbatim}
block declare
  ...           -- declarations local to this block
begin
  ...           -- code body of this block
on (...)        -- identifies one or more exception conditions
  ...           -- code to be executed when one of the indicated
                -- exceptions is raised
on (...)        -- additional exception handlers
  ...
...
end block;
\end{verbatim}
If there are no new declarations introduced by the block the word
{\tt declare} may be omitted.

The {\tt block statement} is normally executed simply by executing all
the statements in the main body of the block.  Should an exception be
raised during the execution, control will pass to the exception
handler, if any, handling that exception.  If the current block has
not provided a handler for an exception, its containing block is
allowed to handle the exception, and so forth up to the outermost
block (the ``main program'' block).  The outermost block implicitly
handles all exceptions not otherwise handled by the program, and its
behavior when such an exception is handled is to simply terminate the
process that experienced the exception.

If the main body of the block terminates without raising an exception,
execution resumes with the statement following the entire {\tt block}
statement.  This is also the case following the execution of any
exception handler attached to a block.

The special keyword {\tt others} appearing in an exceptions list can
be used to introduce a handler that will handle any exception not
otherwise handled within the body of the associated block.  For
example, all exceptions occuring within the main body of the following
block will be handled by the attached {\tt on (others)} handler:
\begin{verbatim}
block begin
  ...
on (others)
  ...
end block;
\end{verbatim}
Note that exception handlers can themselves raise exceptions.  Such
an exception will never be handled by a handler attached to the same
block as the one to which the executing handler is attached; rather
the exception will propogate outward at least to the next enclosing
block.  The implicit {\tt on (others)} handler attached to the
outermost block can never raise an exception since it does nothing (it
simply exits the outermost block, thereby causing the process to
terminate).
\item Looping Through an Enumeration\par It is sometimes convenient to
loop over all the values in an enumeration type.  This can be achieved
with the {\tt for-enumerate} statement, as in:
\begin{verbatim}
for c: color repeat
  ...
end for;
\end{verbatim}
The body of the statement is executed once with the indicated variable
({\tt c}, above) bound to each value of the indicated enumeration type
in turn.  If the enumeration type is ordered, the values will be
visited in increasing order; otherwise the order is unpredictable.
\end{enumerate}
\item Dynamics and Communication
\begin{enumerate}
\item Creating Processes\par A new running process can be created from
any {\em checked} program.  See items~\ref{currentprogram}
and~\ref{programliterals} for two means of acquiring checked program
values.  The {\tt assert checked()} statement can convert an unchecked
program into a checked program, but it is not currently implemented.
Unchecked program values are normal Hermes records that can be
constructed wholly under program control; relevant type declarations
appear in the {\tt predefined} definitions module.  See the Users'
Guide for instructions on checking unchecked programs via the Hermes
compiler and on using various program loading facilities.

Two operations on checked programs result in the creation of
processes: {\tt create of} and {\tt procedure of}.  Either operation
results in an outport connected to the new process by means of its
initialization port (declared in the program being instantiated).
All other variables in the newly created process are initially
uninitialized.  The creating process can use its connection to the new
process' initialization port to establish additional communication
channels by exchanging other ports, or to exchange other information
as needed.

The {\tt create of} operation immediately creates a running instance
of the program operand.  The {\tt procedure of} operation does not
immediately create a new process; instead, each time a message is sent
to the resulting outport, a new process is created and the message is
routed to that process' initialization port.  Thus, every message sent
to an outport obtained via {\tt procedure of} will be sent to a
different process, created specifically to handle that message.

{\tt Procedure of} is convenient when a program is designed to handle
a single request and then terminate, like procedures in some other
languages.  {\tt Create of} is used when the same process must handle
multiple requests and maintain state between individual requests.
Following is an example of both:
\label{inline-proglit-example}
\begin{verbatim}
times2 <- procedure of process (q: times2Q)
   declare
     args: times2Intf;
   begin
     receive args from q;
     args.double <- 2 * args.value;
     return args;
   end process;
accumulate <- create of process (q: sumQ)
    declare
      args: sumIntf;
      sum: integer;
    begin
      sum <- 0;
      while 'true' repeat
        receive args from q;
        sum <- sum + args.value;
        args.sumSoFar <- sum;
        return args;
      end while;
    end process);
while 'true' repeat
  n <- getIntFromUser("Number: ");
  twiceN <- times2(n);
  sum <- accumulate(n);
  call putLine("2 * " | fmt(n) | " = " | fmt(twiceN));
  call putLine("Accumulated sum = " | fmt(sum));
end while;
\end{verbatim}
In this example, each time the outport {\tt twiceN} is used in a {\tt
call} statement (or, as in this case, a function call), a new process
is created running a program that will double its input.  Each new
process created in this manner will serve a single call on its
initialization port and then terminate.  This is dictated by the logic
of the program, not because {\tt procedure of} was used.  If {\tt
create of} were used on this particular program, the resulting outport
would only be useful for a single call; instead, multiple calls can be
made, and each is directed to a new instantiation of the doubling
program.

The outport {\tt accumulate}, in constrast, is acquired by means of
{\tt create of}, and represents a fixed connection to the
initialization port of a single process created at the time of the
{\tt create of} operation.  The program from which this process is
created specifies a loop which will accept a call on the
initialization port and then use the call parameters to update an
accumulating sum.  Thus this process maintains state between
individual calls.  If {\tt procedure of} had been used in this case,
each call on the resulting outport would have started a brand new
instance of the accumulating program, and the sums would not
accumulate from call to call as intended.

Note that there is nothing special about the relationship between a
process and it's creator, beyond the initial connection via the
created process' initialization port.  In particular, there is no
parent/child or other such relationship among Hermes processes.
\item Creating Ports\par A new inport is created via the {\tt new}
operation.  The result is an empty inport (i.e. one with no messages
waiting to be received).  Example:
\begin{verbatim}
new ip;
\end{verbatim}
A new outport is created by means of the {\tt connect} statement,
which specifies an inport to which the outport is to be connected.
\begin{verbatim}
connect op to ip;
\end{verbatim}
The type of the inport variable must be the type appearing in the
outport type's definition.
\item Making Calls\par The most common means of communication among
Hermes processes is via the {\tt call} operation.  The calling process
supplies program variables (possibly expression temporaries) for all
the components of the callmessage defining the call interface.  The
values currently stored in those variables are assembled into a
callmessage, which is then transmitted on an outport to be received by
the process owning the connected inport.  The calling program then
blocks, awaiting return of the callmessage.  When the callmessage is
returned, its components are unloaded back into the caller's variables
from which they originated, and the caller may then proceed.

There are two ways to perform a {\tt call} operation.
\begin{enumerate}
\item The {\tt Call} Statement\par The form of the {\tt call}
statement is as follows:
\begin{verbatim}
call op(arg1, arg2, ..., argn)
\end{verbatim}
Here, {\tt op} is a variable of some outport type, and {\tt arg1}
through {\tt argn} are variables (or expressions) whose values will be
transferred to successive components of a callmessage constructed for
the call.
\item Function Calls\par An alternate syntax allows a {\tt call}
operation to be used as a value-returning expression, as in:
\begin{verbatim}
result <- op(arg1, arg2, ... argn)
\end{verbatim}
In this case, {\tt arg1} through {\tt argn} are used to fill the first
$n$ components of a callmessage, and on return, the $n+1^{\hbox{st}}$
component is moved into the variable, {\tt result}.  Thus the
callmessage type on which {\tt op}'s outport type definition is based
(indirectly through some inport type definition) must have $n+1$
components, the last of which corresponds to the return value when the
function call syntax is used.  If function call syntax is to be used,
the first $n$ callmessage components must be listed in the {\tt
constant(...)} list in the callmessage type definition, as Hermes
expressions are not allowed to have any side-effects with respect to
the values of variables used in the expression.
\end{enumerate}
\item Receiving Messages\par The {\tt receive} statement is used to
dequeue messages that have arrived at an inport; the messages may have
been sent by means of a {\tt call} statement, a function call, or a
{\tt send} statement.  If the inport is empty when the {\tt receive}
operation is performed, the process executing the {\tt receive} blocks
until a message arrives, and then proceeds normally.  The {\tt
receive} statement has the following form:
\begin{verbatim}
receive msg from ip;
\end{verbatim}
The type of variable {\tt msg} must be the same as that on which the
type of inport {\tt ip} is based.
\item Returning Calls\par The {\tt return} statement sends a
callmessage back to the calling process, allowing that process to
proceed with its execution.  The values in the callmessage components
may have been modified by the callee, subject to constraints imposed
by the call interface (e.g. {\tt constant} component lists and minimum
typestate).  The process that returns a callmessage need not be the
same as the process that originally received it, as callmessages may
be forwarded to other processes via the {\tt send} operation (see
item~\ref{send-operation}).  In addition, a process may be in
possession of multiple callmessages simultaneously, representing
multiple calls in progress at once.

The normal form of the return statement is as follows:
\begin{verbatim}
return cm;
\end{verbatim}
\label{return-exception}
If the callmessage's type definition listed exceptions (see
item~\ref{callmessage-typedef}), then an exception-raising form of the
{\tt return} statement is allowed.\footnote{Since a {\tt discarded}
exception is automatically defined for every callmessage type that
doesn't explicitly contain one, this form is actually always
available.}  If {\tt xxx} is the name of an exception on the type
definition for {\tt cm}'s type, then the following statement returns
the call and raises exception {\tt xxx} of the interface in the
caller:
\begin{verbatim}
return cm exception xxx;
\end{verbatim}
The callmessage variable ({\tt cm} above) is left uninitialized by
both forms of the {\tt return} statement.

Note that a process that returns a callmessage continues its own
execution following the {\tt return} statement.  The {\tt return}
operation should be thought of as a communication operation, {\tt not}
as a control operation.
\item Testing for Messages\par The {\tt empty of} operation tests an
inport to see whether there are any messages that can be received from
it:
\begin{verbatim}
if empty of ip then
  ...           -- compute another digit of pi
else
  receive cm from ip;
  ...           -- do something really useful
end if;
\end{verbatim}
\item Sending Messages Asynchronously\label{send-operation}\par In
addition to the synchronous (caller blocking) {\tt call} operation,
Hermes also provides an asynchronous communication operation, called
{\tt send}.  The general form is:
\begin{verbatim}
send msg to op;
\end{verbatim}
The {\tt msg} value must be of the type on which outport {\tt op}'s
type is based.  The message is enqueued on the inport to which {\tt
op} is connected, and the sending process then proceeds with its
execution without blocking.
\end{enumerate}
\item Miscellaneous Statements and Operations
\begin{enumerate}
\item Making Copies\par Besides the copying assignment operator ({\tt
:=}) discussed in item~\ref{assignment}, copies of Hermes values can
be created by means of the {\tt copy of} operator.  For example, to
insert a value into a table without leaving the source variable
uninitialized, something like the following can be used:
\begin{verbatim}
insert copy of x into t;
\end{verbatim}
The {\tt copy of} operation is often used when an operation that
causes its operand to become uninitialized must be applied to a
variable in a context in which the variable is constant (e.g. it is a
constant component of a callmessage, or it the inspected variable in
an {\tt inspect} statement).  In such a case, the operation must be
performed on a copy of the variable, rather than variable itself.

Inport and callmessage values cannot be copied via either
mechanism.\footnote{This restriction might be removed with future
language changes.}
\item Discarding Values\par A value that is no longer needed can be
explicitly discarded by means of the {\tt discard} statement:
\begin{verbatim}
discard x;
\end{verbatim}
Normally explicit {\tt discard} statements are unneeded as the typestate
analysis phase of the compiler will insert them whenever variables
would otherwise become conditionally initialized or at program
termination.  However, discarding certain types of values can cause
exceptions to be raised in other processes, so there are times when
explicit {\tt discard} statements are useful.
\item Concatenation\par The concatenation operator ({\tt |}) is used
to combine two ordered tables into another.  Most commonly, it is
applied to values of type {\tt predefined!charstring} and corresponds
to normal string concatenation, as in:
\begin{verbatim}
call putLine("So, " | userName | "!  What have you done for me lately?"); 
\end{verbatim}
\item Exits\label{exit-statement}\par The {\tt exit} statement causes
behavior very similar to what occurs when an exception has been
raised: it causes an immediate jump to the innermost exception handler
that has been provided to handle the indicated exit.  Here is an
example:
\begin{verbatim}
block begin
  while 'true' repeat
    answer <- askYesOrNo("Do you wish to continue? ");
    if answer = "no" then
      exit done;
    else
      ...
    end if;
  end while;
on exit(done)
  -- all finished
end block;
\end{verbatim}
\item Evaluate Blocks\par If a complex piece of code is required to
compute a value to be used in an expression, an {\tt evaluate} block
can be used to express the computation.  For example:
\begin{verbatim}
insert (evaluate emp: employeeRec from
    new emp;
    emp.name <- name;
    ...
  end) into employees;
\end{verbatim}
Within the {\tt evaluate} block, no variables declared outside the
block may be altered, due to the Hermes rule that expressions must
have no side-effects with respect to values of program variables.
\item Creating Nominals\label{unique}\par New nominals are created
with the {\tt unique} operator:
\begin{verbatim}
id <- unique;
\end{verbatim}
\item The Current Program\label{currentprogram}\par A process can
retrieve the program it is executing as a checked program value, via
the {\tt currentprogram} operation.  This is sometimes used to make
recursive calls:
\begin{verbatim}
self <- create of currentprogram;
call self(...)
\end{verbatim}
\item Program Literals\label{programliterals}\par A program literal
identifies a checked program value that can be used as an expression.
Programs obtained from program literals will be checked, and therefore
can be used as arguments to the {\tt create of} and {\tt procedure of}
operations.  There are two forms of program literals:
\begin{enumerate}
\item In-Line Program Literals\par The source for an entire Hermes
program can appear as a program literal, as in the example for
item~\ref{inline-proglit-example}.  The form of an inline program
literal is exactly the same as the form for a Hermes process module
except that no initial module name, {\tt using(...)} list, or {\tt
linking(...)} list appear.  The modules imported via top-level {\tt
using(...)} and {\tt linking(...)} lists are available to inline
program literals.
\item Statically Linked Programs\par Programs named in the {\tt
linking(...)} list of a process module are incorporated by the
compiler into the program being compiled.  Programs thus incorporated
are then available for use in named program literals, as follows:
\begin{verbatim}
foo: using (...)
linking (bar, ...)
process (...)
declare
  ...
begin
  ...
  barFn <- create of process bar;
  ...
end process
\end{verbatim}
In this example, we say that program {\tt foo} {\em statically links}
program {\tt bar}.  Program {\tt bar} is incorporated in its compiled
form, and must therefore be compiled prior to compiling {\tt foo}.
See the Users' Guide for details on how references to statically
linked programs are resolved by the compiler.
\end{enumerate}
\end{enumerate}
\end{enumerate}
\item Exceptions\label{exceptions}\par Exception handlers were described in
item~\ref{block-statements} above.  Here we describe the types of
exceptions that can be raised, and how they are identified in
exception handlers.  There are two types of exception:
\begin{enumerate}
\item Built-In Exceptions\par These are exceptions that indicate
problems executing the basic Hermes operations required by a program.
When a built-in exception is raised, the currently executing
instruction is interrupted, and all effects it may already have had
are erased prior to jumping to the appropriate exception handler.
Thus any Hermes operation that raises an exception will appear not to
have begun execution by the time the exception handler is invoked.
The built-in exceptions and the conditions under which they can be
raised are:
\begin{enumerate}
\item {\tt Depletion}\par This exception can be raised by almost any
Hermes operation (but never by a {\em coercion}, see
item~\ref{coercions}).  It is an indication of general resource
unavailability, such as insufficient memory, numeric results that
exceed available representation limits, unavailability of network
resources required for a {\tt send} or {\tt call} operation, etc.
\item {\tt CaseError}\par Caused by a {\tt reveal} statement when the variant
being revealed is in a case other than that indicated in the {\tt
reveal} statement.
\item {\tt ConstraintFailure}\par Caused by an {\tt assert} statement whose
constraint expression yields the value {\em false}.  Constraints and
the {\tt assert} statement are not yet implemented and are not further
described in this document.
\item {\tt ConstraintError}\par Caused by an {\tt assert} statement whose
constraint expression raises an exception.  Constraints and the {\tt
assert} statement are not yet implemented and are not further
described in this document.
\item {\tt Disconnected}\par This exception is raised in any process that is
waiting for messages to arrive on inports for which no connected
outports exist.  The process might be executing a {\tt receive}
statement or a {\tt select} statement in which there are enabled
clauses and all enabled clauses have associated event guards.  The
disconnected condition may exist prior to execution of the {\tt
receive} or {\tt select} operation, or it may develop while the process
executing the statement is blocked awaiting a message.

The current implementation will also raise {\tt Disconnected}
exception for a process that attempts to {\tt call} or {\tt send} to
an outport whose connected inport has been discarded.  In a future
release, this may cease to be the case.
\item {\tt DivideByZero}\par Raised whenever the divisor (second operand) of a
division, {\tt mod}, or {\tt rem} operation is zero.
\item {\tt DuplicateKey}\par Raised whenever an {\tt insert} or {\tt merge}
instruction attempts to add an element to a keyed table which already
contains an element with the same key value.  Note that when {\tt
DuplicateKey} is raised for a {\tt merge} operation, {\em no} elements
are added to the destination table, even if some elements of the
source table could be added without violating any key specifications.
\item {\tt InterfaceMismatch}\par This exception indicates that the type of the
initialization port of a program being instantiated with {\tt create
of} or {\tt procedure of} is not the type on which the expected
outport type is based.
\item {\tt NotFound}\par This exception can be raised by any of the table
operations that must select a single table element.  These are: {\tt
inspect} (item~\ref{inspect-table}), {\tt position of} applied to a
selector (item~\ref{position-of-selector}), {\tt remove}
(item~\ref{remove}), and selector as an expression
(item~\ref{selector-expression}).  Note that {\tt exists of} will not
raise {\tt NotFound}; it simply evaluates to {\em false} when no
element is selected.
\item {\tt PolymorphMismatch}\par This exception is raised whenever a
polymorph is unwrapped or inspected, and either the wrapped type is
not the type of the receiving variable, or the wrapped typestate is
not at least as high as the typestate specified in the statement.
\item {\tt DefinitionError}\par This exception is raised by the {\tt
checkdefinitions} statement when the definitions module being checked
contains errors.  The {\tt checkdefinitions} statement is not yet
implemented, and is not otherwise discussed in this document.
\item {\tt RangeError}\par This exception is raised by a {\tt convert of}
operation that attempts to convert any value to an ordered enumeration
value, and the value to be converted is either negative or greater
than or equal to the number of values in the enumeration type.  It is
also raised by an {\tt insert} or {\tt merge} operation that specifies
a position (via the {\tt at} keyword) that is greater than the current
size of the receiving table.
\item {\tt Uncopyable}\par This exception is raised whenever any attempt is
made to copy an inport or callmessage.  Records, variants, tables, and
polymorphs that contain uncopyable values are also uncopyable.
\end{enumerate}
Exception handlers list built-in exceptions they are to handle via the
names listed above.  For example:
\begin{verbatim}
block begin
  insert x into t;
on (duplicateKey)
end block;
\end{verbatim}
\item User-Defined Exceptions\par As discussed under
item~\ref{callmessage-typedef}, callmessage type definitions can
include named exception returns.  A process owning a callmessage can
name any exception defined for the callmessage on a {\tt return}
statement used to return the callmessage, as discussed in
item~\ref{return-exception}.  In this case, the caller that originated
the callmessage experiences an exception.  A handler names this
exception by means of the callmessage type name and the exception
name, as in:
\begin{verbatim}
block begin
  while 'true' repeat
    call putLine(file.readLine());
  end while;
on (readLineIntf.endOfInput)
end block;
\end{verbatim}
\item Exit handlers\par Though they are not technically exceptions,
{\tt exit} statements cause jumps very similar to those caused by
exceptions.  Handers can be designated to handle {\tt exit}'s by means
of an {\tt on exit(...)} clause listing the names of the exits to be
handled.  An example appears with item~\ref{exit-statement}.
\item {\tt On (Others)}\par A handler clause of the form {\tt on
(others)} will handle all exceptions occuring within the associated
block's main body that are not otherwise handled.  Note, however, that
{\tt exit}'s are {\em not} handled by {\tt on (others)} handlers;
explicit handlers must appear for all {\tt exit} statements in a
program.
\end{enumerate}
Note that a single handler clause can list exceptions, or exits, or
{\tt others}, but no mixing of these three cases is allowed.
\item Typestate\label{typestates}\par Typestate checking is a feature
of Hermes that goes beyond conventional type checking.  The Hermes
compiler uses typestate checking to ensure that operations are
performed, not only on operands of the correct type, but also only on
operands that can be proven to possess certain prerequisite properties
at run-time.  For example, an integer variable must be initialized
before it can be used in an expression; therefore the following
program fragment would be rejected by the compiler:
\begin{verbatim}
discard x;
if y = 0 then
  x <- 1;
end if;
z <- x + 1;
\end{verbatim}
Initialization state is just one of several {\em typestate attributes}
tracked on a variable-by-variable (and component-by-component, for
records, callmessages and variants) basis by the Hermes compiler.

See the book, ``Hermes: A Language for Distributed Computing'' by
Strom et al (Prentice-Hall, 1991) for a complete description of the
typestate checking algorithm and typestate preconditions required by
specific operations.

\begin{enumerate}
\item Specifying Typestates\par A typestate is a collection of
typestate attributes, each applying to one or more program variables.
We write down a typestate by listing its attributes within curly
braces, as in:
\begin{verbatim}
{init(x), case(v, v.a)}
\end{verbatim}
\item Built-In Typestate Attributes\par The built-in attributes are as
follows:\footnote{User-defined ``constraint'' attributes are not yet
implemented and are not discussed further in this document.}
\begin{enumerate}
\item {\tt init(x)}\par Indicates that variable {\tt x} is known to
have a value.
\item {\tt case(v, v.a)}\par Indicates that the variant value
contained in variable {\tt v} is known to be in the case associated
with component {\tt a}.  Whenever {\tt init(v)} is present in a
typestate but no {\tt case(v, v.a)} attribute is present, {\tt v} is
said to be ``hidden.''
\item {\tt checked(p)}\par Indicates that the program value contained
in variable {\tt p} has been checked and is therefore eligible for
instantiation via {\tt create of} or {\tt procedure of}.
\item {\tt checkeddefinitions(d)}\par Indicates that the definitions
module {\tt d} has been checked and is known to be error-free.  All
definitions modules contained in a program value must have this
attribute before the program value can become checked.
\end{enumerate}
\item The {\tt full} attribute\par The {\tt full} typestate attribute
is an abbreviation for one or more {\tt init} attributes.
Specifically, if {\tt x} is a variable of a record or callmessage
type, {\tt full(x)} means {\tt init(x)} and recursively {\tt
full(x.c)} for all components {\tt c} of {\tt x}.  If {\tt x} is any
other type, {\tt full(x)} and {\tt init(x)} are synonymous.
\item Formal Typestates\par Where typestates appear in the syntax of
Hermes type definitions and statements, they must be in a special form
known as ``formal typestates.''  A formal typestate looks just like a
normal typestate, except arguments to typestate attributes are
partially implied by context.  For example, the typestate
specification in a table type definition (see
item~\ref{table-typedef}) specifies the typestate of every value that
will ever exist as an element of a table of that type.  In the type
definition itself, there is no variable name that can be used to refer
to table elements, so formal typestates are used in which the implied
variable is interpreted as ``any table element.''

In a formal typestate attribute, each argument is interpreted as
follows:
\begin{itemize}
\item An asterisk ({\tt *}) is interpreted as the implied variable.
\item A name is interpreted as a component of the implied variable,
which must be a record, callmessage, or variant.
\item A totally missing argument list (no parentheses following the
attribute name) is equivalent to a single asterisk, i.e. a single
argument representing the implied variable.
\end{itemize}
As an example of the first two rules, the following table definition
indicates that elements must be initialized, and must be in case {\tt 'atom'},
corresponding to component {\tt name}:
\begin{verbatim}
lispValue: variant (
  'pair' -> pair: lispPair,
  'atom' -> name: charstring,
  'nil' -> nil: empty
);
lispAtoms: table of lispValue {init(*), case(*, name)};
\end{verbatim}
The following example illustrates the final rule; all table elements
must have the {\tt checked} attribute:
\begin{verbatim}
checkedPrograms: table of program {checked};
\end{verbatim}
Formal typestates appear in type definitions for tables (see
item~\ref{table-typedef}), variants (see item~\ref{variant-typedef}),
inports (see item~\ref{inport-typedef}), and callmessages (see
item~\ref{callmessage-typedef}).  They also appear in the {\tt unwrap}
(see item~\ref{unwrap}) and {\tt inspect {\em polymorph}} (see
item~\ref{inspect-polymorph}) statements.
\item Coercions\label{coercions}\par As a result of its typestate
analysis the compiler may (and almost always does) identify points in
the program at which certain typestate attributes must be dropped in
order for the program to meet all typestate requirements.  For
example, assume the following type definitions:
\begin{verbatim}
e: enumeration ('a', 'b');
v: variant of e (
  'a' -> a: aType {full},
  'b' -> b: bType {full}
);
t: table of v {init};
\end{verbatim}
Now consider the following program fragment:
\begin{verbatim}
block declare
  aValue: aType;
  v: v;
  t: t;
begin
  ...
  unite v.a from aValue;
  insert v into t;
  ...
end block;
\end{verbatim}
At the point of the {\tt insert} statement, the following typestate
attributes (among others) are present for {\tt v}: {\tt init(v),
case(v,v.a)}.  The table type {\tt t} requires that its elements be
hidden (no {\tt case} attribute appears in the element typestate given
in the table type definition).  Hence, the typestate algorithm
requires that the attribute {\tt case(v,v.a)} be dropped prior to the
{\tt insert} operation.

In order to drop attributes, the compiler inserts {\em coercions} into
the program during compilation.  For every typestate attribute there
exists a coercion that causes the attribute to be dropped (and the
condition it represents to become false).  For technical reasons,
coercion operations are never allowed to raise exceptions.

The coercions used to drop the built-in typestate attributes are:
\begin{itemize}
\item {\tt discard}---Drops an {\tt init} attribute.  Causes the value
contained in a variable to be discarded (generally implying the
release of resources, such as heap-allocated storage, required for the
representation of the value).
\item {\tt hide}---Drops a {\tt case} attribute.  The value of the
currently revealed variant component must first be coerced down to the
corresponding case typestate listed in the variant type definition,
possibly resulting in additional coercions.
\item {\tt drop}---Drops a {\tt checked} or {\tt checkeddefinitions}
attribute.  In the current implementation, {\tt drop} is a no-op.
\end{itemize}

Besides statement preconditions, coercions are needed whenever two or
more control flows join, and the typestates present on the incoming
branches are not identical.  In this case, the highest typestate
consistent with all incoming branch typestates is computed (the
``meet'' in a lattice-theoretic sense), and coercions are inserted
along each incoming branch to lower the typestate along that branch
accordingly.  For example, in the following example, {\tt discard(x)}
is inserted at the end of the {\tt then} clause, since {\tt init(x)}
is present along that branch but not in the {\tt else} clause.
\begin{verbatim}
discard x;
if color = 'red' then
  x <- f();
  y <- x * 2;
else
  y <- 100;
end if;
\end{verbatim}
\end{enumerate}
\end{enumerate}

\label{lastpage}
\end{document}
