Carnegie Mellon University

Research Showcase @ CMU

Computer Science Department School of Computer Science


An Informal Definition of Alphard (Preliminary)

Paul N. Hilfinger

Carnegie Mellon University

Gary Feldman

Robert Fitzgerald

Izumi Kimura

Follow this and additional works at:

This Technical Report is brought to you for free and open access by the School of Computer Science at Research Showcase @ CMU.
It has been accepted for inclusion in Computer Science Department by an authorized administrator of Research Showcase @ CMU.
For more information, please contact

The copyright law of the United States (title 17, US. Code) governs the making
of photocopies or other reproductions of copyrighted material. Any copying of this
document without permission of its author may be prohibited by law.


An Informal Definition of Alphard

Paul Hilfinger
Gary Feldman
Robert Fitzgerald
Izumi Kimura
Ralph L. London
KVS Prasad
VR Prasad
Jonathan Rosenberg
Mary Shaw
Wm. A. Wulf (editor)

February 12, 1978
Computer Science Department
Carnegie-Mellon University
Pittsburgh Pa., 15113

This work was supported in part by the Advanced Research Projects Agency cf the Department of Defense under contract: DAHC 15-72-C-0308 and F44620-73-C-0074 ( which is monitored by the Air Force Office of Scientific Research), and in part by the National Science Foundation Grant OCR 74-04187.

An Informal Definition of Alphard


The authors and their colleagues have been experimenting with a collection of ideas about
programming languages for several years. Our goals included determining the extent to which language
could support contemporary programming methodology, could aid In the construction of verifiable
programs, and, at the same time, could be a completely practical programming tool.

in the context of that exploratory spirit it seemed inappropriate to rigidly blnd decisions about the
details of the language. Hence, although our explorations were carried out in a relatively uniform
notation and published under the name "Alphard", there really never was an Alphard language. The
astute reader of our previous publications will have noted, and probably will have been frustrated by,
the fact that we felt completely free to change the notation from paper to paper as the needs of our
exploration seemed to warrant.

With this document we are breaking with our previous strategy. We are new defining a specific
language which we expect to serve as the basis of our further research, in the future we do not
intend to alter this language In the same free manner as we have in the past. There are two reasons
for this shift in strategy: First, although we didn't admit it, much of the language was frozen in our
heads, and the minor differences that appeared in published examples only served to confuse our
readers. Second, and far more importantly, we believe that the premises on which all the "data
abstraction" languages are based are untested in practice. We feel the need to gain experience
before we can proceed with any confidence to tackle the next set of exploratory questions. To gain
that experience we need to freeze, and to implement, at least some portion of the language -- and that
is what we are now doing.

Since we expect to work in the context of the language defined here for some time to come, the
language Is extremely conservative. Our past experience has been that simultaneously achieving
verifiability and efficiency is possible -~ but delicate. Hence we have chosen to include only features
whose implications we fully understand. For example, we have omitted features dealing with
concurrency, exceptional-condition handling, and so on. We fully appreciate that these features will be
needed in a "production" version of Alphard; they are emitted here because they are still the subject
of our research.

The present version of this report carries the word "Preliminary" in Its title; we hope to promptly
circulate a second version of the report from which this word has been ellded. Our purpose in
circulating this first version is to solicit comment. We will deeply appreciate any and all critiques of
both the language and its presentation. Such comments should be sent to Bill Wulf,
Computer Science Department. Carnegie-Mellon University, Pittsburgh. Pa. 15213.

An Informal Definition of Alphard i

  1. Introduction 2
    1. Unusual Aspects of the Language 3
    2. Style and Conventions of the Report 5
  2. Fundamental Concepts 7
    1. Objects, Addresses, and Values 7
    2. Type and Type Descriptions 8
    3. Binding 10
    4. Type Matching 11
  3. Basic Lexical Structure 14
    1. Symbols 14
    2. Comments 14
    3. Identifiers 15
    4. Special Rewrite Rules 15
    5. Special literals 17
  4. Program Structure, Expressions and Statements 19
    1. Program Structure, Blocks 19
    2. Expressions and Statements 19
    3. Invocations 20
    4. Conditional Expressions 22
    5. Value Expression 23
    6. With Expressions 23
    7. First Expression 24
    8. Loop Statements 25
    9. Exit Statements 25
    10. Null statement 26
    11. Inner block 26
    12. Assert Statement 26
  5. Declarations 28
    1. Scope of Declarations 28
    2. Auxiliary Declarations 28
    3. Remote Definitions 29
    4. Label Declarations 29
    5. Object Declarations 29
    6. Evaluation of Type Descriptions 30
    7. Formal Parameters 32
    8. Routine Declarations 33
    9. Form Declarations 35
    10. Abbreviations 36
    11. Generators 37
    12. Assumptions 39

An Informal Definition of Alphard ii

Apx A: Collected Syntax 40

Apx B: Standard Prelude 43

B.1. Primitive Prelude 43

B.2. Standard Prelude 43

B.3. Implementation Prelude 44

Apx C: Special ldentifier Assumptions 46

C.1. Generator routines 46

C.2. Extensible routines 47

Apx D: A Complete Example 48

Apx E: Proof Rules 51


Chapter 1

The Alphard language has been designed to meet several objectives simultaneously:

To support contemporary programming methodology, and to encourage the development of
understandable and modifiable programs. Specifically, we wish to make the abstractions
used during the construction of a program explicit in the resulting program text.

To permit formal specification of properties of a program, and to permit practical verification
(proof) that the program satisfies these specifications.

To permit the programmer to control certain decisions that have traditionally been preempted by
the language implementation (e.g,, the representation of data structures and method of
storage allocation).

To permit the Alphard compiler to generate compact, efficient code. With the aid of an
optimizing compiler, we expect to produce better code than is typically produced by
assembly language programmers.

In setting these objectives, our principal concern is with high quality, reel programs -- those which are
used extensively and are of significant size and complexity. Many of these programs arise in the area
which has been called "systems": compilers, operating systems, and the like: such applications are
representative of our concerns although they are not our exclusive focus. Our intended user
community consists of relatively experienced professionals rather than casual or student programmers.

The designers of a programming language generally make a number of philosophical decisions that
have manifold effects on the product of their effort. We, for example, believe that "power" or
"expressiveness" is best achieved through mechanisms which permit the programmer to synthesize
more complex facilities out of relatively simpler ones. Thus the composition, or structurlng
mechanisms play the central role in Alphard; by contrast, for example, the collection of primitive data
types is small. The philosophical justifications for this decision are: (1) all of the familiar data types
can be built from Alphard's primitives, (2) the basic language is much simpler without a large collection
of data types, and (3) in making the composition mechanism strong enough to define the familiar data
types, we have also made it strong enough to define many more problem-specific ones.

Perhaps nowhere are the language designers' philosophies more evident than in those decisions
relating to the tradeoffs between expressiveness, safety, and efficiency. Alphard, like all languages,
strives for a balance between these, but our notion of balance is colored by the intended application
area(s) and user profiles. For these applications the long term costs of maintaining and running
programs far outweigh their initial development costs. Thus we have tilted the balance in favor of
those language attributes which contribute to efficiency and maintainability, possibly at the expense of
those which facilitate rapid program construction.

We have, for example, not emphasized “expressiveness” In the sense of a large collection of
constructs —- each of which is ”just right” for a particular situation. We believe that we have,


however, supported expressiveness in a larger sense by encouraging program organizations which
convey important, abstract information about the way that the program works.

Similarly, we have emphasized safety and efficiency, sometimes at the expense of brevity or
convenience. This has led us to restrict some traditional constructs (e.g., scope and parameter rules)
and refrain from making some tempting generalizations. We are aware of many areas in which the
present design could be generalized in rather obvious ways; we have chosen not to do so, however,
when we might compromise the programmer's confidence in both the correctness and performance of
his program1

1.1. Unusual Aspects of the Language

Many aspects of programming languages have become fairly standard in the past decade. Alphard
constructs are intentionally similar in style and meaning to the analogous constructs in other languages.
In particular, we have leaned heavily on the Algol-Pascal culture: the syntax of expressions, variable
declarations, procedures, and so on, are all derived from this culture. The following, for example, is a
fragment of a valid Alphard program and is obviously similar to Pascal:

     var x,y,z:int;
     if x ≥ y then z:=z+1 fi;

We expect that the similarity between the Alphard constructs and the analogous ones in other
languages will aid both the reader of this report and the programmers who use the language.

There are, however, a number of aspects of the language which differ significantly from many
traditional languages. This section provides brief notes on these aspects of Alphard, it is, in effect, a
list of points at which the reader should be aware that things may not be as expected.

1. Type Definitions: The programmer may define a new type through a construct called a form.
   The form permits both the specification of the abstract properties of (objects of) the new
   type and the implementation of that type in terms of pro-existing types. Type definitions
   (forms) may be parameterized; in particular they may accept other form names as
   parameters. Such forms are called "generic" and define a class of types (e.g., array(T).
   where T is a type, defines array-of-integer, array-of-real, array-of-set-of-integer, etc.).

2. Primitive types: Integer, real, complex, etc, are not primitive types in Alphard; similarly,
   structures such as arrays, records, and references (pointers) are not primitive. All of these
   familiar notions are available, however. Either they are provided as "syntactic sugar"
   through some standard abbreviations, or else they are made available to the programmer as a
   part of a "standard prelude" -- a set of standard definitions which (conceptually) prefaces
   every program. Specifications for the standard prelude are included as appendix
   B to this report.

1 We are convinced that deciding what not to include in a language design is much harder than inventing clever
new things to include.


   There are (only) two distinguished types in Alphard: they are distinguished in the sense that
   must be considered as part of the language and not as part of the standard prelude.
   are "rawstorage" and "boolean". Specifications of these types and their associated
   may be found in appendix B; informally, however:

  1. Type “rawstorage”: This type corresponds to a vector of contiguous, addressable.
    untyped memory “cells” of conventional computers (we shall refer informally to a
    rawstorage unit of length one as a "cell" or a "word" but we make no a
    committment to the number of bits in each such cell): bit-wise logical, shifting, and
    integer operations are defined on cells. All other types are (ultimately)
    represented in terms of objects of type rawstorage, and the definition of this type
    contains the basic mechanism for associating a “higher level” type with an area of
    storage. Type rawstorage is distinguished (only) because its implementation
    cannot be expressed in the language.
  2. Type ”boolean”: Objects of type boolean are primitive (unstructured), and possess
    values from a set designated (true,false). Type boolean is distinguished in the
    sense that, although it can be defined in terms of type rawstorage, it is needed
    for the definition of other language constructs -- e.g., the conditional statement.
    The customary operations are provided.

3. Type Checking: Most modern programming languages contain some notion of the
   "equivalence" of types and require that the types of actual parameters to procedures be
   equivalent, to those specified by the corresponding formal parameter definitions. The
   presence of parameterized and generic type definitions in Alphard makes it advantageous to
   replace the notion of equivalence by a more liberal notion of “matching“. Formal parameter
   definitions specify a collection of properties which the corresponding actual parameter must
   possess, specify a collection of properties which are irrelevant, and provide a limited facility
   for relating properties of distinct parameters. Together these define a class of valid actual
   parameter types, and provide what is generally called “strong typing“; in particular, the
   parameter specification and matching is sufficiently strong to ensure verifiability.

4. Scope Rules: Alphard's block structure is similar to that of Algol 60: declarations appear at
   the head of a block, the meaning of an identifier is determined from its nearest enclosing
   declaration, and so on. Unlike Algol, however, in Alphard the bodies of procedures and forms
   do not inherit the names of variables available in enclosing blocks. The intent of these scope
   restrictions2 is to ensure that all effects of an action can be determined by examining the
   text immediately surrounding the action itself. An additional benefit is that Alphard can be
   implemented (very efficiently) using a stack, but without the need for a display.

5. Operator Overloading: The meaning of the usual infix operators (e.g., "+", "*", etc.) may be
   extended to programmer-defined data types. The symbols for, the associativity of, and the
   precedence of these operators are fixed by the language (see appendix C).

2 A particular consequence of the scope restrictions - together with companion restrictions on overlapping actual
parameters and selectors -— is to prevent unintended "aliasing". That is, they ensure that within a given scope
there is at most one name for a given storage call.


6. Selectors: The programmer may define the representation of a data structure by means of a
   selector. Intuitively, a selector defines an algorithm for naming data, just as a procedure or
   function defines an algorithm for computing values. A selector may be thought of as a
   procedure that returns a pointer (reference, address) to an element of a data structure; the
   syntax for defining selectors is therefore similar to that of procedures. "Pointer" is not,
   however, a type in Alphard; no variables of this type can be declared, and hence the "value"
   returned by a selector cannot be stored. The effect of this (coupled with some verification
   requirements) is that selectors are “safe”; most of the (useful) flexibility of general address
   arithmetic is retained without introducing its corresponding dangers. In particular, It is
   possible to define a restricted style of "reference“ variable completely within the language
   and to ensure that this type is at least as safe as array indices in other languages.

7. Assertions: Assertions are permitted almost everywhere and special syntax encourages
   their use in appropriate places. The language in which the assertions are written, however,
   is not defined by Alphard. The choice of that language is, we believe, a private matter
   between the programmer and verifier.

8. Iteration: Four iteration statements are provided, three of which are somewhat different
   from what one might expect.

  1. The do statement repeats its body until the body invokes an explicit exit.
  2. The for statement serves a function similar to the for-step-until construct of Algol
    60, but does so in a manner that permits the programmer to define the type of the
    control variable, the way it is initialized and incremented, and the nature of the
    test for completion of the loop. These aspects of loop control are all defined in a
    form (usually a specialized form called a generator).
  3. The first statement provides a special syntax for those common loops that search
    a data structure and perform one of two actions depending upon whether or not an
    element with a specified property is found. '

   The fourth iteration construct is the familiar while statement.

9. Sugaring: A number of familiar notions such as records and enumerated types are not
   primitive notions in Alphard. They are provided, however, as abbreviations for the more basic
   notions from which they are formed3

1.2. Style and Conventions of the Report

This report is a precise but informal definition of Alphard; It is neither a primer nor a completely
rigorous formal definition. It is intended, however, to be the reference for users, implementors, and
verifiers. To that end we have attempted to be as precise as our human limitations and the vagaries of
English permit. We have consciously adopted the style and tone of the Algol 60 report, which we
believe remains the exemplar language definition.

The syntactic definition of the language uses conventional BNF with the following additions and

3 Pun intended!


1. Key words (reserved words) are denoted by underlining.
2. Metasymbols are denoted by lower-case letters enclosed in angular brackets, e.g., "(emit)".

3. The symbols ( and ) are meta-brackets and are used to group constructs in the meta-

4. Three superscript characters, possibly in combination with a subscript character, are used to denote the repetition of a construct (or a group of constructs enclosed in {}). In particular:
"*" denotes "zero or more repetitions of".
"+" denotes "one or more repetitions of".
“#” denotes "precisely zero or one instance of".
Since it is often convenient to denote lists of things that are separated by some single punctuation mark, we denote this by placing the punctuation mark directly below the repetition character. Thus,
<vvv> ::= <a> { <b> | <c> }
defines a <vvv> to be an <a> followed by either a <b> or a <c>.
<xxx> ::= <a>*
defines an <xxx> to be a sequence of zero or more a’s.
<yyy> ::= <a> <b>,*
defines a <yyy> to be an <a> followed by zero or more <b>s separated by commas.
<zzz> ::= {<a> | <b>};+
defines a <zzz> to be a sequence of one or more things separated by semicolons — where the "things" may be either <a>s or <b>s.
<uuu> ::= <a>* <b>
defines <uuu> to be either “<a><b>" or simply "<b>"

The semantics of the language are described in English. Proof rules for some constructs are provided
in appendix E.

Certain portions of this report describe processes in terms of extra variable creations, text
replacements (copying), or other actions. These are informal expositions and at all tlmea the language
(compiler) is required to only produce the same net semantic effect. Such expositions should be
interpreted in their intended, helpful sense. Obscure consequences of the particular processes will not
be supported.


Chapter 2
Fundamental Concepts

The following chapters define the syntax and semantics of Alphard; in this chapter we describe
certain pervasive notions that are used in the definition.

A complete Alphard program consists of a collection of declarations and statements which are
elaborated4 to produce some desired effect. Declarations define forms (which, in turn, define classes
of types), routines5 (which may be invoked to evoke further elaboration), variables, and a number of
other entities of lesser immediate importance. Statement: define actions to be performed; they may
specify selective or iterative elaboration of component statements and expressions. Of particular
immediate interest, because they cover the major ideas we wish to discuss, are the notions involved in
the elaboration of the declaration of variables and in the elaboration of routine invocations.

The elaboration of a variable declaration, e.g.
      var x:vector(int,1,10)
begins with elaboration of the type description (vector(int,1,10)), followed by instantiation of an
object of the type resulting from this elaboration (instantiation involves both allocation and
initialization); finally, a binding at the name to the instantiation is performed.

The elaboration of a routine invocation, e.g.,
begins with the elaboration of the actual parameters (a: and y), followed by matching of the nominal
type of the actual parameters with the type descriptions of the positionally corresponding formels; if
this matching succeeds a set at bindings is performed6 and the routine body is elaborated.

The words and phrases in bold-face above, type, object. ..., are representative of the notions we
shall discuss in this chapter. Because of mutual dependencies between the notions, however, we shall
not discuss them in precisely the order in which they are mentioned above. We have chosen instead
an order which attempts to minimizes the forward references.

2.1. Objects, Addresses, and Values

Intuitively an object is a generalized (and typed) storage cell, or variable; it is used to hold the
value of some abstract data type.

4 We use the word “elaboration”, in preference to “execution”, to connote actions taken at “compile time” as well
at “run time”. Elaboration may be thought of as an idealized, direct execution of the textual version of the
Alphard program.

5 The word “routine” is used systematically to cover the notions of proc, vproc, func, and sel.

6 At this point a result object may also be instantiated, but this is not essential to the present discussion.


An object possesses a unique (generalized) address, a type, and a value (or state). Objects may
be dynamically created and destroyed. The address and type of an object are fixed throughout its
lifetime, but the value it possesses may be altered.

An object may be primitive, in which case its values (I.e., the values it may possess) are members of
an arbitrary set. Otherwise, the object is composed of a sequence of one or more (previously created)
objects, called its concrete components. The value of such an object may be taken to be the
sequence of values of its concrete components. For the purpose of the following exposition, if x
denotes an object, xi denotes its ith component object.

Two objects may overlap; that is, their values need not be independent. A common case, though not
the only one, is that one object wholly contains the other, as a vector contains its elements. Two
objects that do not overlap are called independent. Any logical dependency (l.e., overlap) between
the values of two objects is fixed. A newly created object independent of all previously existing
objects is called a new object.

The creation of an object is generally associated with allocation of storage for the object and
inltlalization of its value. The entire process is called instantiation and the resulting object is called
an instantiation of its type. The first step of instantiation is the elaboration (evaluation) of a type
description to yield a type (see section 5.6). Next the object is created. For primitive objects
this is a direct operation; otherwise it is achieved by (recursive) Instantiation of its concrete
components. (Note that at the moment of creation the generalized address of the object is
determined.) After allocation, the initialization procedure defined with the base type of the object ls
invoked as described in section 5.5.

Objects are destroyed by first invoking a finishing procedure defined with the base type of, the
object (as described in section 5.5), then de-allocating the object (for primitive objects) or
destroying its concrete components (for non-primitive objects).

2.2. Type and Type Descriptions

Intuitively, type is that property of an object which defines its possible behaviors7 . More formally, a
type characterizes the possible values (states) of an object and the set of operations that may be
applied to it.

There are two explicit syntactic manifestations of the notion of type in the language: form
declarations (which define a class of types), and type dascriptions (which describe a class of object
types that may be bound to an identifier in declarations or formal parameter specifications).

Form declarations are defined in section 5.9. For our present purposes it is sufficient to
note that: (1) every form has a name. (2) a form may be parametenzed, and (3) the form declaration
makes available various operations. A subset of these operations (the side-effect producing ones) is
called the update set.

7 Note that objects, not values, are typed, indeed naked values do not exist in Alphard -- values only exist in
objects. Thus, for example, we may speak informally of lhe 'velue produced by a procedure", but in fact the
procedure returns an object that contains the value.


Type descriptions are used in three contexts: (1) In variable declarations, where they define the
type of an object to be instantiated. (2) in formal parameter specifications, where they define the
class of legal actual parameters, and (3) In routine definitions, where they specify the type of the
object returned. In addition, in both contexts type descriptions define the nominal type of any object
bound to a particular identifier. Thus, the nominal type of an object is the information about its type
that can be inferred by accessing the object through a particular identifier.

The distinction drawn in the last paragraph between "type“ and "nominal type" Is an important,
though possibly subtle, one. A "type" is associated with an object and determines all possible
behaviors of that object. A "nominal type" is associated with an identifier which, In turn, is bound to an
object. The nominal type associated with an identifier determines the possible behaviors that can be
caused through that identifier. In the general case a nominal type will be "less specific' than the type
of the object to which the identifier is bound.

In the following sections we more formally define the notions of type, type descriptions, and nominal

2.2.1 Type

A type results from the elaboration of a type description (see section 5.6) and consists of a
base type, a (possibly null) sequence of actual type qualifiers, and an update set.

A base type is a form name; it uniquely identifies a class of types. For example, the base type of
"vector(real,1,10)" is "vector". In the following, If T la a type. Base(T)8 represents the base type of

An actual type qualifier is intuitively an actual parameter in a type description; hence it corresponds
to a formal parameter in a form definition. It may be an object address, an object, a routine name, a
type, or a marker denoted unk9. In ”vector(real,1,10)", the actual type qualifiers are "real", "1", and

A type none of whose qualifiers is unk is called a full type: a type with at least one unk qualifier is
called a partial type.

The update set consists of a set of routine designators from among those defined with the base
type; specifically, the update set consists of those routines which may have a (visible) effect on an
object of the type. If T is a type, Update(T) denotes its update set.

If T is a type, then Qual(T) denotes the sequence of actual type qualifiers of T and Quali(T) denotes
the ith element of that sequence.

8 Here and in the sequel we shall use functions such as Base(T), Qual(T), Update(k), etc. to explain semantic
aspects of the language; these functions are only part of the semantic exposition, not constructs in the language

9 The marker unk, which is to be read "unknown", denotes situations in which the corresponding form formal is
not considered a part of the nominal type.


2.2.2 Type Descriptions

A type description is a syntactic construct which describes a class of types and may designate
restricted access to objects of those types. A type description consists of a base type, a sequence
of formal type qualifiers and an update set. The elaboration of a type description yields a type or a
nominal type.

A base type is (as above) a form name.

A formal type qualifier is either the marker unk or else a description at an object address, an object,
a routine, or a type. When used to specify a formal parameter, a formal type qualifier may be an
identifier preceded by a "?" symbol; in such cases an "implicit binding" is implied (see section

The update set consists of a set of routine names trom among those defined with the base type.
Update sets give restrictions on the effect-producing actions that may be applied to an object10. If D
Is a type description. Update(D) denotes its update set.

2.2.3 Nominal Type

A nominal type, like a type, consists of a base type, a (possibly null) sequence of actual type
qualifiers, and an update set. These notions are detined exactly as in the detinition of type.

A type is always associated with an object. A nominal type, on the other hand, is always associated
with an identifier. The nominal type of an identifier may, in the general case, be less specific than the
type of the object to which that identifier is bound; however, the type of an object will always match
the nominal type of the identifier.

2.3. Binding

During elaboration, some identifiers become associated with -- bound to -- entities: these entities
may be objects, routines, or types. The binding at identifiers to obiacts is of particular interest and
includes both the declaration of variables (and associated instantiation of an object) and parameter

In all contexts in which an identifier may become bound to an object (i.a., in a variable declaration or
formal parameter position) there is an associated type description, in the case of a variable
declaration, this description determines the type of the object created, in the case of a formal
parameter, the type description defines the types of allowed actual parameters, in both cases,
however, the type description is elaborated to a nominal type which determines the permitted uses of
the object identified through this identifier.

10 In practice we allow more than just the names of effect-producing operations in the update sol part of certain
type descriptions, notably those which specify generic (formal parameters, in such cases we allow non-olfact-
producing attribute names as well: this is merely a shorlhand for an "assumes clause' (see section 5.12).
This abbrewalicn is permitted because oi its similarity oi intent to the update set: it describes a set of attributes
which the routine or form body requires for correct operation.


In both declarative and formal parameter positions the description of a binding may be preceded by
either var or const. The only difference between the two is that in the latter case (const) the update
set of the identifier is set to empty; in the former (var) case the update set is determined from the
associated type description. A particular consequence of this mechanism is that parameters in const
positions are, intuitively, passed "by reference" but cannot be modified by the called procedure.

If K is an identifier bound to an object, then we refer to this object as Obj(k) and to its associated
nominal type as Type(k).

2.4. Type Matching

The process of parameter binding requires a notion of what it means for an actual parameter to
match, or satisfy, a formal parameter specification, intuitively this process involves determining that
the nominal type associated with the formal parameter ”includes", or “covers", the nominal type of the
actual -- that is, ensuring that the behaviors permissible through the formal parameter name are among
those permissible through the actual parameter name. For simplicity we break this process into three
subprocesses: subsumption, syntactic satisfaction, and implicit binding. Each of these is used for a
different kind of actual/formal matching as specified below.

A list of actual parameters
       a1 ..., an
is said to match a list of formats
       f1:t1, f2:t2, ..., fn:tn where the ai are objects, types, or routine names, if there exists a binding of objects, types, and
routines to the implicit formals in the ti such that if each fi is bound to ai then for each i,
  1. If ti is a description of a routine (proc, vproc, func, or sel), then ai is the name of a "proc“, ...,
    or "sel" with formal parameters identical to those of ti after possible renaming of formal
  2. If ti is "form" (or "pform"), then ai is a type (if ai is a partial type ti must have been pform)
    and the assumed definition of fi (see section 5.12) is syntactically satisfied (see
    section 2.4) by ai.
  3. If ti is a type description, then ai must be an object such that when ti is elaborated, ti
    subsumes Type(ai).

In addition, all implicit formals bound to types must be bound to types syntactically satisfying the
assumed definition of the form (see section 5.12).

The notions of subsumption, syntactic satisfaction, and implicit binding are defined below; we begin
with the notion of subsumption -- the kind of matching used when an object parameter is expected.


   Definition: We say that a (nominal) type Tf subsumes a (nominal) type Ta (in symbols, Tf>>Ta)

  1. Base(Tf) = Base(Ta).
  2. length(Qual(Tf)) ≤ length(Qual(Ta)). Note: if length(Qual(Tf)) < length(Qual(Ta)), the
    formal qualifier sequence of Tf is extended on the right with a sufficient number of
  3. For each qualifier of Tf, i.e., Quali(Tf)):
    1. If Quali(Tf) is unk, Quali(Ta) may be anything.
    2. if Quali(Tf) is a type, Quali(Ta) is also a type and Quali(Tf)>>Quali(Ta)
    3. If Quali(Tf) describes a routine, then Quali(Ta) is also a routine and Quali(Ta)
      matches Quali(Tf).
    4. if Quali(Tf) is an object of base type U, Quali(Ta) is also an object of base
      type U and the value of the result of applying &= for U to Quali(Tf) and
      Quali(Ta) would be true.
  4. Update(Tf) ⊆ Update(Ta)).

In some cases condition 3d cannot be checked at compile time. At the discretion of the implementors,
the compiler may provide the options of generating warnings, generating checking code, or refusing to
compile such cases.

   Definition: Two types are identical if each subsumes the other.

In Alphard, both routines and forms may be "generic“. That is, they may require types as parameters
-- or, equivalently, they may have parameters whose type is not specified in the routine (m) header.
In such cases there will be an "assumes clause" which specifies the properties that the routine (m)
assumes about the generic parameter; this clause gives sufficient information to check all uses of the
parameter locally, in order for a given use of the M or routine to make sense, the actual parameter
must at least meet the syntactic assumptions made about it. Thus the notion of matching formal and
actual parameters in such cases involves of determining whether the actual parameter syntactically
satisfies the formal parameter assumptions 11.

11 More generally, of course, a proof will be required to demonstrate that the actual parameter makes semantic
sense as well.


   Definition Given an assumed declaration of a generic parameter, T:
         form T
            <definitions of f1...fn)
   and a candidate actual type
         Q(a1, a2, ...)
   whose base type is declared
         form Q(p1, ...)
   we say that the type Q(a1,...) syntactically satisfies T if textual substitution of “Q(a1,...)" for
   "T" uniformly throughout the specifications of T results in T‘s specifications containing
   declarations of f1,...fn identical to those in T's specifications (ignoring assertions and
   implementations), though possibly only after suitable renaming of formal parameters.

In the process of determining whether an actual parameter of type T matches a formal parameter
specification we may discover that Qual of the formal is an identifier preceded by "?". Such identifiers
are called "implicit formal parameters“, and are "implicitly bound" to corresponding (qualifiers of the)
actual parameters. Such bindings are performed before other matching.

Definition Let Tf be the formal type and Ta be the actual type. If, in determining whether
Tf>>Ta. Base(Tf) or Quali(Tf) is an identifier preceded by a "?“, the identifier is implicitly
to the corresponding Base(Ta) or Quali(Ta) and becomes an "implicit formal parameter“.
The nominal type of an implicit formal is made identical to the nominal type of the corresponding
form formal. Note that only one binding is established for such identifiers, so multiple
occurrences must be consistent.

In the procedure declaration
proc P(x:vector(int,?lb,?ub)) is ...
for example, "lb" and "ub" are such implicit formals. They are, respectively, the lower and upper
bounds of an actual parameter vector. Thus, if some program fragment contains
... var y:vector(int, 1, 10); ... P(y)
then 1 and 10, respectively, will be implicitly bound to the formals lb and ub.

The following table attempts to recap the essential aspects of the notion of actual/formal parameter

Formal Actual Matching Rule
x:form full type syntactic satisfaction
x:pform type syntactic satisfaction
x:<routine description>   routine name point 3 of match rule
x:?T object Type(noject) must syntactically satisfy T
x:<type description> object subsumption
object object equality under &= for the type of the formal
unk anything always matches
?T match after implicit binding
routine name routine name    same routine


An informal Definition of Alphard

Chapter 3
Basic Lexical Structure

3.1. Symbols

<letter> ::= A | B |... | Z | a |... | z
<digit> ::= 0 | 1 |... | 9
<alphanumeric> ::= <letter> | <digit> | '
<special symbol> ::= <basic symbol> | <operator>
<basic symbol> ::= begin | end | endof | ; | : | ( | ) | $ | :: | & |
if | then | else | fi | case |
of | esac | fo | with | in | ni | first | suchthat | from | do | od |
for | exitloop | leave | skip | assert |
var | const | aux | as specified | = | init |
final | unk | ? | proc | vproc | func | sel | label |
note | eton | ! | elif | elof | pform | while | > | < | . | # |
copy | alias | form | inline | pre | post | rule |
is | forward | external | specs | impl | shared |
invariant | initially | axiom | repmap |
record | enumerated | assumes | value | generator
<operator> ::= <binary operator> | <unary operator>
<binary operator> ::= ↑ | * | / | div | rem | + | - | < | ≤ | = | <> | ≥ | > | and | or | cand | cor | imp |
<assign op>
<unary operator> ::= + | - | not

Typographical features such as blanks (spaces), ends of lines, etc., are generally not significant (but
see section 8.4.3); an implementation may use them to delimit identifiers, numbers, etc. Outside
strings, no such features may appear immediately after the symbol '8." or '?', or around the symbols
"." and "s" when they are used as described in sections 3.4.2 and 4.3.

Upper and lower case letters are distinct. Also, note that the grave symbol is considered a
(significant) alphanumeric and thus may be used in constructing identifiers; it is intended that this be
used to improve program readability by separating mnemonically signlfcant portions of such identifiers.

Basic symbols such as begin are conceptually single characters and are underlined in this report to
emphasize that fact. An implementation, however, must reserve (all upper/lower case spellings of) the
corresponding identifiers to denote these symbols. Thus "BEGIN". "begin", "Begin", etc, are all
interpreted as the basic symbol M: we strongly encourage, however, consistent use of one spelling
in a given program.


The following two commenting constructs are lexically equivalent to a space (blank) character when
they appear outside of strings.

      note <any sequence not containing the lexeme "eton"> eton
      !<any sequence up to end of line>

The first commenting construct encountered in a line takes precedence over any contained within it.


3.3. Identifiers

3.3.1 Syntax

<identifier> ::= <letter> {<alphanumeric>}*
<special identifier> ::= &start | &finish | &next | &done | &value | &subscript | &<operator>
<identifier list> ::= <identifier>,+

3.3.2 Examples


All the above identifiers are distinct.

3.3.3 Semantics

Identifiers have no inherent meanings. They identify objects, forms, types, procedures, selectors.
statements, and parameters. Declarations establish the meanings of identifiers within particular

Two identifiers are defined to be similar if they differ at most in the typographical case used to
spell them; thus "ABC", "Abc", "aBc", etc. are all similar. Except when used as routine names, similar
identifiers may not be declared in the same scope12.

Special identifiers denote entities of special significance in the language. They may be defined but
never directly referenced: they are invoked as the consequence of using some other construct defined
by the language. A simple example of the use of such symbols appears in section 3.4.1, where
the language-defined notion of "+" invokes the user-definable function named ”&+"; more interesting
examples may be found in sections 4.7 and 4.3. (Requirements on the definitions of
such routines appear in appendix C.)

3.4. Special Rewrite Rules

In order to simplify the language definition, a number of familiar and convenient notations are
provided indirectly rather than as a part of the syntax. To accomodate these, we define several
"rewrite rules" that transform programs from the more familiar notation to that described by the report.
These transformations convert infix operators to function invocations, provide “qualified names", and
introduce semicolons. We shall use the notation C1 --> C2 to describe some of these transformations;
the notation means that constructs of the form C1 are transformed into constructs of the form C2.

12This restriction is imposed in order to prevent subtle errors arising from the use of similar identifiers in the
same scope. Routines are exempted from the restriction in order to permit operator overloading.


3.4.1 Operators

Neither the syntax nor semantics of Alphard includes the traditional notion of arithmetic or boolean
expressions with infix operators. Rather, the language is defined as though all operations were
expressed as function invocations, in order to permit the user to write programs in the more familiar
Infix-expression format, however, two transformations are performed. First, the input text is fully
parentheslzed in order to observe the following precedences and associativities:

   1. Associativities: The operators at highest and lowest precedence are right associative: the
   remainder are left associative.

   2. Precedence:
      ↑   (highest precedence)
      *   /   div   rem
      +   -
      ≤   <   =   ≠   >   ≥
      and   cand
      or   cor
      :=   +:=   -:=   *:=   etc.   (lowest precedence)

After being parenthesized, expressions are converted to functional form. If α and β denote arbitrary
unary (monadic) and binary (diadic) operators, respectively, then the following transformations are

      <term>1   β   <term>2   -->   &β(<term>1,<<term>2)
      α<term>   -->   &α(<term>)
      <term>1   β:=   <term>2   -->   &:=(<term>1, &β(<term>2))

where the <term>s denote any phrases balanced in parentheses.

After being placed in functional form, three of the relational operators are rewritten as the boolean
negation of one of the remaining three:

      &≠(t1,t2)   -->   &not(&=(t1,t2))
      &≤(t1,t2)   -->   &not(&>(t1,t2))
      &≥(t1,t2)   -->   &not(&<(t1,t2))

In addition, two of the boolean operators are rewritten as conditional expressions:

      t1 cand t2   -->   if t1 then t2 else false fi
      t1 cor t2    -->   if t1 then true else t2 fi

This rewrite is required to avoid the possibility of undefined argument values in invocations.

Note that, as stated earlier, symbols of the form &<operator> may be defined by the user. Thus, by
giving a definition to "&+", the programmer gives a definition to the operator "+"; this does not allow
redefinition of existing operators, but does allow these operators to be extended to new types.

3.4.2 Name Qualification and Subscripting

It is often convenient to refer to the (visible) components of an object by symbolic names; for example, the components of a record have traditionally been named in this way. The conventional
syntax allows "X.y" to denote the y component of X.


HTML translation in progress

The syntax of Alphard does not support such "dotted name" qualification directly, but instead uses
the functional form, y(X). To permit the dotted-name notation and user-defined subscripting, qualified
names are transformed in two steps. First, dotted names are eliminated in favor of a functional form:

<qualname).<identifier) dashdash> <identifier>((qualname))
where (qualneme) is any sequence of identifiers (including special identifiers), '.'s, 'S's, and
sequences of lexemes belanced and enclosed in parentheses or square brackets. The rule is applied
right-to-lelt; thus, for example

A.y dashdash> y(A)

0.9[s.t].f dashdash) i(g(0)[t(s)])
After all dots have been removed, square brackets are removed:

<term)[<expressionllst>] dashdash) &subscript((term).(axpressioniist))
Thus, the example aboVe becomes

Q.g[s.t].f dashdash> f(g(0)[t(s)]) dashdash) f(&suoscript(g(0).t(s)))
Note that the user may define the selector asupscn‘pt and hence may specify the access algorithm for
a type.

3.4.3 Automatic Introduction of Semicolons

The effect of the following transformation is to eliminate the need for explicit semicoions to separate
declarations or statements when those semicolons would (all at the end of a text line. According to the
syntax in this report, certain phrases are separated from each other by semicolons, in those cases
where the final iexeme on a line could end such a phrase, e.g..

the compiler automatically inserts a semicolon between the two unless, on the basis of preceding
symbols it is possible to determine that doing so would render an otherwise syntactically valid program
into an invalid one.

3.5. Special literals

Certain well-established literal denotations exist for some types (e.g., integer, real, boolean).

3.5.1 Syntax

<speciai iiteral>
<unsigned integer>
<unsigned real>
(unsigned rationai>

<unsignedinteger> | <unsignad raal> l <siring> l <booiaan> i <radix>

(unsigned rational>[E<scsie-iactor>}' l <unsigned inleger>€<scala-lector>
<unsigned integer>.<unsigned integer>

(4-)‘(unsigned intsgar>

<string> '<any sequence oi characters with all quotas doubled>'
<boolean’ ::- true | false
<radix> ::- (<alphanumoric>)‘-<alphmumeric>

3.5.2 Examples



HTML translation in progress

"He seid,"“Hal"""

3.5.3 Semantics

(radix) Ilterala are 'of type rawstarage. The (alphanumeric) following the "it" character specifies
the representation base. The value: of the ulphanumerlcs are interpreted as follows: 0-9 denote 0-9,
A-Z denote 10-85, n-z denote 36-61. Note that 0. 1 and ' (zero, an, and grave) are not legal baae


HTML translation in progress

Chapter 4
Program Structure, Expressions and Statements

4.1 Program Structure, Blocks

A compilation unit may be either a block or a set of declarations, if it is a block. It is a “program" In
the traditional sense dashdash a stand-alone computation. If it is a set of declarations, the scope of the
declarations is system-dependent.

4.1.1 Syntax

(compilation unit>

<exec decl iist>
<exec decl>

begin <bloclt> eLd | <exsc geci list)

(<exec dsci lisip)‘ (<stmt>); h)“

{ <exsc decl> );

<var deci> | <¢onst decl> l <proc deci> | <lorm dad) I <laoei daci>

4.1.2 Semantics

A block specifies a computation whose effect is as though the following order of execution were
observed: '

1. Elaborate the declarations in the order given (see 2.2 and 5.5).
2. Elaborate the statements (<stmt>s) in sequence (aside from exits; see 4.9).
3. Destroy the objects created in 1 in the reverse order of declaration.

The scope of all declarations in a block is the text of the block, where not superseded by nested

4.2. Expressions and Statements

Expressions and statements designate actions to be performed. Their elaboration results in changes
In the execution state of the program. Expressions differ from statements only in that their elaboration
may "produce values'l as well as performing other actions; statements only perform actions. For
definitional brevity and convenience, ovary expression is considered to be a statement, but not
conversely. When an expression is used in a context requiring a statement, its "value'I is discarded.

Somewhat more precisely, the "value produced by an expression" is an object resulting from its
elaboration: the type of this object is uniquely determined by the rules stated in the remainder of this
chapter. This resulting (unnamed) object exists until any immediately enclosing expression or
statement that uses it has finished execution.


HTML translation in progress

4.2.1 Syntax


(invocation) I (conditional expression) I (value expression) I
<with expression> I <first expression>

<stmt> ::- <expression> I <loop stmt> I <exit stmt) | <null stmt> I
<inner stmt> I <labeled stmt> | <assert stmt>
<labeled stmt> ::- <identifier> : <stmt>

4.2.2 Semantics

Statement labels are used by salt statements (section 4.9). The effect of an exit
statement is to force control to the point immediately following the labeled statement whose label is
used in the exit. Labels must be declared (see section 5.4) and may be used to label only
one statement within the scope of their declaration.

4.3. Invocations

4.3.1 Syntax

(invocation) (special |il§rai> I (simple invocation>I<aciuals>}‘ I (<invocation>)
<actu=ls> (l<uluil>}.)
<aciual> (expressiov I <type ducriptiorv

<simple invocation> (<idenlilier>€ )‘ (id-11min» | (special idontilior>

infix and prefix operators fall under this syntax by the rewrites of section 3.4.1. Subscripting,
denoted by "[...]“, falls under this syntax by the rewrites of section 8.4.2. Note: (special identifier>s
may not appear in source programs; they result only from these rewrites.

4.3.2 Examples

The most obvious <lnvocation>s are those denoting routine 'calls", 0.9.:
in addition, however, (invocations) result from the rewrite rules for lnfix operators and subscripting,
&:=(a, &¢(b,c))
&:I(x, &subscript(v.i))
Finally, <invocation>s occur as part of type descriptions:

4.3.3 Semantics

A simple invocation may designate a type, an object, or a routine (a procedure or selector) as
indicated in chapter 5, identifiers may designate multiple entities in any given context
(operator overloading), so some means of reaoiving the conflict is necessary. An identifier may be
qualified on the left by the name of the f_or_m containing its definition; such qualifiers are separated by
"s". Alternatively, the proper definition may be determined by examining the types of the actuals dashdash
that is, by choosing that definition for which type checking (section 2.4) succeeds, it is an error if the
compiler cannot disambiguate statically (l.e., at compile—time).

Assuming that the entity designated by G is uniquely determined, an invocation such as:
denotes an elaboration and possibiy a resulting value as follows:


HTML translation in progress

1. The actual parameters, ei, are elaborated in an undefined order. An el designating a routine
without an argument list designates that routine, rather than the value resulting from its
execution. The results of this elaboration are objects, types, and routines (see section
5.5 for the evaluation of partial types).

2. The number of formal parameters of 6 must be it (n20). The actuals must match the formals
of G (see section 2.4); it is an error if they do not.

3. Each formal parameter of G which designates a routine (as in "f:proc(...)"), a type (as in
”Tzform"), or a reference parameter (as in "w x:..." or "const ) is bound to the
corresponding e, (also see section 5.7).

4. Each object formal (see 5.7) with an empty (binding) is treated as if it were
specified const (see below).

5. For each formal identifier. Ir, designated to be a const parameter (see section 5.7),
Update(k) is made empty. For all other i: bound to objects. Update(k) is derived from the
type description of the formal parameter.

6. w and const parameters are checked for posaible overlap (see section 2.1-), in order for
the (invocation) to be legal it is necessary that either '

there is no overlap between an actual parameter that stands in a m position and any
other actual in either a v_ar or const position.

all overlapping positions are designated alias in the formal parameter specifications.

7. For each formal identifier, k, designated to be a copied parameter, a new object of the same
type is instantiated. The values of the actual parameters (see sections 5.6 and
5.7) are copied into these variables from the corresponding e, using the "Ens"
procedure defined for that type: it is an error if the '81:" procedure is not defined for the

8. if G is a routine and returns a value, or if it is a selector (see section 5.3), its
definition contains a type description which specifies the type of its result. This description
is elaborated, if G is a vproc or m, an object of the type is instantiated to receive the
"value" that will be returned, if G is a selector no object is instantiated; the type
description defines the type of the object whose (generalized) address is returned. Note
that a vproc or m must specify a full type for the result; a s_el need only specify a partial

9. If G is a routine its body is elaborated with the established bindings. If G Is a type
description either an instantiation or a matching is performed, depending on the context.

10. Any auxiliary objects (i.e., copied parameters or actuala which are themselves result
objects of procedures) are deallocated.

It should be noted that, by the rules above, the invocation of a parameterless procedure, P, is
necessarily written "PO".


HTML translation in progress

4.4. Conditional Expressions

4.4.1 Syntax

(conditional expression) dashdash- <if expressiun> l <caso expressien>

<if expression) as 1 <expression> thgn <block> ( e_li1 prressiorw thgg <block> )‘ {alsg <block>P fl
<case axpression> an 5252 <expressign> 91 «as» ”Log <ean> )‘ ( mwlock) 1" gsa;
<case> ::- (<expression>). :: <black>

4.4.2 Examples

E a[l])max then mexp := i; mix :, e[l] fl
y := i1 x>z then x else 2 fl
case K: fl
1100:: MB :5 C[EA]; R := R+MB e_lo_1.
sue M8 :3 C(EA]; a := R-MB Lat
MUL:: MB 1: (:[EA]; n :s R-Ma Ling
T := case n o_t 1::MALE 5L0! 2::FEMALE figflEUTER g

4.4.3 Semantics

Conditional expressions denote expressions and statements to be evaluated conditionally. Such an
expression has a value if

a. All (block): in l! are single expressions.

b. All these expressions are of identical type (this type becomes the type of the expression).

C. A" else clause is present.

The expression
I131 22281 weMSZ-uwsnmsneesnn a
is equivalent to
u 61 m 51 L's:
u 32 men 52 922

ii an then 5n else Sn” 3!


In the expression
E 3 2E1 51 i“. 52 E
B must have a result of type boolesn, and the elaboration of 3 must not have observahle effects. If
the value of B is true. 51 Is evaluated, otherwise $2 is evaluated, if the E expression occurs in a
context requiring a value, the value is that of the expression chosen (by the rules above. 51 and 82
must be simple expressions of the same type), in the absence of an gLs_e clause. 82 Is taken to be

skip (see section 11.10).


HTML translation in progress

In the expression
case E0 o_f
E11. E,n1::s1eior
E21, 52,12 :: $2 elof

En”, .... Emnm :: S"I else


Eo, E1 1 . .... Emn must all be expressions of the same type. E0 is evaluated. The EU are evaluated (In

error if there is no such operator. The evaluation of E0 and the Eu" must not have observable effects.
As soon as a match yields true (say with E”). S, is evaluated, if all matches fail. Sm” la evaluated.
Exactly one black 5| is evaluated for each correct evaluation of the fig expression. The value of the
g expression is that of the SI evaluated (again, each 3, must be a single expression).

4.5. Value Expression

4.5.1 Syntax

<value expression> ::- valgg’ <idantiliar>{:<obj type>)' c_i <black> LO

4.5.2 Examples

8 :3 value yrint o_f y:=0; fl x:invec(A) E yzlyox E f_o
value A o_f Munge(A.48) Le

4.5.3 Semantics

value x:T o_f S 19
the variable x (whose scope is S) is instantiated and S is executed. If ":(obj type)“ is omitted, as in
value x o_f S 19
the existing instantiation of x is used. In both cases, the result of the m expresslon is the object

4.6. With Expressions

4.6.1 Syntax

<wvth expression) ::- wit <with list) in <block> g
<wilh list) ::- <identiiier>5invocation> },

4.6.2 Example:

with Z:A[i].son[k] l2 Z.age :- O; Z.number := k 1i
wlth R:x.y.z, Q:x.y.w i_n m s:T; s := 0; Q :l R; R :l a n_i


HTML translation in progress

4.6.3 Semantics

A E expression provides a local shorthand for complicated invocations. The phrase
w xm in s 1'
causes elaboration of Fl, binding of x to R, and elaboration of S with that binding, if the <block> is a
single expression, the EL“ expression yields a value (the value of the <block>).

4.7. First Expression

4.7.1 Syntax

<first expression) :dashdash firsi<tempiala> sgghthat prressiom (ihgn‘biocv). (elgg <block>}' fl
<temp|ate> ::- <identiiier> irom (<identiiier>:)‘<type description) | <identiiier> from <irwocstion>

4.7.2 Examples

first i from upto(‘l ,n) suchthat A[l])max then max :: AU]; jmax :I i E
y :I first x from invec(A) suchthat x>max then x else 0 fl

4.7.3 Semantics

The fir—st expression invokes the generator specified in its template (see section 5.1 1) to
produce a sequence of values. These values are tested in turn by the suchthat clause, which must be
a boolean expression and which may not have observable side effects. If the fir—st expression

Lrst x M 9:0 suchthat B M S1§ls_e 82 fl
occurs in a context where a value is not required, its semantics are precisely those of the statement

L1: w
L2: Pm
11! 9:0; &start(g):
E &done(9) M &finish(g): i332 L2 Q
L": x:&value(g) in i_f_ B th_e_q s1;&finish(g); Lea—vs L1 g [11
£n_d L2
gn_d L1

where &start. 8-done, etc, are provided by the m (or generator) 0 (see also sections 4.8
and 4.9), it either the m or the 55: clause is absent, it defaults to 35L;- (see section
4.10). If "gt" is absent, an elsewhere unused identifier is substituted by the compiler. If the
full type in the template is absent, the declaration (v_a_r 9:0) is omitted; in such cases an existing
instantiation (namely "g") is used.

Note that the statement 52 in the expansion above is outside the scope of the declarations of g and
x: neither of these may be referenced in $2.

lf the first expression occurs in a context requiring a value. 51 and 52 must both be present and be
single expressions of identical type (say T), in these contexts, the semantics are precisely those of
value t:T o_f first x from 9:0 suchthat B then t:= 51 else tzlsz fl f_o


HTML translation in progress

4.8. Loop Statements

4.8.1 Syntax

<ioop strut)
<simpie |oop>
(while simt>
<for simt>

(simpie locp> I (while stmi> l <lor stmi>
d_9_ <block> g

wniig <expression> <simple loop)

Lo_r <iempiaie> (simple ioop>

4.8.2 Examples

fl x=y M exitloop fl
Ex)yth£x:=x-y flymy-xfl

while xyénil E P(car(x)): x := cdr(x) E
E x from lnvec(a) Q x :3 O E

4.3.3 Semantics

The simple loop; "g S E”, executes S repeatedly; it will terminate uniy if an exit command (see
section 4.9) is executed. The while loop. "while B d_o s g", is semanticaiiy equivalent to

d_o _ n_0t(B) mi exitioon fl; 5 o_d
The M loop. "m x M 9:0 3 S 3:5", is semantically equivalent ta
a 9:0; &start(g)

E &done(g) m exitiooa g
m x: &value(g) iii S 1i
A: in the E expression (section 4.7), if “g:" is absent, an elsewhere-unused identifier is substituted
by the compiler. If the full type in the template is absent, the declaration (fl 9:0) is omitted and an
existing instantiation is used.

4.9. Exit Statements

4.9.1 Syntax

<exii simt> ::- My]; [ mad-ntifiev

4.9.2 Example:

leave L
See aiso sections 4.8 and 4.7.


HTML translation in progress

4.9.3 Semantics

The statement "leave l.“ occurring within a statement labeled "L" (or a routine named "L") causes
evaluation of the innermost such statement (routine) to terminate; execution resume: at the point it
would have if the statement (routine) had terminated normally. (Note: if the relative nesting of the
labeled statement is such that, had the leave not been executed, objects would have been
deallocated and final clauses executed, these same doaliocation actions and finalization: are
performed in the same order as part of the leave.)

An exitlooo causes termination of the innermost loop statement (d_o, whlle, or E, section 4.8)
containing the exitloop.

4.10. Null Statement

4.10.1 Syntax

<null strnl> :2- skig

4.10.2 Semantics

The null statement does nothing.

4.11 Inner block

4.11.1 Syntax

<inner block> ::-' hegin (block) m l mm<hlock> endgi {<idanliiilr>)'

4.11.2 Semantics

The declarations and statements oi the block are executed as given in section 4.1. If the optional
Identifier is present, it must match the label of the inner block or the name of the routine whose body is
the inner block.

4.12. Assert Statement

4.12.1 Syntax

<assort stml> ::- asgerx (assertion)

4.12.2 Examples

d_q assert (GCD(X.Y) = GCD(sO.y0) }:
E x=y gig} exitloop fl

"W ‘ in” m" f” 'm " “a" W"


HTML translation in progress

4.12.3 Semantics

An assert statement indicate: a condition that must be true when control passes through the
statement. It has no sementlc effect. The syntax of (anenlon) Is not specified by the language
(other than that the assertion lax! must be enclosed in, and balanced in brackets, “(...)"). It I: the
province of a verifier or verifying compiler only.


HTML translation in progress

Chapter 5

Declarations define routines (proc, vproc, func, and gel declarations) and classes of types (form
declarations), specify the instantiation of objects (v_ar, const), and bind identifiers to these entitles.

5.1. Scope of Declarations

The scope of a declaration dashdash the program text in which the binding it establishes is valid dashdash depends
on the kind of declaration and the place it appears, in the sequel, normal Algol scope means the
innermost block containing the declaration, including all blocks it encloses that do not redefine the
identifier. Restricted Algol scope is the same as normal Algol scope, but excludes the text of routine
and EL! declarations.

Generally identifiers naming routines and fggn—s obey Algoi scope rules; identifiers naming objects
(l.e., variable names) obey restricted Algol scope. Thus, no free variable names appear in routine or
M bodies; all variables are either locally declared or passed in through the parameter list. A few
additional scope restrictions are discussed later.

5.2. Auxiliary Declarations

Any declaration may be preceded by the keyword EE’ identifiers defined in such declarations may
not be used (except within the assertion language). Auxiliary declarations serve as modeling tools in
the specifications; the entities described by such declarations may or may not exist in the
implementation, if such entitles do exist, they may be implemented in a manner different from that
described in the 2115 declaration. (Note, however, that the clause g_s_ specified may be used in an
implementation to force precisely the representation appearing in an 5111 definition of an entity).

An auxiliary declaration of a boolean-valued function, for example, might be conveniently used to
express a condition that is useful for verification or specification purposes. No obligation to actually
implement this function (whose implementation might be undesirable or impractical in some
environments) is implied by the a): declaration. Consider, for example, the M:

form DirectedGrapMsizezint) i3

aux func lsTree(g:DirectedGraph):boolean
post { returns true lit 9 is a tree ):

end DirectedGraph;
This form provides the predicate "is-Tree" which test: an arbitrary directed graph for treeness; since
the predicate is specified aux it can only be used in specifications, not in code.


HTML translation in progress

5.3. Remote Definitions

Occasionally the detailed implementation of an entity (variable,

point remote from its declaration. The following important cases arise:


forward: It may be necessary to mention an entity before is defined; this is logically
necessary in mutually recursive routine and form definitions. A forward indicates that the
required definition appears later in the current program text.

2 specified: in the implementation of a form it may be desirable to define an implementation
of an entity to be identical to its specification; such definitions are denoted a_s specified.
Somewhat similarly, a form implementation may mention an (object) parameter of the form,
describing it a specified, to denote that a run-time representation of the parameter is to

external(<system specs»: The definition of some entities may be defined external to the
present program text, e.g., on a "file" or a "library”l supported by the host system. In such
cases the entity may be defined as external. The <system specs) is a system-dependent
notion (and syntax) that describes the place where the definition ia to be found (e.g., in a
particular "file").

5.4. Label Declarations



<labal deci) 7:- lgbgi <idantilier iiat>



label L1. EXIT, Rethink;



routine, or form) may appear at a

Labels, like all other identifiers, must be declared before use. A label may be 'placed" (used to label
a statement) only once in the scope of its declaration.

5.5. Object Declarations


War deci>
<censt decl>


<obi deci group>
<obj lype>
<init fin clause>


<aux> m (we; dac! group>i<inil ii." clausvl'}:

<3ux> cons? (<obj deal group> (<init lin clausa>)' i Qunsl assianflf
(aux ‘

<idenlifier lisf> : <obj iype>

<type description> l figgeg’ligd

- <expression> [ (in_it<slml>)' (final <slml>)‘

<const assign) :z- (idenlilier iisl> - express-om


HTML translation in progress

5.5.2 Examples

!_a_r a.b.c:int, g:reai
fl const azint = 5
v__ar lNF~f‘Ie(vector(mumbie.14325)) i_nl_t open(iNF)
fl q,x.r:§ specified
v_ar Q:queue(int) M newm) m destroy(0)
const ADD=0. SUB=1, MULTIZ

5.5.3 Semantics

Object declarations may occur inside form declarations or in blocks: their meanings in the two
contexts differ. See section 5.9 for a discussion of their meanings in form declarations.

In blocks, object declarations have restricted Aigol scope (see section 5.1). Semanticaiiy, constant
declarations ((const deci>s) differ from variable declarations ((var decl)s) oniy in that, outside the
initialization and finalization clauses. Update(c) is empty for c a constant; for variables the update set
is determined from the (type description).

The (obj decl group>s within an object declaration are processed in unspecified order (note.
however, that declarations are processed in ieft-to-right order; thus the programmer may impose an
ordering if that is appropriate). For each group, the full type is evaluated, and for each identifier, a
new object of that type is instantiated and bound to the identifier, if an i£i_t_ clause is present, It is
executed. The declaration

. . .x.y.z:T=E
is equivalent to .

. . .x.y.z:‘i’ m x:=y:=z:IE
if ":T" is absent (from a constant decimation), as in ”SEE ass“, the type is that of the expression to
the right of the equal sign.

A final clause, if present, is executed just before deallecation of the variables or constants with

which it is associated. Deaiiocation is always in reverse oi the (possibly unspecified) order of

Objects may be designated "5 specified'l only in form implementations (section 5.9). This
indicates that the (type description) is to be copied from the form specifications.

An <init fin clause) in a constant declaration can be omitted only in the specifications part of a form
(see section 5.9).

5.6. Evaluation of Type Descriptions

(type description): are syntactic entities which appear in object declarations and formal parameter


HTML translation in progress

5.6.1 Syntax

<type description> ::- <simpla invocation> ( ( (dermal web}: ) }' (<updaia sai>}’ l
?<identiiier>{<updaia ssh)’

<formal qual> ::- <expression> l ?<idantiiiar>(<updala ssi>}' I (<idaniiiier>:)‘ <iype descripticn> I
w b

<updaie sei> :z- < ( <idaniliier> I <speciai identiiier> }, >

Note that the outer <)'s in the deiinition or (update set) are part of the language, not metabrackets
(see examples below).

5.6.2 Examples

vector(raal.1 .10)

5.6.3 Semantics

The (simple invocation) (see 4.3) must designate a unique form ("3" qualification allowa duplicate
nested form definitions). Disambiguation on the basis of argument types is not performed.

Elaboration of a (type description), T(e1,....en)(p1,...,pm>, proceeds as follows13 :

1. The el are elaborated in an undefined order. The results or this elaboration are objects.
routines, and types. The following special cases should be noted:

a. The elaboration of w is yn_k.

b. The elaboration of ?Identifiers implies an implicit binding: it is illegal if this is not in
the context of e formal/actual parameter matching.

2. The number of formal parameters of T must be n (n20). The actuals must match the formals
of T (see section 2.4), it is an error if they do not.

a. Each object actual is handled as in section 4.3.3.

4. The sequence of routines, types, objects, and fl markers produced by the preceding
becomes the Dual property of the result type. T is the Base type (see section 2.2). The p,
become the update set.

The (update set> defines the update set of the type description (see 2.2). The listed identifiers
must be names of routines declared with the base type. Only these routines and routines with no visible
effects may be applied to the object within the scope covered by the declaration in which the type
description appears. In the case that the update set is attached to an identifier or a (type formal).
the llsted identifiers must be further specified in an "assumes clause' (see 5.12) unless they


13Note that an implementation may require compile-lime elaboration oi those type descriptions used as formal
parameter specifications.


HTML translation in progress

are (special identifier>s such as "an". The assumptions about (special identifier)s are uniform and
-are included in appendix C. If no (update set) Is given it is assumed to contain the full
update set of the type; the (update set) "0" denote the .empty set.

5.7. Formal Parameters

Certain entities dashdash forms and routines dashdash can be parameterized. Formal parameters specify these
parameterlzations. The process of determining whether a given sequence of actual: conforms to the
sequence of formal parameters is known as matching or type checking. This process binds actual
parameters to the corresponding formal parameters. It may also cause certain implicit bindings of
identifiers marked with a “?" iexeme in the formals; these identifiers are impllcif parameters with the
same scope as ordinary formals. The implicit bindings are in effect whenever the explicit bindings of
ordinary formals are.

The scope of a formal parameter to a routine is the text of the parameterlzed declaration. In the
"restricted Algol scope" sense. That is, the scope of a formal does not include routine or form
declarations within the parameterized routine text.

The scope of a formal parameter to a M is at most the text of the parameterized EL“, declaration:
it is also subject to "restricted Algoi scope", in addition, unless egpllcitly redeclared in the M
(specifically, redeclared as specified), the scope of Log formals is limited to the specifications and
object declarations (including L clauses) of the 1313 other than shared objects.

5.7.1 Syntax

<torma|s> ( {<r0ulina form-P I <binding><obj formal) l <type furnish): )

<routine formal> <formal id list) w <parms> | <iormai id list) (vprgs | Luggl gel)“ parrns>
<bindins) i 5221 i i flef'i m_ns_t I w.) )‘

<formal id iist> <identilier iisl> :

(obj iormai> :z- <formal id iist> <typa description)

<type formal> ::- <formsl id iist> { Lem I m }(<updata sat>)'

5.7.2 Examples

(const x:Ti , fl q:?T2, copy r:vector(?T2.1.n))
(Tzforrn, h:proc(x:real):int)

5.7.3 Semantics

Formal parameters give the specifications of allowable actual parameters and provide local names for
these parameters. A (routine formal) indlcates a parameter position to be filled with a procedure or
selector. A (type formal) indicates a position to be filled by a type description. An (obj formal)
indicates a position to be filled by an object. The association of actual parameters to formals is
determined positionally.

The specification of an object parameter may be preceded by a qualifier that controls the binding of
actual to formal; the possible qualifiers are c_o_x. EEK! v_ar, and __s. The qualifiers coast and v_a_l:
denote "by reference" parameters; in both cases the parameter name is bound to the actual parameter
object, const parameters (like names declared in £o_n_s_t object declarations), have an empty update

set. As specified in section 4.3, the qualifier copz indicates that a local object is to be instantiated


HTML translation in progress

and initialized from the actual by copying using the &:= operation defined for the type. The update set
of copied parameters is set to empty, hence they may be used only for input. The qualifier % has no
semantic effect, it indicates that a reference parameter may overlap other reference parameters;
unless the w qualifier is present, overlapping reference parameters are prohibited.

For type formula the actual type description must be a full type if the formal is specified as a form, it

may be a full or partial type if the formal is specified as a pform.

qualified by alias, the compiler assumes that the semantics of cans! and copy are identical14 dashdash hence
the compiler is free to copy const parameters if it seems desirable to do so. This statement is not true
for forms or in the presence of alias, and the optimization may not be performed in those cases.

The notation

is short for
e:T, b:T, czT

identifiers preceded by ”?" are implicit formula. One binding is established for the identifier during
matching, no matter how often it appears. It is an error if it is not possible to establish such a binding.
Ail instances of the identifier inside a given (female) list must be preceded by "?".

5.8. Routine Declarations

Routines encapsulate computations. A routine (w, M' fit—no) may or may not return a result
object. If it does, the update set of the compiler-generated name bound to the returned object is
always null; there can be no effects on a procedure result. A seiector always has a result and must
not have effects; unless explicitly restricted, the (update set) of a selector result ia the full update
set of the base type. Except within M specifications (section 5.9), routine declarations
have normal Algol scope.

5.8.1 Syntax

<routine deci> .., <vprcc decl> I <aro¢ dacl> | <sal daci>
<vproc daci> ::- <aux> (iniinei' {vgroc l igngkrouiin- id) <v parmv <pre post) <assumes>

(<routine body>}'

<proc decl> <aux> (inlina ‘ grog <rouiina id> <parms> <pre post> <assumas> [<routina body>)"

<sel decl> <aux> (inlingi' abroutina id><v parms> <pra post> <aasumas> (<rouiina body>)"
’<routine id> <idantiiier> l <spacial identifiar>

<parms> (<icrmsls>}’

<v perms) {<fermaiv)‘.<type descripliav

<pre> [g <assarilon>-,)"

(pre post> <prs> {M <assertion>;)'

<routine body> i3 <simi> | Efisgecviisd l i; forward I ngigrngl (<sysiem spec?)

14 This assumption is valid only so long as user—defined assignment operators, " :I', preserve the intended
meaning. The compiler cannot enforce the correctness of any usar~deiined operation, and specifically not that of


HTML translation in progress

5.8.2 Examples

vproc f(x:int):real
grg (abs(x)<maxintreai);
I3 floet(x);
inllne s_ei triang(v_a_r A:vector(?T.1.?n), l,i:int):T
i-s_ A[i'(i-1) _di_v 2¢j]
m empty I3 5 specified

5.8.3 Semantics

Selectors (declared s_el) name objects. Procedures (declared HES) produce effects but do not
return values. Value-returning procedures (declared 1mg), may produce effects and also return
values (actually objects). Functions (declared 1%) are semantically equivalent to vproc's except that
they are deterministic15 and do not have observable effects on their parameters. The (sum) portion
of the (routine body) of a vproc or m must be a single expression of the type returned by the

The qualifier inllne has no semantic effect. It indicates that the compiler should make the declared
routine "open" dashdash i.e., produce a copy of the object code at each invocation site.

The pre and post clauses have no semantic effect, but are specifications of the routine‘s behaviorl
The pre clause gives conditions which will be true at entry: post gives conditions at routine exit (the
keyword result is conventionally used in post conditions to specify the value returned).

The routine body may be absent only in M specifications (see 5.9). It may be given "as
specified" only in m implementations; this indicates that the body is to be carried down from the
specifications. The routine body may be specified as forward if its declaration appears later in the
same (block). The body may be specified as external if the text of the definition is to be found in the
system-dependent entity specified by (system specs).

The formal parameter lists and result types must be omitted in form implementations if the same
routine (name) is declared in the specifications of the form. They are copied from the declaration of
the routine in the specifications.

The assumes clause (see section 5.12) declares generic parameters (implicit and explicit).
Throughout the text of the routine declaration, only those properties declared in the assumes clause
are used in testing syntactic and semantic validity.

As stated previously, identifiers that name objects observe restricted Algoi scope. Thus, the body of
a routine cannot access objects declared outside itself unless they are passed through the parameter
list. Also, as stated previously, the objects named by distinct formal parameter names cannot overlap
unless they are explicitly qualified with a_ii£_s_.


15 That is, invocations With equal inputs yield equal oulpuis. More precisely, for F to be a func, &-(A,B) mus!
imply &-(F(A).F(E)).- ii 84- is not defined, invocations with identical inputs must have identical ouipuis.


HTML translation in progress

5.9. Form Declarations

Forms define classes of types. There is one form declaration for each base type, identifiers
declared in form declarations have normal Algol scope.

5.9.1 Syntax

<form decl>
<form body)

<aux> lorm <idenliliar>l<lormais>)' <pra><assurnas> is <lorm bpdy>
(<specs>}'(<impl>)' m (<identifiar>)‘ | <abhrev body> l forward I external
“system Specs» 1 5mm

<specs> sages ( <var decl> [ (other farm decls> h. .

<impl> i_n_wp_l ( <shared> <var decl> I <olher iorm decls> };

(other form deals) <routine deci> i <iorm dezi> | <axiorn>i <shared> <<cnsi decl>

<shared> shared”

<axiom> invariant <usertion> I initially <asseriion> | axiom <usertion> [ regmag

<assertion> I M1. <identiiiar> <assartion>

5.9.2 Examples

m F(T:m, xzint) i_s

fl mxint:
vproc p(f:F):T fl (m<x) po_st {m>x);

const mg specified
fl mg specified;
vproc o is F.m:=F.xo1;

5.9.3 Semantics

The memes defined in the specifications (<specs)) of a M are available outside the form
declaration. The scope of these names is the same as if they had been declared immediately outside
the form, except that v_ar and const declarations become routine declarations as described below. The
scope of the names in the specifications does not include the implementation (<impl>). Note, however.
that all these names must be redeclared in the implementation The implementation may be omitted if
the M declaration appears as part of the specifications of another form. The specification may be
omitted if the declaration appears in the implementation of another form, in which case it la copied from
the specifications of the containing form.

specs and (var deals) of the (form body) unless they are explicitly redeclared (a_s specified) in the
i_m_pi, in the latter case a run-time representation of these objects becomes part of the implementation
of objects instantiated from the m, in such cases it is also possible for these names to be mentioned
(again E specified) in the specs, and hence to be externally available. These redeclarations in the
m and specs must be compatible with the (binding) of the formal parameter; that is, an identifier
redeclared var must also have a var (binding) (an identifier redeclared const may have a var, const, or
copx (binding). _ -

Objects declared in a form usually become the concrete components of the objects that result from
instantlating the form; there are thus distinct instantiation: of these objects for different instantiation:
of the form. An exception occurs when a declaration is prefixed by by the modifier shared: A single


HTML translation in progress

instantiation of a shared object is common to all instantiations of the form. In particular, it makes
perfect sense to define a shared const of a given type within the dailnition of that type. Such a
constant functions as a named literal oi the type.

<Axiom>s have no semantic effect, but provide further specifications.

Non—shared constant and variable declarations within io_rln_ specifications are shorthand for certain
procedure and selector declarations. That is.
form T”.
fl P:Q
const MR
is short for
form T...
s_e_l P(v_ar_ t:T):Q
func A(t:T):R

in the implementation, object declarations again become selector and procedure declaration: as
follows. When an object of base type T is instantiated, the object declarations in its implementation
are elaborated as usual (and the in_it clauses are performed); This results in a set of newly created
objects which become the concrete components of the object being created. These components may
be accessed within the bodies of the routines in the implementation by using implicit selectors
(procedures) with the same names as those given in the object declarations. Thus, we can write
form T...
w x:int;
P'_°E 1(GzT) i3 0.x
That is, inside f, "x" is treated as a selector on objects of type T and is applied to the formal
parameter. Q, to access the xscomponent or the particular actual. Note in particular that "x", like all
object names, obeys restricted Algol scape and hence is not inherited by the body of the 51:5, f.

5.10. Abbreviations

Abbreviated form body definitions are provided for two commonly occurring kinda of abstractions,
"records" and ordered "enumerated” types.

5.10.1 Syntax

<abbrev body>
<record type)
(enumerated type)

(record type) i «numerztsd type)
record ((<obj decl zrbuy), )

gngmgral§g( <Idenliflar list> )

5.10.2 Examples

record (
record (x,y:int, load:real, thetazradians)
enumerated ( red, blue, green, purple, bardot )


HTML translation in progress

5.10.3 Semantics

The declaration
m H...) i_s record (
is semantically equivalent to
m F(...) E
fl d1. ..., dk;
M cons(d1, ..., ck): F(...);
m &=(lhs.rhs:F): boolean;
vproc MAE lha.rhs:F): F(...)-.
w d1. ..., dk;
m cons i_s_
value v:F(...)
o_f m assign to components at v m t_o
fl &= '3 m compare components for equality fl
vprcc &:= E m assign rhs to ills component-by-component m
m F
In addition, all parameters of F are converted to "Identifiers" when they acpoar in formal parameter
lists of "cons". "&=“, or "&:=".

The declaration
form C i3 enumerated (i1....,in)
is semantically equivalent to

m c 1'2
shared const l1. .... ! distinct constants:
func 8.: ! equality test
vproc 81:: , l assignment
fu_ng min ...; .' minimum element (-i1)
m max ...; i maximum element (=an
w succ ...; ! successor (not defined on in)
func cred ...; ! predecessor (not defined on l1)
func card ...; ! cardinality of enumeration (=n)
func decode ...; ! converts element to its ordinal (a.g., decode(|3)=6)
func code I convert: ordinal to element (e.g., code(ZHZ)

! convert element to stringlet (its printname)

func unspell . - .I convert stringlet (printname) to element
generator gen ! generates elements in order (l1 In)
and C

5.11. Generators

Generators are specialized forms. They are useful for defining objects that will be bound to the
control variables of the m and flrst constructs (see 4.7, 4.8). (Any form may provide such objects.
but their use is sufficiently constrained by the language that special abbreviated syntax is provided

for defining forms intended specifically for this purpose.)


HTML translation in progress

5.11.1 Syntax

<forrn deci) :z- <aux> generator <Identilier> {<formals>)‘ : (type description) <pre> <assumes>
is (form body)

5.11.2 Example

generator upto(lb.uo:int): int I3
E {ubSmaxmt-l A leminint)
all}, yfl k:int=ub+1;
2‘2 for
(premise ISkSu A l([i..k-1]) (ST(k)) I([I..k])
mg i([]) (E k m g: upto(l.u) d_o sT(k) w i([i..u])}
E first
(premise P A lSkSu A (Vw)(lSw(k D pfl(w)) A #(R) (5100} Q
premise P A (Vw)(lSwSu 3 pfiflw) ($2) 0
conci P (USS—t k m g: upto(l.u) suchthat #0:) m 510:) 9B 52 fl) 0}

w k: g specified;
const lb,up, as specified.
func &dcne i3 g.k)g.ub;

proc amext i3 g.k+:=1;
proc &finish is g.k:=g.ub01;
endof upto
Note that in this example we have chosen to ignore statement and predicate parameters other than k.

5.11.3 Semantics

in order to generate loop control variables, I m must provide definitions for the routines &start.
annext, &done and &value. A definition or the routine &finish is optional, if no definition is provided for
&finish, the compiler will provide (1) an appropriate header. (2) the body ‘s_k_i£ in the specifications, and
(3) the body a_s“ specified in the implementation. Restrictions on the definitions of &dona, &start.
s-next, &finish, and &value are provided in appendix C.

A distinguished class of Liz-£5 defining objects for controlling loops is designated by the reserved
word generator and the syntax indicated above. This class is significant because the behavior of these
objects is sufficiently constrained to be specified by a proof rule. Necessary properties of the
specifications of the generator routines can be derived from the proof rules and the constraints16 . As
a result, these specifications are not written explicitly, instead, proof rules for Q's-t and f_o_r loops that
use the generator are written as shown above. An instantiation of a generator may be used only to
control loop constructs for which it provrdes proof rules.

1'6 See ”Abstraction and Verification in Alphard: Defining and Specifying iteration and Generators' by Mary Shaw,
Wm. A. Wolf, and Ralph i. London, in Communication; citric ACM. August 1577, pp. 553664.


HTML translation in progress

5.12. Assumptions

Assumptions provide "skeleton" declarations for generic parameters and provide sufficient
Information to verify all uses of these parameters locall.y

5.12.1 Syntax

<aasumes> ::- (M <ionn dub):

5.12.2 Examples

assumes form T is specs func &=(a,b:T):boolean

5.12.3 Semantics

formal (see 2.4).

The following routine illustrates the use of assumptions and generic parameters:
1m equal'vaczors(x.y:vector(?T.?Ib.?ub)):boolean
assumes fcv_rm T E specs fix—no &3(e,b:T):boolean fl
I_s flag I M upto(ib,ub) suchthat xfijaiyfl] thfl false w true fl
This routine will determine whether two vectors, x and y, are equal so long as (1) the type of the
elements of the vectors. T, provides an equality operator and (2) the two vectors have the same upper
and lower bounds. An assumes declaration behaves as though it had normal Algol scope; in particular,

An informal Definition of Alphard 40

Appendix A
Collected Syntax

<letter> ::= A | B |... | Z | a |... | z
<digit> ::= 0 | 1 |... | 9
<alphanumeric> ::= <letter> | <digit> | '
<special symbol> ::= <basic symbol> | <operator>
<basic symbol> ::= begin | end | endof | ; | : | ( | ) | $ | :: | & |
if | then | else | fi | case |
of | esac | fo | with | in | ni | first | suchthat | from | do | od |
for | exitloop | leave | skip | assert |
var | const | aux | as specified | = | init |
final | unk | ? | proc | vproc | func | sel | label |
note | eton | ! | elif | elof | pform | while | > | < | . | # |
copy | alias | form | inline | pre | post | rule |
is | forward | external | specs | impl | shared |
invariant | initially | axiom | repmap |
record | enumerated | assumes | value | generator
<operator> ::= <binary operator> | <unary operator>
<binary operator> ::= ↑ | * | / | div | rem | + | - | < | ≤ | = | <> | ≥ | > | and | or | cand | cor | imp |
<assign op>
<unary operator> ::= + | - | not
<identifier> ::= <letter> {<alphanumeric>}*
<special identifier> ::= &start | &finish | &next | &done | &value | &subscript | &<operator>
<identifier list> ::= <identifier>,+
<special literal> ::= <unsigned integer> | <unsigned real> | <string> | <boolean> | <radix>
<unsigned integer> ::= {<digit>}+
<unsigned real> ::= <unsigned rational>{E<scale-factor>}# | <unsigned integer>E<scale-factor>
<unsigned rational> ::= <unsigned integer>.<unsigned integer>
<scale-factor> ::= {+|-}#<unsigned integer>
<string> ::= "<any sequence of characters with all quotes doubled>"
<boolean> ::= true | false
<radix> ::= {<alphanumeric>}+#<alphanumeric>
<compilation unit> ::= begin <block> end | <exec decl list>
<block> ::= {<exec decl list>;}# {<stmt>};+ {;}#
<exec decl list> ::= { <exec decl> };*
<exec decl> ::= <var decl> | <const decl> | <proc decl> | <form decl> | <label decl>
<expression> ::= <invocation> | <conditional expression> | <value expression> |
<with expression> | <first expression>
<stmt> ::= <expression> | <loop stmt> | <exit stmt> | <null stmt> |
<inner block> | <labeled stmt> | <assert stmt>
<labeled stmt> ::= <identifier> : <stmt>
<invocation> ::= <special literal> | <simple invocation>{<actuals>}# | (<invocation>)
<actuals> ::= ({<actual>},*)
<actual> ::= <expression> | <type description>
<simple invocation> ::= { <identifier>$ }* <identifier> | <special identifier>


<conditional expression> ::= <if expression> | <case expression>
<if expression> ::= if <expression> then <block> { elif <expression> then <block> }# { else <block> }# fi
<case expression> ::= case <expression> of <case> { elof <case> }* { else <block> }# esac
<case> ::= { <expression> },+ :: <block>
<value expression> ::= value <identifier>{:<obj type>}# of <block> fo
<with expression> ::= with <with list> in <block> ni
<with list> ::= { <identifier>:<invocation> },+
<first expression> ::= first <template> suchthat <expression> { then <block> }# { else <block> }# fi
<template> ::= <identifier> from {<identifier>:}#<type description> | <identifier> from <invocation>
<loop stmt> ::= <simple loop> | <while stmt> | <for stmt>
<simple loop> ::= do <block> od
<while stmt> ::= while <expression> <simple loop>
<for stmt> ::= for <template> <simple loop>
<exit stmt> ::= exitloop | leave <identifier>
<null stmt> ::= skip
<inner block> ::= begin <block> end | begin <block> endof {<identifier>}#
<assert stmt> ::= assert <assertion>
<label decl> ::= label <identifier list>
<var decl> ::= <aux> var { <obj decl group>{<init fin clause>}# },+
<const decl> ::= <aux> const {<obj decl group> {<init fin clause>}# | <const assign>},+
<aux> ::= { aux }#
<obj decl group> ::= <identifier list> : <obj type>
<obj type > ::= <type description> | as specified
<init fin clause> ::= = <expression> | { init <stmt> }# { final <stmt> }#
<const assign> ::= <identifier list> = <expression>
<type description> ::= <simple invocation> { ( {<formal qual>},+ ) }# {<update set>}# |
?<identifier> { <update set> }#
<formal qual> ::= <expression> | ?<identifier> { <update set> }# | { <identifier>: }# <type description> |
<update set> ::= < { <identifier> | <special identifier> },+ >
<formals> ::= ( { <routine formal> | <binding> <obj formal> | <type formal> },+ )
<routine formal> ::= <formal id list> proc <parms> | <formal id list> { vproc | func | sel } <v parms>
<binding> ::= { copy | { alias }# { const | var } }#
<formal id list> ::= <identifier list> :
<obj formal> ::= <formal id list> <type description>
<type formal> ::= <formal id list> { form | pform } { <update set> }#


<routine decl> ::= <vproc decl> | <proc decl> | <sel decl>
<vproc decl> ::= <aux> {inline}# {vproc | func} <routine id> <v parms> <pre post> <assumes>
{ <routine body> }#
<proc decl> ::= <aux> {inline}# proc <routine id> <parms> <pre post> <assumes> { <routine body> }#
<sel decl> ::= <aux> {inline}# sel <routine id> <v parms> <pre post> <assumes> { <routine body> }#
<routine id> ::= <identifier> | <special identifier>
<parms> ::= { <formals> }#
<v parms> ::= { <formals> }# : <type description>
<pre> ::= { pre <assertion>; }#
<pre post> ::= <pre> { post <assertion>; }#
<routine body> ::= is <stmt> | is as specified | is forward | is external (<system specs>)
<form decl> ::= <aux> form <identifier> { <formals> }# <pre> <assumes> is <form body>
<form body> ::= { <specs> }# { <impl> }# end { <identifier> }# | <abbrev body> | forward | external
( <system specs> ) | as specified
<specs> ::= specs { <var decl> | <other form decls> };+
<impl> ::= impl { <shared> <var decl> | <other form decls> };
<other form decls> ::= <routine decl> | <form decl> | <axiom>| <shared> <const decl>
<shared> ::= shared #
<axiom> ::= invariant <assertion> | initially <assertion> | axiom <assertion> | repmap
<assertion> | rule <identifier> <assertion>
<abbrev body> ::= <record type> | <enumerated type>
<record type> ::= record ( { <obj decl group> },+ )
<enumerated type> ::= enumerated ( <identifier list> )
<form decl> ::= <aux> generator <identifier> { <formals> }# : <type description> <pre> <assumes>
is <form body>
<assumes> ::= {assumes <form decl>},*


HTML translation in progress

Appendix B
Standard Prelude

The complete specifications of the types in the standard prelude will appear in a future technical
report. This appendix previews that report by listing the types to be included and summarizing their
main properties. This, together with the reader‘s experience and goodwill, should suffice to understand
the language definition.

The type definitions loosely referred to as the "standard prelude“ actually comprise three classes of
definitions. The primitive prelude defines operationally the basic notion of linear contiguous storage
and all of the common machine operations. The standard prelude proper includes types that we
expect to be implemented for all versions of the language, usually as a part of the compiler. The
Implementation prelude includes types that provide facilities of the underlying hardware, operating
system, or support environment of a particular implementation, in addition, types (such as real) which
should be defined for a large class of systems (but not all) are defined here, it is our intention that
whenever a particular implementation chooses to define a type given here, it follows our specifications
to the greatest extent possible.

B.1. Primitive Prelude

The RawStorage form supplies the fundamental abstraction of linear contiguous storage as
described in Chapter 1. Fetching and storing are defined for RawStorage objects of equal length. The
integer and bitwise boolean operations are provided for RawStorage objects of length one. In addition
we provide support here for the subsequent definition of forms such as collections and references, as
well as the ability to do storage management.

B.2. Standard Prelude

There are three major classes of types in the standard prelude. The sections below sketch the
major properties Of BBC".

B.2.1 Scalars

are unstructured; they’ possess values from a set designated (true, false). The customary unary and
binary functions are provided, along with assignment.


HTML translation in progress

Integers are restricted to machine precision. The standard prelude supports the customary unary
'and binary arithmetic operators on integers, the arithmetic relations, named constants to describe the
finite range of a particular implementation, assignment, and transfer functions to and from Stringlets.

B.2.2 Linear Structures

Two linear, homogeneous, fixed-length data structures are provided in the standard prelude.
Vectors may have elements of many types; Stringlets are minimally sufficient to support I/O

Vectors may have elements of almost any type (the type must be ailocatabla without special
restrictions). Any particular Vector, of course, contains elements of only one type. The length of a
Vector is fixed at instantiation time. A subscript selector for integer indlcea and a generator that
produces the elements in order are provided, if the element type supports either assignment or
equality test, that operation is extended to the entire Vector. There is a slice routine which returns a
subvector of the original vector (with the new origin forced to zero).

strlnglels closely resemble vectors of characters. The same operations are provided for stringlets
as for Vectors. In addition, literals are supported by the syntax of section 3.5 and an assortment of
special predicates on stringlets of length 1 is provided (lscharacter, IsLetter, lleglt, etc.). Transfer
functions to and from integers are also provided. Note that type 'charactar“ is not included in the
standard prelude; use Srrlnglers of length 1 instead.

B.3. Implementation Prelude

Certain other types appear in some fashion in almost every language. These types do not have
uniform specifications across implementations, but rather depend on the host machine, since we don't
want to require these for all systems, we cannot include them in the standard prelude. Instead, such
types are provided in an implementation prelude - a segment of the definition of each implementation
that is frankly machine-dependent. In addition, certain types which may not exist under all
implementations, pm which must have uniform specifications for those systems on which they do exist.
are included here.

The types defined here may provide direct access to features of the underlying hardware; they may
support special facilities of the environment or the operating system; they may slmpiy be data types
that are best supported directly by the compiler.

B.3.1 Scalars

Reels have the properties of hardware floating-point values. Unary and binary arithmetic operators
and relations are supported to the extent that the underlying machine allows. Constanta describing
floating point accuracy, assignment, and transfer functions to and from integers and stringlars are
also provided. There is NO mixed-mode arithmetic.


HTML translation in progress

B.3.2 Input and Output

The implementation prelude requires a minimal set of operations on flies or characters. This, together
with transfer functions to and from String/era, is intended to guarantee the availability of at least
primitive input/output facilities. It is intended that each implementation prelude provide such richer
support as is appropriate, provided such support is an upward compatible extension of the facilities
described here.

Eor_m [OF/1e supports sequential files of characters. Files are sequences at str/nglats of length
one. They are constructed by appending stringlus and decomposed into String/on. The available
operations are commands to open or close an File for reading or writing, to test the status of an File,
and to read or write a Strlnglat from or to an File. Note that file is an auxiliary M definition such
objects cannot be declared. IOFIIe, on the other hand, has a null representation. Hence it is not
meaningful to declare objects of this type.

B.3.3 Machine Dependent Types

These types may provide direct access to features or the underlying hardware or to special facilities
of the environment or the operating system.


HTML translation in progress

Appendix C
Special identifier Assumptions

A certain number of Alphard routines are used lor special purposes. Their definitions are thus more
constrained than has been indicated elsewhere in this report. These routines are distinguished in that
their names begin with ampersand ("an"); syntactically, they are (special identifier>si The routines are
invoked by specific language constructs rather than by ordinary routine invocation.

These routines are grouped into two classes. Generator rout/nos are invoked by the E and grit
Iteration constructs in the manner described in sections 4.7 and 4.8. Extensible operators are
effected by the intlx operator rewrite rules as well as by the subscript rewrite rule (see section 3.4).
Extensible operators include all operators named by (special identifier)s other than generator routines;
they can be overloaded by user-defined forms.

C.1. Generator routines

The generator routines are &oone, &start, annaxt. Mlnish and lwalue.

C.1.1 Use restrictions

The restrictions on the invocation of generator routines as an ordinary routines are intended'to
support two conflicting requirements. First, it is mandatory that a Lg: or fir—st loop body not be able to
use these functions on the object generating the loop control variable, it is, in general, desirable that
they not be invoked in other arbitrary places outside of loops either. It is, however, useful to be able
to use these routines in the definitions of other generators, specifically those which simultaneously
generate elements of two or more data structures.

The invocation restriction is thus that: &start. &next and Mlnish can only be invoked in the definition
of an &start. &next or &l‘inish routine of another generator: adone can only be invoked in the definition
of an &start, &next. &flnish or &done routine in another generator; &value can only be invoked within
another generator. This would seem to permit use of the same generator object to create control
variables in two nested loops. Any problems which this might cause for the generator object would be
detected as violations of sufficient independence of the object from the body of the outer loop.

(3.1.2 Definition restrictions

Suppose a generator named gen defines a type of object that provides a control variable of type t
for the "<identifier> M" construct. The generator routines must have header specifications

mi &done(g:gen):bool;
s_el &value(g:gen)zt;
m &start(g:gen);
proc &next(g:gen);
9193 &finish(g:gen);


HTML translation in progress

C.2. Extensible routines

The extensible routines are 8.1, a'. 8:], &div, alrenI. &¢(unary and binary). &-(unary and binary). &<,
&=, 5.), «Sand. &or, Mme, &not. &:= and &subscript.

C.2.1 Use restrictions

Extensible routines can be invoked either by uslng the infix operator rewrite rule or by using the
subscript rewrite rule (see 3.4). There is no loss 01 generality in prohibiting their invocation as ordlnary

C.2.2 Definition restrictions

Within m f, specifications of these operators must subaume:

func a.i(|eftperm:f.rightparm:t):t1;

func 8.‘(leftparm.rlghtparm:f):f;

func 8./(levtparm,rightparm:f):1;

func &div(leftparm.rlghtparm:f):t;

fune &rem(leftparm,rightparm:f):t;

func &+(Ieftparm,rlghtparm:l):f;

func &+(parm:f):f;

func 8dashdash(Ieftparm.rlghtparrn:i):l;

mi &-(parm:f):f;

func 6:<(Ieftparm,rightparm:f):l:ocl;

func a.=(leftparnwightparm:f):booi:

rune &>(ieltparm.rightparm:l):bool;

vproo &:-(ali£ m leftpannd, ias rightparm:f):i:

s_el &subsorlpt(alterdot:f,p1:t1. .. .pn:tn):t;
The compiler is able to enforce only the precedence and syntax of these operators. However, their
traditional use in mathematics raises other expectations about them; most people, for example,
presume "-6" is at least associative and possibly commutative. We strongly urge that the programmer
overload these operators only with operations that preserve those expectations; failure to observe
this convention may badly mislead the reader.


HTML translation in progress

Appendix D
A Complete Example

We now present a complete Alphard program. This program defines finite sera with a fixed maximum
size, then uses them in a small program. Several aspects of the program deserve special note.

Form FinSet defines one variety of sets. These sets must be homogeneous (l.e., all elements must be
of the same type), but the elements may he of any type that provides assignment and equality
operators. Thus FinSet is a generic type definition. The specifications of FinSet are stated in terms of
ordinary mathematical sets; the restrictions that apply to set: of type FinSet are explicit.

We assume the types of the standard prelude. Appendix 5. In particular, we use vectors, integers,
and the generator upto for integers. The main program defines an ordered enumerated type and uses
the generator that is automatically defined for such a type.

The names V and in used in the implementation of Finset are available to the bodies of the routines
defined in that form. V and in may be used as qualifiers on any objects of type FinSet that those
' routines receive as parameters. The names V and m are not available outside the form.

FinSet defines routines &+(union). &‘(lntersect). &:=(assign), and &=(eduallty). These extend the
definitions of the binary infix operators 9. '. :I, and I to pairs of FinSets. The Fin5et implementation
also takes advantage of the rewrite rule for MI and -:I.

Assertions are included in the speciHCationa of the FinSet operators. (We use ”prime“ notation in
post conditions: 5' Is the value that 5 had on entry to the procedure.) Some have also been included in
the main program to explain the operation of the program.

Three kinds of loops are used. Routines insert. Remove, and Has all use flLs_t loops to search for
elements, insert defaults the 91:2 part and Remove defaults the 1'32 part. Note that the equality test
in the suchthot clauses of these loops uses the equality defined for EitType. As a result, the code for
these routines may depend on the definition of the type passed as an lnstantiation parameter to
FinSet. The main program declares three sets -< one is a set of colors and the other two are sets of
sets (of colors). The program uses 12', loops with the generator coiorSgen on colors. It also uses a
conventional m.

The '$' name qualification is used for names colorScard and colorSgen. These are constants defined
for the ordered enumerated type color (number of elements and a standard generator, respectively).
They are associated with the type rather than with any variable of the type. The qualification is used
to distinguish ord and gen from the corresponding definitions associated with other enumerated types.


HTML translation in progress


An informal Definition oi Alphard

fgrm FinSetlEl(Tgpe:fgrm<&:-.G->.Haxsiza:intagnrl
9;; I HaxSize 2 Bl

Lg guess

M g; F5:flath:matical5:tlEl{Type}
invariant I cardinalitgtFS) s Haxsizal

initial); l FS-l l l

EEB§ Inserilzgg S:Fin5¢i.x:El(TgpI) re cardinality(lll U S.FS) s S.HaISiza )
S.F5-S.F5' U (xi l

gran: Removelfl S:FinSai.x:E|tTupal S.FS - S.F5' - lxl l

vgrgc Choose(S:Finset):EltTgpe



vgrcc sulm Fl,S:FinSet):Fin5It





we: S.FSl

regglt I x(S.FS l
:ardinalitqu.FS U S.FS) s R.nax5iza l

regglt I R.FS’ U S.FS' l
regulg I R.FS' n S.FS’ l
ragul - R.FS I S.FS' l
:1:ng I (Fl.FS' - S.FS‘) l



Empthet (E Hype: form,naxSizI: int-gar)
ggst I result - (I l



1g; V:vectar(EltTgps.1.HaxSizs), mainleger igi; n:-€
gcn;g HaxSize: g3 spegifleg;

regmag I PS I lV[i1 l lsismll

invariant [(BsmsnaxSize) A (Vi.j([l..u](VIiI-Vljlai-jll )




Lg First p m uptul1.5.m) sutha; S.le]-I
gigs S.» Ix- 1: 5.V[S.mlx-x Li


Lg first p from upto(1.5.m) suchghgg S.V[pl-x
thgn S.V(pJ:-5.V[Slm1; Sm ~x- 1 fl

vgrcg Choose 1; S.VI1]

fgng Has
Lg first 9 £525 upto(1.5.m) agchthag S.V[p]-x
£553 krue gig; false £1
fgn; 6+
i_5 value T:Finsath.Elngpa.R.flax5iza) a_{
T.m :- R.m
jg; j from gggg(l.R.m) g9 T.Vlj1 :- R.V[j] gg
Q; j m upto(1.S.m)1q_ lnnrtlT.S.Y[leg§
fgng 5*
L; vglue TzFinset(R.EltTgpa.R.flax5ize} g1
DI j m uptollfiml E i_f Hasl5.R.V(j])
then ln::rt(T,R.V[jJ) .li 22
vgrac 5:-

L3 valug R g; R.u :- S.u; jg; i frgm upto(1.5.n) gg R.V[i] :- S.V(i] 9g fig



HTML translation in progress

fung 5-
;; R.m-S.m aLd first i m uptollfiun) guchsrugt w Has(S.R.V[i])
(PW—en falss :2; true fl
fgn; EmplgSet
i4 Jul x a M *3

! Compute pnuerset of enumerated tupa
fgrm color 15 enumerated (red.orangs.gellcu.graen.b|ua.viale‘) gag
git; Covanei: FinSat(FinSat(-:alor.color£card), chuloricard)
asger-t { Color5:t - I l )
M!Color$et- l I}!)
it c m colon-89m d3
v_a_r; Temp: FinSet(Finsu(automaton-Scam), chulortcard)
Temp :- CalorSet
uni I; Tamp - EmptySaHFinSat(=0!or.cnlnr$caro)) gg
1g; Current: FinSet(culur.cnlor$caru)
Insert(Current.c): Insart(ColarSot.Eurren0
9—6- .
M ( Color-Set - (S I 5 ; (xlx in a valul a! my. Color-Sail ) )



HTML translation in progress

Appendix E
Proof Rules

Proof Rules Omitted From Preliminary Version