Changeset 4313

Timestamp:

11/04/09 22:09:51 (3 weeks ago)

Author:

sukyoungryu

Message:

[spec] Added the Preliminaries part.

Location:

trunk/Specification

Files:

• fortress/fortress.bib (modified) (5 diffs)
• preliminaries/intro/acknowledgments.tex (added)
• preliminaries/intro/intro.tex (modified) (1 diff)
• preliminaries/intro/nutshell.tex (added)
• preliminaries/intro/organization.tex (added)
• preliminaries/intro/philosophy.tex (added)
• preliminaries/overview (deleted)
• preliminaries/overview.tex (copied) (copied from trunk/Specification/preliminaries/overview/overview.tex) (1 diff)
• preliminaries/preliminaries.tex (modified) (1 diff)

trunk/Specification/fortress/fortress.bib

@@ -15 +15 @@
 %   trademarks of Sun Microsystems, Inc. in the U.S. and other countries.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+@book{Eiffel,
+  year = {1988},
+  title = {Object-oriented Software Construction},
+  publisher = {Prentice Hall},
+  author = {B. Meyer}
+}
 
 @inproceedings{fgj,
@@ -66 +73 @@
   address = "Cambridge, UK",
   year = "1998"
+}
+
+@book{Haskell,
+  year = {2003},
+  title = {Haskell 98 Language and Libraries},
+  publisher = {Cambridge University Press},
+  author = {Simon Peyton-Jones}
 }
 
@@ -98 +112 @@
 }
 
+@article{MillsteinChambers,
+  author={Todd Millstein and Craig Chambers},
+  title={Modular Statically Typed Multimethods},
+  journal={Information and Computation},
+  volume=175,
+  number=1,
+  pages={76-118},
+  month=may,
+  year=2002,
+}
+
 @techreport{morton,
   author = "G. M. Morton",
@@ -104 +129 @@
   month = mar,
   year = 1966
+}
+
+@inproceedings{NextGen,
+  title = {Compatible Genericity with Run-time Types for the {J}ava {P}rogramming {L}anguage},
+  booktitle = {OOPSLA},
+  year = {1998},
+  author = {R. Cartwright and G. Steele}
 }
 
@@ -115 +147 @@
 }
 
+@book{OCaml,
+  author ={Xavier Leroy and
+           Damien Doligez and
+           Jacques Garrigue and
+           Didier R\'{e}my and
+           J\'{e}r\^{o}me Vouillon},
+  title = {The Objective Caml System, release 3.08},
+  year = {2004},
+  publisher = "\url{http://caml.inria.fr/distrib/ocaml-3.08/ocaml-3.08-refman.pdf}"
+}
+
 @misc{Rats,
   author = "Robert Grimm",
   title = "Rats! -- An Easily Extensible Parser Generator",
   howpublished = "\url{http://cs.nyu.edu/~rgrimm/xtc/rats.html}" }
+
+@book{Scala,
+  year = {2004},
+  title = {The Scala Language Specification},
+  author = {Martin Odersky and
+           Philippe Altherr and
+           Vincent Cremet and
+           Burak Emir and
+           St\'{e}phane Micheloud and
+           Nikolay Mihaylov and
+           Michel Schinz and
+           Erik Stenman and
+           Matthias Zenger},
+  publisher = "\url{http://scala.epfl.ch/docu/files/ScalaReference.pdf}"
+}
+
+@article{Scheme,
+  author = "Richard Kelsey and William Clinger and Jonathan Rees",
+  title = "Revised$^{5}$ Report on the Algorithmic Language {Scheme}",
+  journal = "ACM SIGPLAN Notices",
+  volume = "33",
+  number = "9",
+  pages = "26--76",
+  year = "1998",
+  url = "citeseer.csail.mit.edu/article/kelsey98revised.html"
+}
+
+@book{Self,
+  year = {2000},
+  title = {The Self Programmer's Reference Manual},
+  author = {Ole Agesen and
+           Lars Bak and
+           Craig Chambers and
+           Bay-Wei Chang and
+           Urs H\"{o}lzle and
+           John Maloney and
+           Randall B. Smith and
+           David Ungar and
+           Mario Wolczko},
+  publisher = "\url{http://research.sun.com/self/release_4.0/Self-4.0/manuals/Self-4.1-Pgmers-Ref.pdf}"
+}
+
+@book{SML,
+  author ={Robin Milner and Mads Tofte and Robert Harper and David MacQueen},
+  title = {The Definition of Standard ML (Revised)},
+  year = {1997},
+  publisher = "The MIT Press"
+}
+
+@article{traits,
+  author = {St\'ephane Ducasse and Oscar Nierstrasz and Nathanael Sch{\"a}rli and Roel Wuyts and Andrew P. Black},
+  title = {Traits: A mechanism for fine-grained reuse},
+  journal = {ACM Trans. Program. Lang. Syst.},
+  volume = {28},
+  number = {2},
+  year = {2006},
+  issn = {0164-0925},
+  pages = {331--388},
+  doi = {http://doi.acm.org/10.1145/1119479.1119483},
+  publisher = {ACM Press},
+  address = {New York, NY, USA},
+}
 
 @book{Unicode,

trunk/Specification/preliminaries/intro/intro.tex

@@ -19 +19 @@
 \chaplabel{intro}
 
-% \input{\home/preliminaries/intro/philosophy}
-% \input{\home/preliminaries/intro/nutshell}
-% \input{\home/preliminaries/intro/acknowledgments}
-% \input{\home/preliminaries/intro/organization}
+\input{\home/preliminaries/intro/philosophy}
+\input{\home/preliminaries/intro/nutshell}
+\input{\home/preliminaries/intro/acknowledgments}
+\input{\home/preliminaries/intro/organization}

trunk/Specification/preliminaries/overview.tex

@@ -18 +18 @@
 \chapter{Overview}
 \chaplabel{overview}
+
+\note{Keyword and varargs parameters,
+array comprehensions,
+dimensions and units,
+tests and properties,
+distributions,
+some ASCII conversion, and
+some common types are not yet supported.
+
+From \secref{programming-env} to \secref{apitool} are out of date.
+
+Some examples in this chapter are not tested nor run by the interpreter.}
+
+\note{Eric: Note that APIs are difficult to remove from fortresses: we have
+to first remove every component referring to them. Also note
+that an autogenerated API source file isn't automatically compiled
+into the fortress. I think the error should be signaled when the
+programmer tries to compile the API.}
+
+In this chapter, we provide a high-level overview of the entire Fortress
+language. We present most features in this chapter through the use of examples,
+which should be accessible to programmers of other languages.
+In this chapter, unlike the rest of the specification,
+no attempt is made to provide complete descriptions
+of the various language features presented. Instead, we intend this overview to
+provide useful context for reading other sections of this specification,
+which provide rigorous definitions for what is merely
+introduced here.
+
+\section{The Fortress Programming Environment}
+\seclabel{programming-env}
+
+Although Fortress is independent of the properties of a particular
+platform on which it is implemented, it is helpful for concreteness
+to present the programming model used in the Fortress reference implementation.
+In this programming model,
+Fortress source code is stored in files and organized in
+directories, and there is a text-based shell from which we can store
+environment variables and issue commands to execute and compile
+programs.
+
+A Fortress program can be processed in one of two ways:
+
+\begin{itemize}
+
+\item It can be \emph{executed}. The Fortress program is stored in a file with
+the suffix ``\shellcommand{.fss}'' and executed directly from an underlying
+operating
+system shell by calling the command ``\shellcommand{fortress run}'' on it.
+For example,
+suppose we write the following \(\hbox{\rm``\STR{Hello,~world!}''}\) program
+to a file ``\shellcommand{HelloWorld.fss}'':
+\input{\home/preliminaries/examples/Overview.shell.a.tex}
+
+The first line is an \emph{export statement};
+we ignore it for the moment.
+The second line defines a function \VAR{run},
+which takes a parameter named \VAR{args}
+and prints the string \(\hbox{\rm``\STR{Hello,~world!}''}\).
+Note that the parameter \VAR{args}
+does not include a declaration of its type.
+In many cases,
+ types can be elided in Fortress and inferred from context.
+(In this case,
+the type of \VAR{args} is inferred based on the program's export statement,
+explained in \secref{overview:apis}.)
+
+We can execute this program by issuing the following command to the shell:
+
+\shellcommand{fortress run HelloWorld.fss}
+
+The instruction \shellcommand{fortress run} can be abbreviated as \shellcommand{fortress}:
+
+\shellcommand{fortress HelloWorld.fss}
+
+\item It can be \emph{compiled}. In this case, the Fortress program is
+compiled into a
+\emph{component}, which is stored in a hidden persistent cache maintained by the implementation,
+called a \emph{fortress}. Typically, a single fortress holds all the components
+of a user, or group of users sharing programs and libraries.
+In our examples,
+we often refer to the fortress we are storing components in
+as \emph{the resident fortress}.
+
+For example, we could have written our \(\hbox{\rm``\STR{Hello,~world!}''}\)
+program as follows:
+\input{\home/preliminaries/examples/HelloWorld.tex}
+
+We can compile this program, by issuing the command
+``\shellcommand{fortress compile}'' on it:
+
+\shellcommand{fortress compile HelloWorld.fss}
+
+As a result of this command, a component named ``\TYP{HelloWorld}'' is stored
+in the resident fortress. The name of this component is provided by
+the enclosing component declaration surrounding the code. If there is
+no enclosing component declaration, then the contents of the file are
+understood to belong to a single component whose name is that of the
+file it is stored in, minus its suffix. For example, suppose we write the
+following program in a source file named ``\shellcommand{HelloWorld2.fss}'':
+\input{\home/preliminaries/examples/HelloWorld2.tex}
+
+When we compile this file:
+
+\shellcommand{fortress compile HelloWorld2.fss}
+
+the result is that a new component with the name \TYP{HelloWorld2} is stored
+in the resident fortress.
+Once this component is compiled,
+we can execute it by issuing
+the following command:
+
+\shellcommand{fortress run HelloWorld2.fss}
+
+Compiling a source file allows us to catch static errors before running a program.
+It also allows the system to perform static optimizations on a program and use those
+optimizations when executing.
+
+Once a program is compiled, the cached code will be used during execution unless
+modifications have been made to the source file since the most recent compilation.
+If the source file is newer, the program is recompiled before execution.
+
+\end{itemize}
+
+A source file must contain exactly one component declaration, and its name must
+match the file name.
+
+In a compiled file,
+multiple component declarations may be included.
+For example, we could write the following file
+\shellcommand{HelloWorld3.fss}:
+
+%component HelloWorld
+%   export Executable
+%   run(args) = print "Hello, world!"
+%end
+%
+%component HelloWorld2
+%   export Executable
+%   run(args) = print "Hi, it's me again!"
+%end
+\begin{Fortress}
+\(\KWD{component} \TYP{HelloWorld}\)\\
+{\tt~~~}\pushtabs\=\+\(   \KWD{export} \TYP{Executable}\)\\
+\(   \VAR{run}(\VAR{args}) = \VAR{print}\;\hbox{\rm``\STR{Hello,~world!}''}\)\-\\\poptabs
+\(\KWD{end}\)\\[4pt]
+\(\KWD{component} \TYP{HelloWorld2}\)\\
+{\tt~~~}\pushtabs\=\+\(   \KWD{export} \TYP{Executable}\)\\
+\(   \VAR{run}(\VAR{args}) = \VAR{print}\;\hbox{\rm``\STR{Hi,~it's~me~again!}''}\)\-\\\poptabs
+\(\KWD{end}\)
+\end{Fortress}
+
+When we compile this file, the result is that both the components
+\TYP{HelloWorld} and \TYP{HelloWorld2} are stored in the resident fortress.
+
+If a fortress already contains a component with the same name as a
+newly installed component, the new component shadows the old one. For
+example, if we first compile the source file \shellcommand{HelloWorld3.fss}
+above and then compile the following file \shellcommand{HelloWorld4.fss}:
+
+%component HelloWorld
+%   export Executable
+%   run(args) = print "I didn't expect that!"
+%end
+\begin{Fortress}
+\(\KWD{component} \TYP{HelloWorld}\)\\
+{\tt~~~}\pushtabs\=\+\(   \KWD{export} \TYP{Executable}\)\\
+\(   \VAR{run}(\VAR{args}) = \VAR{print}\;\hbox{\rm``\STR{I~didn't~expect~that!}''}\)\-\\\poptabs
+\(\KWD{end}\)
+\end{Fortress}
+
+then executing the component \TYP{HelloWorld} on our fortress will result in
+printing of the following text:
+
+\begin{verbatim}
+I didn't expect that!
+\end{verbatim}
+
+We can also ``remove'' a component from a fortress.
+For example:
+
+\shellcommand{fortress remove HelloWorld}
+
+After issuing this command, we can no longer refer to \shellcommand{HelloWorld}
+component when issuing commands to the fortress.
+(However, a removed component might still exist as a constituent of other,
+\emph{linked}, components; see \secref{overview:apis}.)
+
+\label{overviewComponent}
+\section{Exports and Imports}
+\seclabel{overview:apis}
+
+When a component is defined, it can include \emph{export statements}.
+For example,
+all of the components we have defined thus far
+have included the export statement ``\EXP{\KWD{export} \TYP{Executable}}''.
+Export statements list various \emph{APIs}
+that a component implements.
+Unlike in other languages, APIs in
+Fortress are themselves program constructs; programmers can rely on
+standard APIs, and declare new ones. API declarations are sequences of
+declarations of
+variables, functions, and other program constructs, along with their
+types and other
+supporting declarations. For example, here is the definition of API
+\TYP{Executable}:
+\input{\home/preliminaries/examples/Executable.tex}
+
+This API contains the declaration of a single function \VAR{run},
+whose type is \EXP{(\TYP{String}\ldots) \rightarrow ()}. This type is an
+\emph{arrow type}; it declares the type of a function's parameter,
+and its return type. The function \VAR{run} includes a single
+parameter; the notion \EXP{(\TYP{String}\ldots)} indicates that it is a
+\emph{varargs} parameter; the function \VAR{run} can be called with an
+arbitrary number of string arguments. For example, here are
+valid calls to this function:
+
+%run("a simple", " example")
+%run("run(...)")
+%run("Nobody", "expects", "that")
+\begin{Fortress}
+\(\VAR{run}(\hbox{\rm``\STR{a~simple}''},\;\hbox{\rm``\STR{~example}''})\)\\
+\(\VAR{run}(\hbox{\rm``\STR{run(...)}''})\)\\
+\(\VAR{run}(\hbox{\rm``\STR{Nobody}''},\;\hbox{\rm``\STR{expects}''},\;\hbox{\rm``\STR{that}''})\)
+\end{Fortress}
+
+
+The return type of \VAR{run} is \EXP{()}, pronounced ``void''.
+Type \EXP{()} may be used in Fortress as a return type
+for functions that have no meaningful return value.
+There is a single value with type \EXP{()}:
+the value \EXP{()}, also pronounced ``void''.
+References to value \EXP{()} as opposed
+to type \EXP{()} are resolved by context.
+
+As with components, APIs can be defined in files and compiled. APIs
+must be defined in files with the suffix \shellcommand{.fsi}.
+An \shellcommand{.fsi} file contains
+source code for exactly one API, and its name must match the file name,
+minus the suffix.
+If there are  no explicit ``\KWD{api}''
+headers, the file is understood to define a single API whose name is
+the name of the containing file (minus its suffix).
+
+An API is compiled with the shell command ``\shellcommand{fortress compile}''.
+When an API is compiled,
+it is installed in the resident fortress.
+
+
+For example, if we store
+the following API in a file named ``\shellcommand{Zeepf.fsi}'':
+\input{\home/preliminaries/examples/Zeepf.tex}
+then we can compile this API with the following shell command:
+
+\shellcommand{fortress compile Zeepf.fsi}
+
+This command compiles the API \TYP{Zeepf}
+and installs it in the resident fortress.
+%If we omit the enclosing API declaration,
+%so that the file \shellcommand{Zeepf.fsi} consists solely of the following code:
+
+%foo: String -> ()
+%baz: String -> String
+%\begin{Fortress}
+%\(\VAR{foo}\COLON \TYP{String} \rightarrow ()\)\\
+%\(\VAR{baz}\COLON \TYP{String} \rightarrow \TYP{String}\)
+%\end{Fortress}
+
+%then the file is assumed to consist of the declaration of a single API
+%named \TYP{Zeepf}.
+
+Unlike component compilation, API compilation does not shadow
+existing elements of a fortress.
+If we attempt to compile an API with the same name as an API
+already defined
+in the resident fortress, an error is signaled
+and the fortress is left unchanged. To remove an API, we must
+first remove all components referring to the API,
+and then issue the shell command ``\shellcommand{fortress removeApi}''.
+
+
+A component that exports an API must provide a definition
+for every program construct declared in the API. For example, because
+our component \TYP{HelloWorld}:
+\input{\home/preliminaries/examples/HelloWorld.tex}
+exports the API \TYP{Executable}, it must include a definition for the
+function \VAR{run}.
+The definition of \VAR{run} in \TYP{HelloWorld} need not include
+declarations of the
+parameter type or return type of \VAR{run}, as these can be inferred
+from the
+definition of API \TYP{Executable}.
+
+Components are also allowed to \emph{import} APIs. A component that
+imports an API is allowed to use any of the program constructs
+declared in that API. For example, the following component imports the API
+\TYP{Zeepf} and calls the function \VAR{foo} declared in \TYP{Zeepf}:
+\input{\home/preliminaries/examples/Blargh.tex}
+
+The component \TYP{Blargh} imports declaration \VAR{foo} from the API \TYP{Zeepf}
+and exports the API
+\TYP{Executable}. Its \VAR{run} function is defined by calling function
+\VAR{foo}, defined in \TYP{Zeepf}.
+In an import statement of the form:
+%import A.{S}
+\begin{Fortress}
+\(\KWD{import}\:A.\{S\}\)
+\end{Fortress}
+all names in the list of names \VAR{S} are imported from API $A$, and can be
+referred to as unqualified names within the importing component. In
+the example above, the names we have imported consist of a
+single name: \VAR{foo}. If we had instead written:
+\input{\home/preliminaries/examples/Blargh2.tex}
+then we would have been able to refer to both \VAR{foo} and \VAR{baz}
+as unqualified names in \TYP{Blargh}.
+
+Note that no component refers directly to another component,
+or to constructs defined in another component.
+Instead, \emph{all external references go through APIs}.
+This level of indirection provides us with significant power.
+It provides a way to hide implementation details in a component.
+Also, our intention is that in future implementations,
+it will be possible to make use of APIs to provide sophisticated
+link and upgrade operations for the purposes of building
+large programs.
+%Programmers will be able to link together components from separate
+%programming teams, swap in revised components into deployed
+%applications, and even test components that rely on expensive libraries
+%by wiring them up to special
+%\emph{mock components} that provide just enough functionality to allow
+%for testing.
+
+Components that contain no import statements and export the API
+\TYP{Executable} are referred to as \emph{executable components}. They
+can be compiled and executed directly as stand-alone components. All
+of our \TYP{HelloWorld} components are executable components.
+However,
+if a component imports one or more APIs, it cannot be executed as a
+stand-alone program. Instead, its imports are resolved to
+other components that export all of the APIs it imports,
+to form a new \emph{compound} component. For example, we define
+the following component in a file named \shellcommand{Ralph.fss}:
+\note{The example is commented out because it is not supported yet nor run by the interpreter.}
+%\input{\home/library/examples/Ralph.compile.tex}
+
+We can now issue the following shell commands:
+
+\shellcommand{fortress compile Ralph.fss} \\
+\shellcommand{fortress compile Blargh.fss} \\
+\shellcommand{fortress run Blargh.fss} \\
+
+The first two commands compile files \shellcommand{Ralph.fss} and
+\shellcommand{Blargh.fss},
+respectively, and install them in the resident fortress. The third
+command tells the resident fortress to run component \TYP{Blargh}.
+References to API \TYP{Zeepf} in \TYP{Blargh} are resolved to their
+implementation in component \TYP{Ralph}.
+
+All references to API \TYP{Zeepf} in \TYP{Gary} are resolved
+to the declarations provided in \TYP{Ralph}.
+
+Note that forming the compound component \TYP{Gary} has no effect on the
+components \TYP{Ralph} and \TYP{Blargh}.
+These components remain in the resident
+fortress, and they can be linked together with other components to
+form yet more compound components.
+Conversely, if \TYP{Blargh} or \TYP{Ralph} is
+recompiled, deleted, or otherwise updated,
+there is no effect on \TYP{Gary}.
+Conceptually, \TYP{Gary} contains its own copies
+of the components \TYP{Blargh} and \TYP{Ralph},
+and these copies are not corrupted by actions on other components.
+For this reason, we say that components in Fortress
+are \emph{encapsulated}. (Of course, there are optimization tricks
+that a fortress can use to maintain the illusion of encapsulation
+without actually copying. But these tricks are beyond the scope of
+this specification.)
+
+Compound components are \emph{upgradable}: They can be upgraded with
+new components that export some of the APIs used by their
+constituents. For example, if a new version of \TYP{Ralph} is compiled and
+installed in the resident fortress,
+we can manually \emph{upgrade} \TYP{Gary} with
+the new version by performing the following shell command:
+
+\shellcommand{fortress upgrade NewGary from Gary with Ralph}
+
+This command produces a new component, named \shellcommand{NewGary},
+resulting from an upgrade of \shellcommand{Gary} with \shellcommand{Ralph}.
+The components referred to as \shellcommand{Gary} and \shellcommand{Ralph}
+are unaffected. An important property of fortress components is that
+they are \emph{stateless}; once constructed, they are never modified.
+Even if a component is ``removed'' from a fortress, the components
+it is a constituent of are unaffected.
+
+However, we can rebind \emph{the name} \shellcommand{Gary}
+in the resident fortress to our new component with the following command:
+
+\shellcommand{fortress upgrade Gary from Gary with Ralph}
+
+or simply:
+
+\shellcommand{fortress upgrade Gary with Ralph}
+
+Now, the original component referred to by \shellcommand{Gary} is
+shadowed; it cannot be referred to directly from the shell.
+However, it might still exist in the fortress as a constituent of
+other components, which are unmodified by the upgrade.
+To upgrade all components in a fortress at once
+with a new version of \shellcommand{Ralph} (rebinding all
+names to the resulting upgrades), we can issue the command:
+
+\shellcommand{fortress upgradeAll Ralph}
+
+\section{Automatic Generation of APIs}
+\seclabel{apitool}
+
+Note that the component named \TYP{Zeepf} exports the API
+\TYP{Zeepf}. Components and APIs exist in separate namespaces, and therefore
+it is allowed for a component to have the same name as an API.
+In fact, if we hadn't already defined and compiled API \TYP{Zeepf},
+we could generate it automatically
+from the definition of component \TYP{Zeepf}
+with the following shell command:
+
+\shellcommand{fortress api Zeepf.fss}
+
+This command generates a new source file, \shellcommand{Zeepf.fsi}, in the
+same directory as \shellcommand{Zeepf.fss}, which includes declarations for
+all program constructs defined in \shellcommand{Zeepf.fss}.
+
+In general, if a component $C$ exports an API $A$ with the same name as $C$,
+it is possible to automatically generate a source file
+for the API $A$ from $C$
+by issuing the shell command \shellcommand{fortress api} on the file
+containing the definition of $C$.
+This API contains declarations for all definitions in $C$ that are not
+declared in other APIs exported by $C$, and that do not include
+the modifier \KWD{private}.
+If a source file with the name of $A$ already exists in the
+same directory as the source file of $C$, an error is signaled,
+and no file is created.
+
+If there is more than one component defined in a file,
+APIs are generated for all components defined in the file that
+export APIs with the same name as the respective component.
+Each generated API is placed in a separate source file whose
+name corresponds to the name of the API it defines.
+
+Note that the API corresponding to an automatically generated source
+file is not automatically added to the resident fortress; the source
+file must still be compiled via a separate action. Often, programmers
+may want to edit the autogenerated file before compiling it to the
+fortress.
+
+It is not always desirable for a component to export an API of the same name.
+Many components will export only publicly defined standard APIs.
+However, automatic generation of APIs from components may be useful,
+particularly for components defined internally by a development team.
+Large projects may contain many internally defined components that
+are never released externally,
+except as constituents of compound components.
+
+\section{Rendering}
+
+One aspect of Fortress that is quite different from many other languages
+is that various program constructs are rendered in particular fonts,
+so as to emulate mathematical notation.
+For example, variable names are rendered in italic fonts.
+Many other program constructs have their own rendering rules. For
+example, the operator \verb$^$ indicates superscripting in
+Fortress.
+A function definition consisting of the following ASCII characters:
+
+\begin{verbatim}
+f(x) = x^2 + sin x - cos 2 x
+\end{verbatim}
+
+is rendered as follows:
+
+\input{\home/preliminaries/examples/Overview.Rendering.a.tex}
+
+Array indexing, written with brackets:
+
+\begin{verbatim}
+a[i]
+\end{verbatim}
+
+is rendered as follows:
+
+\input{\home/preliminaries/examples/Overview.Rendering.b.tex}
+
+There are many other examples of special rendering conventions.
+
+Fortress also supports the use of Unicode characters~\cite{Unicode} in
+identifiers. In order to make it easy to enter such characters with
+today's input devices, Fortress defines a convention for keyboard
+entry: ASCII names (and abbreviations) of Unicode characters can be
+written in a program in all caps (with spaces replaced by underscores).
+Such identifiers are converted to Unicode characters. For example,
+the identifier:
+
+\begin{verbatim}
+GREEK_CAPITAL_LETTER_LAMBDA
+\end{verbatim}
+
+is automatically converted into the identifier:
+
+$\Lambda$
+
+There are also ASCII abbreviations for writing down commonly used
+Fortress characters. For example, ASCII identifiers for all Greek
+letters are converted to Greek characters
+(e.g., ``\txt{lambda}'' becomes $\lambda$
+and ``\txt{LAMBDA}'' becomes $\Lambda$).
+Here are some other common ASCII shorthands:
+
+\begin{tabular}{rclrcl}
+         \txt{BY}  & \emph{becomes} & $\times$ &
+         \txt{TIMES}  & \emph{becomes} & $\times$ \\
+         \txt{DOT}  & \emph{becomes} & $\csdot$ &
+         \txt{CROSS} & \emph{becomes} & $\times$ \\
+         \txt{CUP} & \emph{becomes} & $\cup$ &
+         \txt{CAP} & \emph{becomes} & $\cap$ \\
+         \txt{BOTTOM} & \emph{becomes} & $\bot$ &
+         \txt{TOP} & \emph{becomes} & $\top$ \\
+         \txt{SUM} & \emph{becomes} & $\sum$ &
+         \txt{PROD} & \emph{becomes} & $\prod$ \\
+         \txt{INTEGRAL} & \emph{becomes} & $\int$ &
+         \txt{EMPTYSET} & \emph{becomes} & $\emptyset$ \\
+         \txt{SUBSET} & \emph{becomes} & $\subset$ &
+         \txt{NOTSUBSET} & \emph{becomes} & $\not\subset$ \\
+         \txt{SUBSETEQ} & \emph{becomes} & $\subseteq$ &
+         \txt{NOTSUBSETEQ} & \emph{becomes} & $\not\subseteq$ \\
+         \txt{EQUIV} & \emph{becomes} & $\equiv$ &
+         \txt{NOTEQUIV} & \emph{becomes} & $\not\equiv$ \\
+         \txt{IN} & \emph{becomes} & $\in$ &
+         \txt{NOTIN} & \emph{becomes} & $\not\in$ \\
+         \txt{LT} & \emph{becomes} & $<$ &
+         \txt{LE} & \emph{becomes} & $\leq$ \\
+         \txt{GT} & \emph{becomes} & $>$ &
+         \txt{GE} & \emph{becomes} & $\geq$ \\
+         \txt{EQ} & \emph{becomes} & $=$ &
+         \txt{NE} & \emph{becomes} & $\neq$ \\
+         \txt{AND} & \emph{becomes} & $\wedge$ &
+         \txt{OR} & \emph{becomes} & $\vee$ \\
+         \txt{NOT} & \emph{becomes} & $\neg$ &
+         \txt{XOR} & \emph{becomes} & $\oplus$ \\
+         \txt{INF} & \emph{becomes} & $\infty$ &
+         \txt{SQRT} & \emph{becomes} & $\surd$ \\
+\end{tabular}
+
+A comprehensive description of ASCII conversion is provided in
+\appref{ascii-unicode}.
+
+\section{Some Common Types in Fortress}
+
+Fortress provides a wide variety of standard types, including
+\TYP{String}, \TYP{Boolean}, and various numeric types.
+The floating-point type \EXP{\mathbb{R}64} (written in ASCII as \verb$RR64$)
+is the type of 64-bit precision floating-point numbers.
+For example, the following function takes a 64-bit
+ float and returns a 64-bit float:
+\input{\home/preliminaries/examples/Overview.Types.tex}
+
+Predictably, 32-bit precision floats are written \EXP{\mathbb{R}32}.
+
+64-bit integers are denoted by the type \EXP{\mathbb{Z}64} and
+32-bit integers by the type \EXP{\mathbb{Z}32}
+and infinite precision integers by the type \EXP{\mathbb{Z}}.
+
+\section{Functions in Fortress}
+Fortress allows recursive, and mutually recursive function definitions.
+Here is a simple definition of a \VAR{factorial} function in Fortress:
+
+\input{\home/preliminaries/examples/Overview.Function.factorial.tex}
+
+\subsection{Juxtaposition and function application}
+
+In the definition of \VAR{factorial},
+note the juxtaposition of parameter \VAR{n} with the recursive
+call \EXP{\VAR{factorial}(n - 1)}.
+In Fortress, as in mathematics,
+multiplication is represented through juxtaposition.
+By default,
+two expressions of numeric type that are juxtaposed
+represent a multiplication.
+On the other hand,
+juxtaposition of an expression of function type
+with another expression to its right
+represents function application,
+as in the following example:
+
+\input{\home/preliminaries/examples/Overview.Juxt.sin.tex}
+
+Moreover, juxtaposition of expressions of string type
+represents concatenation, as in the following example:
+
+\input{\home/preliminaries/examples/Overview.Juxt.String.tex}
+
+In fact, juxtaposition is an operator in Fortress,
+just like \EXP{+} and \EXP{-},
+that is overloaded based on the runtime types of its arguments.
+
+There is a special case concerning juxtaposition that is important to mention:
+When writing a numeric literal, the \emph{digit-group separator},
+\txt{NARROW NO-BREAK SPACE} (U+202F),
+may be included between the digits in order to improve readability.
+In ASCII,
+this character can be abbreviated in the context of a numeric literal
+(\emph{and only in this context}) with the character \txt{'}.
+For example, the number 299,792,458 can be denoted in ASCII by the
+following numeric literal:
+
+\begin{verbatim}
+299'792'458
+\end{verbatim}
+
+This literal is converted into Unicode by replacing all occurrences of
+\txt{'} with \txt{NARROW NO-BREAK SPACE}:
+%299 792 458
+\begin{Fortress}
+\(299{}\;792{}\;458\)
+\end{Fortress}
+This is not an application of the juxtaposition operator;
+rather, it is a single token.
+Note that commas cannot be used to separate digits because ambiguities
+would arise with the use of commas in other expressions,
+such as tuples.
+
+\subsection{Keyword Parameters}
+
+Functions in Fortress can be defined to take keyword arguments by
+providing default values for parameters. In
+the following example:
+
+%makeColor(red:ZZ64 = 0, green:ZZ64 = 0, blue:ZZ64 = 0) =
+%   if 0 <= red <= 255 AND 0 <= green <= 255 AND 0 <= blue <= 255
+%   then Color(red,green,blue)
+%   else throw Error end
+\begin{Fortress}
+\(\VAR{makeColor}(\VAR{red}\COLONOP\mathbb{Z}64 = 0, \VAR{green}\COLONOP\mathbb{Z}64 = 0, \VAR{blue}\COLONOP\mathbb{Z}64 = 0) =\)\\
+{\tt~~~}\pushtabs\=\+\(   \KWD{if} 0 \leq \VAR{red} \leq 255 \wedge 0 \leq \VAR{green} \leq 255 \wedge 0 \leq \VAR{blue} \leq 255 \)\\
+\(   \KWD{then} \TYP{Color}(\VAR{red},\VAR{green},\VAR{blue})\)\\
+\(   \KWD{else}\;\;\KWD{throw} \TYP{Error} \KWD{end}\)\-\\\poptabs
+\end{Fortress}
+
+the function \VAR{makeColor} takes three keyword arguments, all of
+which default to \EXP{0}. If we call it as follows:
+
+%makeColor(green = 255)
+\begin{Fortress}
+\(\VAR{makeColor}(\VAR{green} = 255)\)
+\end{Fortress}
+
+the arguments \VAR{red} and \VAR{blue} are both given the value \EXP{0}.
+
+There are some other aspects of this example worth mentioning.
+For example,
+the body of this function consists of an \KWD{if} expression.
+The test of the \KWD{if} expression checks that
+all three parameters have values between \EXP{0} and \EXP{255}. The
+boolean operator \EXP{\leq} is \emph{chained}: An expression of
+the form \EXP{x \leq y \leq z} is equivalent to the expression
+\EXP{x \leq y \wedge y \leq z}, just as in mathematical notation.
+The \KWD{then} clause provides an example of a constructor call in Fortress,
+and the \KWD{else} clause shows us an example
+of a \KWD{throw} expression in Fortress.
+\note{How can we tell this from the example?
+Indeed, in general, we can't distinguish constructors from other functions
+looking only at the call sites.}
+
+\subsection{Varargs Parameters}
+It is also possible to define functions that take a variable number of
+arguments.
+For example:
+\input{\home/preliminaries/examples/Overview.Function.printFirst.tex}
+
+This function takes an arbitrary number of integers and prints the first
+one (unless it is given zero arguments; then it throws an exception).
+
+\subsection{Function Overloading}
+\seclabel{overview-function-overloading}
+Functions can be overloaded in Fortress
+by the types of their parameters. Calls to overloaded functions are
+resolved based on the runtime types of the arguments. For example,
+the following function is overloaded based on parameter type:
+
+\input{\home/preliminaries/examples/Overview.Function.size.tex}
+
+
+If we call \VAR{size} on an object with runtime type \TYP{Cons}, the
+second definition of \VAR{size} will be invoked \emph{regardless of the static type of the argument}.
+Of course, function applications are
+statically checked to ensure that \emph{some} definition will be
+applicable at run time, and that the definition to apply will
+be unambiguous.
+
+
+\subsection{Function Contracts}
+
+Fortress allows \emph{contracts} to be included in function declarations.
+Among other things,
+contracts allow us to \emph{require}
+that the argument to a function satisfies a given set of constraints,
+and to \emph{ensure} that the resulting value satisfies some constraints.
+They provide essential documentation for the clients of a function,
+enabling us to express semantic properties
+that cannot be expressed through the static type system.
+
+Contracts are placed at the end of a function header, before the function body.
+For example, we can place a contract on our \VAR{factorial} function requiring
+that its argument be nonnegative as follows:
+\input{\home/preliminaries/examples/Overview.Function.contract.a.tex}
+
+We can also ensure that the result of \VAR{factorial} is itself nonnegative:
+\input{\home/preliminaries/examples/Overview.Function.contract.b.tex}
+
+The variable \KWD{outcome} is bound in the \KWD{ensures} clause
+to the return value of the function.
+
+\section{Some Common Expressions in Fortress}
+We have already seen an \KWD{if} expression in Fortress. Here's an
+example of a \KWD{while} expression:
+
+\input{\home/preliminaries/examples/Overview.Expression.whileE.tex}
+
+A sequence of expressions in Fortress may be delimited by \KWD{do} and
+\KWD{end}. Here is an example of a function that prints three words:
+
+\input{\home/preliminaries/examples/Overview.Expression.printThreeWords.tex}
+
+A \emph{tuple} expression contains a sequence of elements delimited by
+parentheses and separated by commas:
+
+\input{\home/preliminaries/examples/Overview.Expression.tuple.tex}
+
+When a tuple expression is evaluated, the various subexpressions are
+evaluated \emph{in parallel}. For example, the following tuple
+expression
+denotes a parallel computation:
+
+\input{\home/preliminaries/examples/Overview.Expression.tuple.factorial.tex}
+
+The elements in this expression may be evaluated in parallel.
+This same computation can be expressed as follows:
+
+\input{\home/preliminaries/examples/Overview.Expression.alsodo.tex}
+
+\section{For Loops Are Parallel by Default}
+Here is an example of a simple \KWD{for} loop in Fortress:
+\input{\home/preliminaries/examples/Overview.Expression.forLoop.tex}
+This \KWD{for} loop iterates
+over all elements \VAR{i} between \EXP{1} and \EXP{10}
+and prints the value of \VAR{i}.
+Expressions such as \EXP{1\COLONOP{}10}
+are referred to as \emph{range expressions}.
+They can be used in any context where
+we wish to denote all the integers between a given pair of integers.
+
+A significant difference between Fortress
+and most other programming languages
+is that \emph{for loops are parallel by default}.
+Thus, printing in the various iterations
+of this loop can occur in an arbitrary order, such as:
+
+5 4 6 3 7 2 9 10 1 8
+
+\section{Atomic Expressions}
+
+In order to control interactions of parallel executions, Fortress
+includes the notion of \emph{atomic expressions}, as in the following
+example:
+
+\input{\home/preliminaries/examples/Overview.Expression.atomicE.tex}
+
+An atomic expression
+is executed in such a manner that all other threads observe either that
+the computation has completed, or that it has not yet begun; no other
+thread observes an atomic expression to have only partially completed.
+Consider the following parallel computation:
+\input{\home/preliminaries/examples/Overview.Expression.Also.b.tex}
+
+Both parallel blocks are atomic; thus the second parallel block either
+observes that both \VAR{x} and \VAR{y} have been updated, or that
+neither has. Thus, possible values of the outermost \KWD{do}
+expression are 0 and 2, but not 1.
+
+\section{Dimensions and Units}
+
+Numeric types in Fortress can be annotated with physical units and
+dimensions. For example, the following function declares that its
+parameter is a tuple represented in the units \EXP{\mathrm{kg}} and
+\EXP{\mathrm{m}/\mathrm{s}},
+respectively:
+
+\note{I MANUALLY EDITED THIS CODE -Victor}
+%kineticEnergy(m:RR64 kg_, v:RR64 m_/s_):RR64 kg_ m_^2/s_^2 = (m v^2) / 2
+\begin{Fortress}
+\(\VAR{kineticEnergy}(m\COLONOP\mathbb{R}64\mskip 4mu plus 4mu\mathrm{kg}, v\COLONOP\mathbb{R}64\mskip 4mu plus 4mu\mathrm{m}/\mathrm{s})\COLONOP\mathbb{R}64\mskip 4mu plus 4mu\mathrm{kg}\mskip 4mu plus 4mu\mathrm{m}^{2}/\mathrm{s}^{2} = (m\ v^{2}) / 2\)
+\end{Fortress}
+
+A value of type \EXP{\mathbb{R}64\mskip 4mu plus 4mu\mathrm{kg}} is a
+64-bit float representing a measurement in kilograms.
+When the function \VAR{kineticEnergy} is called, two values in its tuple
+argument are statically checked to ensure that they are in the right units.
+
+All commonly used dimensions and units are provided in \library.
+Unit symbols are encoded with trailing underscores;
+such identifiers are rendered in roman font.
+For example the unit \EXP{\mathrm{m}} is represented as \verb$m_$.
+For each unit, both longhand and shorthand names are provided
+(e.g., \EXP{\mathrm{m}},
+\EXP{\mathrm{meter}}, and \EXP{\mathrm{meters}}).
+The various names of a given unit can be used interchangeably.
+Also, some units (and dimensions) are defined to be synonymous
+with algebraic combinations of other units (and dimensions).
+For example, the unit \EXP{\mathrm{N}} is defined to be synonymous
+with the unit \EXP{\mathrm{kg}\mskip 4mu plus 4mu\mathrm{m}/\mathrm{s}^{2}}
+and the dimension \EXP{\mathrm{Force}} is defined to be synonymous with
+\EXP{\mathrm{Mass}\mskip 4mu plus 4mu\mathrm{Acceleration}}.
+Likewise, the dimension \EXP{\mathrm{Acceleration}}
+is defined to be synonymous with \EXP{\mathrm{Velocity}/\mathrm{Time}}.
+
+Measurements in the same unit can be compared, added, subtracted,
+multiplied and divided.
+Measurements in different units can be multiplied and divided.
+For example, we can write the following variable declaration:
+
+%v : RR m_/s_ = (3 meters_ + 4 meters_) / 5 seconds_
+\begin{Fortress}
+\(v \mathrel{\mathtt{:}} \mathbb{R}\mskip 4mu plus 4mu\mathrm{m}/\mathrm{s} = (3\,\mathrm{meters} + 4\,\mathrm{meters}) / 5\,\mathrm{seconds}\)
+\end{Fortress}
+
+However, the following variable declaration is a static error:
+
+%v : RR m_/s_ = (3 meters_ + 4 seconds_) / 5 seconds_
+%I CREATED THE CODE BELOW MANUALLY -Victor
+\begin{Fortress}
+\(v \mathrel{\mathtt{:}} \mathbb{R}\mskip 4mu plus 4mu\mathrm{m}/\mathrm{s} = (3\,\mathrm{meters} + 4\,\mathrm{seconds}) / 5\,\mathrm{seconds}\)
+\end{Fortress}
+
+In addition, the following variable declaration is a static error
+because the unit of the left hand side of this declaration
+is \EXP{\mathrm{m}/\mathrm{s}}
+whereas the unit of the right hand side
+is simply \EXP{\mathrm{m}} (or \EXP{\mathrm{meters}}):
+
+%v : RR m_/s_ = (3 meters_ + 4 meters_) / 5
+\begin{Fortress}
+\(v \mathrel{\mathtt{:}} \mathbb{R}\mskip 4mu plus 4mu\mathrm{m}/\mathrm{s} = (3\,\mathrm{meters} + 4\,\mathrm{meters}) / 5\)
+\end{Fortress}
+
+It is also possible to convert a measurement in one unit to
+a measurement of another unit of the same dimension,
+as in the following example:
+
+%kineticEnergy(3.14 kg_, 32 f_/s_ in m_/s_)
+\begin{Fortress}
+\(\VAR{kineticEnergy}(3.14\,\mathrm{kg}, 32\,\mathrm{f}/\mathrm{s} \KWD{in} \mathrm{m}/\mathrm{s})\)
+\end{Fortress}
+
+The second argument to \EXP{\VAR{kineticEnergy} } is a measurement in
+feet per second,
+converted to meters per second.
+
+\section{Aggregate Expressions}
+\seclabel{overview-aggregate}
+As with mathematical notation, Fortress includes special syntactic support for
+writing down many common kinds of collections, such as arrays, matrices, vectors, maps, sets, and lists
+simply by enumerating all of the collection's elements.
+We refer to an expression formed by enumerating the elements of a
+collection as an \emph{aggregate expression}.
+The elements of an aggregate expression are computed in parallel.
+
+For example, we can define an array \VAR{a} in Fortress by explicitly writing down its elements, enclosed in brackets
+and separated by whitespace, as follows:
+
+\label{arrayAInf}
+\input{\home/preliminaries/examples/Overview.Expression.aggregate.a.tex}
+
+Two-dimensional arrays can be written down by separating rows by newlines (or by semicolons). For example, we can
+bind \VAR{b} to a two-dimensional array as follows:
+
+\label{arrayBInf}
+\input{\home/preliminaries/examples/Overview.Expression.aggregate.b.tex}
+
+There is also support for writing down arrays of dimension three and higher. We bind \VAR{c} to a three-dimensional
+array as follows:
+
+\label{arrayCInf}
+\input{\home/preliminaries/examples/Overview.Expression.aggregate.c.tex}
+
+Various slices of the array along the third dimension are separated by pairs of semicolons.
+(Higher dimensional arrays
+are also supported. When writing a four-dimensional
+array, slices along the fourth dimension are separating by triples of semicolons, and so on.)
+
+Vectors are written down just like one-dimensional arrays.
+Similarly, matrices are written down just like two-dimensional arrays.
+Whether an array aggregate expression evaluates to an array, a vector, or a
+matrix is inferred from context
+(e.g., the static type of a variable that such an expression is bound to).
+Of course, all elements of vectors and matrices must be numbers.
+
+Note that there is a syntactic conflict between the use of juxtaposition to
+represent elements along a row in an array and the use of juxtaposition to represent
+applications of the juxtaposition operator, and the use of spaces to seperate digits in a numeric literal.
+In order to include an application of the juxtaposition operator or a numeric literal with spaces
+as an outermost subexpression of an array aggregate, it is necessary to include extra parentheses. For example,
+the following aggregate expression represents a counterclockwise rotation matrix by an angle $\theta{}$ in $\mathbb{R}64^2$:
+
+\input{\home/preliminaries/examples/Overview.Expression.aggregate.d.tex}
+
+
+A set can be written down by enclosing its elements in braces and separating its elements by commas.
+Here we bind \VAR{s} to the set of integers \EXP{0} through \EXP{4}:
+
+\input{\home/preliminaries/examples/Overview.Expression.aggregate.s.tex}
+
+The elements of a list are enclosed in angle brackets (written in ASCII as
+\verb$<|$ and \verb$|>$):
+\input{\home/preliminaries/examples/Overview.Expression.aggregate.l.tex}
+
+The elements of a map are enclosed in curly braces, with key/value pairs
+joined by the arrow \EXP{\mapsto} (written in ASCII as \verb$|->$):
+\input{\home/basic/examples/Expr.Map.tex}
+
+\section{Comprehensions}
+Another way in which Fortress mimics mathematical notation is in its support for
+\emph{comprehensions}.  Comprehensions describe the elements of a collection by
+providing a rule that holds for all of the collection's elements.  The elements
+of the collection are computed in parallel by default.
+For example, we define a set \VAR{s} that consists of all elements of another
+set \VAR{t} divided by 2, as follows:
+\input{\home/preliminaries/examples/Overview.Expression.comprehension.s.tex}
+
+The expression to the left of the vertical bar
+explains that elements of \VAR{s} consist of every value \EXP{x/2}
+for every valid value of \VAR{x} (determined by the right hand side).
+The expression to the right of the vertical bar
+explains how the elements \VAR{x} are to be \emph{generated}
+(in this case, from the set \VAR{t}).
+The right hand side of a comprehension can consist of multiple generators.
+For example, the following set consists of every element
+resulting from the sum of an element of \VAR{s} with an element of \VAR{t}:
+\input{\home/preliminaries/examples/Overview.Expression.comprehension.sum.tex}
+
+The right hand side of a comprehension can also contain
+\emph{filtering expressions} to constrain the elements provided by other clauses.
+For example, we can stipulate that \VAR{v} consists of
+all nonnegative elements of \VAR{t} as follows:
+\input{\home/preliminaries/examples/Overview.Expression.comprehension.filter.tex}
+
+There is a comprehension expression for every form of aggregate expression.
+For example, here is a list comprehension in Fortress:
+\input{\home/preliminaries/examples/Overview.Expression.comprehension.l.tex}
+The elements of this list consist of
+all elements of the set \VAR{v} multiplied by \EXP{2}.
+
+In the case of an array comprehension, the expression to the left of the bar
+includes a tuple indexing the elements of the array.
+For example, the following comprehension describes a \EXP{3 \times 3}
+array, all of whose elements are zero.
+%[(x,y) = 0 | x <- {0,1,2}, y <- {0,1,2}]
+\begin{Fortress}
+\([(x,y) = 0 \mid x \leftarrow \{0,1,2\}, y \leftarrow \{0,1,2\}]\)
+\end{Fortress}
+
+The collection of elements \EXP{0} through \EXP{2} can also be expressed via a range expression, as follows:
+%[(x,y) = 0 | x <- 0:2, y <- 0:2]
+\begin{Fortress}
+\([(x,y) = 0 \mid x \leftarrow 0\COLONOP{}2, y \leftarrow 0\COLONOP{}2]\)
+\end{Fortress}
+
+An array comprehension can consist of multiple clauses. The clauses are run in the order provided,
+with declarations from later clauses shadowing declarations from earlier clauses. For example, the following
+comprehension describes a \EXP{3 \times 3} identity matrix:
+
+%[(x,y) = 0 | x <- 0:2, y <- 0:2
+% (x,x) = 1 | x <- 0:2]
+\begin{Fortress}
+\(\ [ \)\pushtabs\=\+\((x,y) = 0 \mid x \leftarrow 0\COLONOP{}2, y \leftarrow 0\COLONOP{}2\)\\
+\( (x,x) = 1 \mid x \leftarrow 0\COLONOP{}2]\)\-\\\poptabs
+\end{Fortress}
+
+
+
+\section{Summations and Products}
+As with mathematical notation, Fortress provides syntactic support for
+summations and productions (and other big operations) over the elements of a collection.
+For example, an alternative definition of \VAR{factorial} is as follows:
+
+\input{\home/preliminaries/examples/Overview.Expression.big.tex}
+
+This function definition can be written in ASCII as follows:
+
+\begin{verbatim}
+factorial(n) = PROD[i <- 1:n] i
+\end{verbatim}
+
+The character \EXP{\prod} is written \txt{PROD}.  Likewise,
+\EXP{\sum} is written \txt{SUM}.
+As with comprehensions, the values in the iteration are generated from specified collections.
+
+\label{overviewTest}
+\section{Tests and Properties}
+Fortress includes support for automated program testing.
+A new test in a component can be defined using the \KWD{test} modifier
+on a top-level function definition with type ``\EXP{()\rightarrow()}''.
+For example, here is a test function that calls to the \VAR{factorial}
+function on some representative values
+result in values greater than or equal to what was provided:
+\input{\home/preliminaries/examples/Overview.Tests.tex}
+
+%test factorialResultLarger [x <- 0:100] = x <= factorial(x)
+\begin{Fortress}
+\(\KWD{test} \VAR{factorialResultLarger} [x \leftarrow 0\COLONOP{}100] = x \leq \VAR{factorial}(x)\)
+\end{Fortress}
+
+The values for \VAR{x} are generated from the provided range
+\EXP{0\COLONOP{}100}.
+
+Programs are also allowed to include \emph{property} declarations, documenting boolean conditions that a program is
+expected to obey. Property declarations are similar syntactically to test declarations. Unlike test declarations,
+property declarations do not specify explicit finite collections over which the property is expected to hold.
+Instead, the parameters in a property declaration are declared to have types, and the property is expected to hold
+over all values of those types. For example, here is a property declaring that \VAR{factorial} is greater than or equal
+to every argument of type \EXP{\mathbb{Z}}:
+
+%property factorialResultAlwaysLarger = FORALL (x : ZZ) (x <= factorial(x))
+\begin{Fortress}
+\(\KWD{property} \VAR{factorialResultAlwaysLarger} = \forall (x \mathrel{\mathtt{:}} \mathbb{Z})\; (x \leq \VAR{factorial}(x))\)
+\end{Fortress}
+
+When a property declaration includes a name, the property identifier is bound to a function whose parameter and body are that of the property,
+and whose return type is \TYP{Boolean}.
+A function bound in this manner is referred to as a \emph{property function}.
+A property function can be called from within tests to ensure that a
+property holds at least for all values in some finite set of values.
+
+\section{Objects and Traits}
+\seclabel{overview-objects-traits}
+
+A great deal of programming can be done simply through the use of
+functions, top-level
+variables, and standard types. However, Fortress also includes a trait and object system for
+defining new types, as well as objects that belong to them. Traits in Fortress exist in
+a multiple inheritance hierarchy rooted at trait \TYP{Object}.
+A trait declaration includes a set of method declarations,
+some of which may be abstract.
+For example, here is a declaration of a simple trait named \TYP{Moving}:
+
+\label{movingDim}
+\input{\home/preliminaries/examples/Overview.Moving.tex}
+
+The set of traits extended by trait \TYP{Moving} are listed in braces after
+\KWD{extends}. Trait \TYP{Moving} inherits all
+methods declared by each trait it extends.
+The two methods \VAR{position} and \VAR{velocity} declared in trait \TYP{Moving}
+are \emph{abstract}; they contain no body.
+Their return types are vectors of length 3, whose elements are
+of type \EXP{\mathbb{R}}.
+As in mathematical notation,
+a vector of length $n$ with element type $T$ is written
+\EXP{T^{n}}.
+
+Traits can also declare concrete methods,
+as in the following example:
+
+\label{fastDim}
+\input{\home/preliminaries/examples/Overview.Fast.tex}
+
+Trait \TYP{Fast} extends a single trait, \TYP{Moving}. (Because it extends
+only one trait, we can elide the braces in its \KWD{extends} clause.)
+It inherits both abstract methods defined in \TYP{Moving}, and it provides
+a concrete body for method \VAR{velocity}.
+
+Trait declarations can be extended by other trait declarations,
+as well as by \emph{object declarations}.
+There are two kinds of object declarations:
+\emph{singleton declarations} and
+\emph{constructor declarations}.
+
+A singleton declaration declares a sole, stand-alone, \emph{singleton object}.
+For example:
+\input{\home/preliminaries/examples/Overview.Sol.tex}
+
+The object \TYP{Sol} extends two traits: \TYP{Moving} and \TYP{Stellar},
+and provides definitions for the abstract methods it inherits. Objects must
+provide concrete definitions for all abstract methods they inherit. \TYP{Sol}
+also defines a field \VAR{spectralClass}.
+For every field included in an object
+definition, an implicit getter is defined for that field. Calls to
+the getter of the field of an object consist of an expression
+denoting the object
+followed by a dot and the name of the field. For example, here is a call to the
+getter \VAR{spectralClass} of object \TYP{Sol}:
+
+
+
+%Sol.spectralClass
+\begin{Fortress}
+\(\TYP{Sol}.\VAR{spectralClass}\)
+\end{Fortress}
+
+If a field includes modifier \KWD{settable},
+an implicit setter is defined for the
+field. Calls to setters look like assignments.
+Here is an assignment to field \VAR{spectralClass}
+of object \TYP{Sol}:
+
+%Sol.spectralClass := G3
+\begin{Fortress}
+\(\TYP{Sol}.\VAR{spectralClass} \ASSIGN G_{3}\)
+\end{Fortress}
+
+In fact,
+all accesses to a field from outside the object to which the field belongs
+must go through the getter of the field, and all assignments to it must go
+through the setter. (There is simply no other way
+syntactically to refer to the field.)
+
+If a field includes modifier \KWD{hidden}, no implicit getter is defined for the object.
+
+
+The self parameter of a method can be given a position other than the default
+position. For example, here is a definition of a type where the
+self parameters appear in nonstandard positions:
+
+\input{\home/preliminaries/examples/Overview.List.tex}
+
+In both methods \VAR{cons} and \VAR{append}, the self parameter occurs as the second parameter.
+Calls to these methods look more like function calls than method calls. For example, in the following
+call to \VAR{append}, the receiver of the call is \EXP{l_{2}}:
+
+\input{\home/preliminaries/examples/Overview.append.tex}
+
+
+A constructor declaration declares an \emph{object constructor}.
+In contrast to singleton declarations, a constructor declaration includes
+value parameters in its header, as in the following example:
+\label{particleDim}
+\input{\home/preliminaries/examples/Overview.Particle.tex}
+
+Every call to the constructor of \TYP{Particle} yields a new object.
+For example:
+\input{\home/preliminaries/examples/Overview.p1.tex}
+
+The parameters to an object constructor implicitly define
+fields of the object, along with their getters (by default). These parameters
+can include all of the modifiers that an ordinary field can. For example,
+a parameter can include the modifier \KWD{hidden}, in which case a getter
+is not implicitly defined for the field.
+
+In the definition of \TYP{Particle}, it is the implicitly defined getters of
+fields \VAR{position} and \VAR{velocity} that provide concrete definitions
+for the inherited abstract methods from trait \TYP{Moving}.
+
+In both singleton and constructor declarations,
+implicitly defined getters and setters can be overridden by defining
+explicit getters and setters,
+using the modifiers \KWD{getter} and \KWD{setter}. For example,
+we alter the definition
+of \TYP{Particle} to include an explicit
+getter for field \VAR{velocity} as follows:
+
+%object Particle(position : (RR Length)^3,
+%                velocity : (RR Velocity)^3)
+%  extends Moving
+%  getter velocity() = do
+%    print "velocity getter accessed"
+%    velocity
+%  end
+%end
+\begin{Fortress}
+\(\KWD{object} \TYP{Particle}(\null\)\pushtabs\=\+\(\VAR{position} \mathrel{\mathtt{:}} (\mathbb{R}\mskip 4mu plus 4mu\TYP{Length})^{3},\)\\
+\(                \VAR{velocity} \mathrel{\mathtt{:}} (\mathbb{R}\mskip 4mu plus 4mu\TYP{Velocity})^{3})\)\-\\\poptabs
+{\tt~~}\pushtabs\=\+\(  \KWD{extends} \TYP{Moving}\)\\
+\(  \KWD{getter} \VAR{velocity}() = \;\KWD{do}\)\\
+{\tt~~}\pushtabs\=\+\(    \VAR{print}\;\hbox{\rm``\STR{velocity~getter~accessed}''}\)\\
+\(    \VAR{velocity}\)\-\\\poptabs
+\(  \KWD{end}\)\-\\\poptabs
+\(\KWD{end}\)
+\end{Fortress}
+
+The explicitly defined getter first prints a message and then returns
+the value of the
+field \VAR{velocity}. \emph{Note that the final variable reference in this getter refers
+directly to the field \VAR{velocity}, not to the getter.} Only within an object definition
+can fields be accessed directly. In fact, even in an object definition, fields are only
+accessed directly when they are referred to as simple variables. In the following definition
+of \TYP{Particle}, the getter \VAR{velocity} is recursively accessed through the special variable
+\KWD{self} (bound to the receiver of the method call):
+
+%object Particle(position : (RR Length)^3,
+%                velocity : (RR Velocity)^3)
+%  extends Moving
+%  getter velocity() = do
+%    print "velocity getter accessed"
+%    self.velocity
+%  end
+%end
+\begin{Fortress}
+\(\KWD{object} \TYP{Particle}(\null\)\pushtabs\=\+\(\VAR{position} \mathrel{\mathtt{:}} (\mathbb{R}\mskip 4mu plus 4mu\TYP{Length})^{3},\)\\
+\(                \VAR{velocity} \mathrel{\mathtt{:}} (\mathbb{R}\mskip 4mu plus 4mu\TYP{Velocity})^{3})\)\-\\\poptabs
+{\tt~~}\pushtabs\=\+\(  \KWD{extends} \TYP{Moving}\)\\
+\(  \KWD{getter} \VAR{velocity}() = \;\KWD{do}\)\\
+{\tt~~}\pushtabs\=\+\(    \VAR{print}\;\hbox{\rm``\STR{velocity~getter~accessed}''}\)\\
+\(    \mathord{\KWD{self}}.\VAR{velocity}\)\-\\\poptabs
+\(  \KWD{end}\)\-\\\poptabs
+\(\KWD{end}\)
+\end{Fortress}
+
+Now, the result of a call to getter \VAR{velocity} is an infinite loop (along with a lot of output).
+
+\subsection{Traits, Getters, and Setters}
+Although traits do not include field declarations, they can include getter and setter declarations, as in the following
+alternative definition of trait \TYP{Moving}:
+
+%trait Moving extends { Tangible, Object }
+%  getter position(): (RR Length)^3
+%  getter velocity(): (RR Velocity)^3
+%end
+\begin{Fortress}
+\(\KWD{trait} \TYP{Moving} \KWD{extends} \{\,\TYP{Tangible}, \TYP{Object}\,\}\)\\
+{\tt~~}\pushtabs\=\+\(  \KWD{getter} \VAR{position}()\COLON (\mathbb{R}\mskip 4mu plus 4mu\TYP{Length})^{3}\)\\
+\(  \KWD{getter} \VAR{velocity}()\COLON (\mathbb{R}\mskip 4mu plus 4mu\TYP{Velocity})^{3}\)\-\\\poptabs
+\(\KWD{end}\)
+\end{Fortress}
+
+Now, an object extending trait \TYP{Moving} must provide the definitions of
+\emph{getters} (as opposed to ordinary methods)
+for \VAR{position} and \VAR{velocity}.
+The advantage of this definition is that we can use getter
+notation on a variable of static type \TYP{Moving}:
+
+% v : Moving = ...
+% v.position
+\begin{Fortress}
+{\tt~}\pushtabs\=\+\( v \mathrel{\mathtt{:}} \TYP{Moving} = \ldots\)\\
+\( v.\VAR{position}\)\-\\\poptabs
+\end{Fortress}
+
+In fact, getters can be declared in a trait definition using field declaration syntax, as in the following example
+(which is equivalent to the definition of \TYP{Moving} above):
+
+%trait Moving extends { Tangible, Object }
+%  position: (RR Length)^3
+%  velocity: (RR Velocity)^3
+%end
+\begin{Fortress}
+\(\KWD{trait} \TYP{Moving} \KWD{extends} \{\,\TYP{Tangible}, \TYP{Object}\,\}\)\\
+{\tt~~}\pushtabs\=\+\(  \VAR{position}\COLON (\mathbb{R}\mskip 4mu plus 4mu\TYP{Length})^{3}\)\\
+\(  \VAR{velocity}\COLON (\mathbb{R}\mskip 4mu plus 4mu\TYP{Velocity})^{3}\)\-\\\poptabs
+\(\KWD{end}\)
+\end{Fortress}
+
+Getter declarations in trait definitions must not include bodies.
+A getter declaration can include the various modifiers
+allowed on a field declaration, with similar results.
+For example, if the modifier \KWD{settable} is used, then a
+setter is implicitly declared, in addition to a getter.
+
+\section{Features for Library Development}
+The language features introduced above are sufficient for the vast majority of applications programming. However, Fortress
+has also designed to be a good language for \emph{library} programming. In fact, much of the Fortress language as viewed
+by applications programmers actually consists of code defined in libraries, written in a small core language. By defining as
+much of the language as possible in libraries, our aim is to allow the language to evolve gracefully as new demands are placed on it.
+In this section, we briefly mention some of the features that make Fortress a good language for library development.
+
+\subsection{Generic Types and Static Parameters}
+As in other languages, Fortress allows types to be parametric with respect to other types, as well as other ``static'' parameters,
+including integers, booleans, dimensions, units, and operators.
+Fortress provides some standard parametric types,
+such as \TYP{Array} and \TYP{Vector}.
+Programmers can also define new traits, objects, and functions that include static parameters.
+
+\subsection{Specification of Locality and Data Distribution}
+Fortress includes a facility for expressing programmer intent concerning the distribution of large data structures
+at run time. This intent is expressed through special data structures called \emph{distributions}.
+In fact, all arrays and matrices include distributions. These distributions
+are defined in \library.
+In most cases, the default distributions
+will provide programmers with good performance over a variety of machines. However, in some circumstances,
+performance can be improved by overriding the default selection of distributions.
+Moreover, some programmers might wish to define new distributions, tailored for particular
+platforms and programs.
+
+\subsection{Operator Overloading}
+Operators in Fortress can be overloaded with new definitions.
+Here is an alternative definition of the \VAR{factorial} function, defined as a postfix operator:
+
+\input{\home/preliminaries/examples/Overview.factorial.tex}
+
+As with mathematical notation, Fortress allows operators to be defined as prefix, postfix,
+and infix. More exotic operators can even be defined as subscripting (i.e., applications of the
+operators look like subscripts), and as bracketing (i.e., applications of the operators
+look like the operands have been simply enclosed in brackets).
+
+\subsection{Definition of New Syntax}
+Fortress provides a facility for the definition of new syntax in libraries.
+This facility is useful for defining libraries for domain-specific languages,
+such
+as SQL, XML, etc.
+It is also used to encode some of
+the language constructs seen by applications
+programmers.

trunk/Specification/preliminaries/preliminaries.tex

@@ -20 +20 @@
 
 \input{\home/preliminaries/intro/intro}
-\input{\home/preliminaries/overview/overview}
+\input{\home/preliminaries/overview}