sankar@Neon.Stanford.EDU (Sriram Sankar) (01/09/91)
An earlier message of mine generated many responses in comp.lang.ada.
I am posting the standard response sent out to people who send in their
first message to anna-request@anna.stanford.edu requesting for info.
Please read this and please get in touch with us for more information.
Sriram Sankar.
Information on Anna and the Anna Tools
Introduction
------------
Anna is a language extension of Ada to include facilities for formally
specifying the intended behavior of Ada programs. It is designed to
meet a perceived need to augment Ada with precise machine-processable
annotations so that well established formal methods of specification
and documentation can be applied to Ada programs.
Language
--------
Reference Manual:
The Anna language is described in many documents. The most readily
available source of information on the language is the Springer-Verlag
_Anna Reference Manual_, volume 260 of the Lecture Notes in
Computer Science series. The primary author is David C. Luckham.
This manual may be purchased at any computer bookstore, and is
probably available in any mathematical reference library.
Introduction to Anna:
An introductory text on using Anna is available now, (Oct, 1990)
published by Springer Verlag in their _Silver series_,
Texts and Monogrpahs in Computer Science. The title of this book is
_Programming with Specifications: An Introduction to ANNA, A
Language for Specifying Ada Programs_, by David C. Luckham.
Various aspects of the Anna language and Anna tools have been documented
in technical reports and published papers. See the bibliography for
a complete list of applicable documents.
Anna Tools
----------
The Program and Analysis Group at Stanford University has developed a
prototype environment supporting the Anna language. The first release
of this environment, Anna-I, is available to anyone who wishes to
experiment with it. The tools implement a large subset of the Ada and
Anna languages. These tools include:
-- Front-End Parser Generator
-- Intermediate Representation Toolkit (Extended DIANA Formal
Interface and Implementation packages (AST), Ada/Anna Parser,
Ada/Anna Pretty Printer, AST Disk<==>Memory package)
-- Ada/Anna Static-Semantic Rules Checker
-- Annotation Transformer
-- Portable Ada/Anna Testing and Debugging System
-- Anna Interactive Tutorial System
The Anna-I tools are completely implemented in Ada, though a small
amount of X-Windows and Verdix VADS dependency may exist in some of
the user-interfaces, depending on the version.
The Parser Generator generates LALR(1) parse tables. Also generated
is an Ada package used to input the tables from disk and to define the
class of nodes in an AST. The parse tables are used by the Parser
to construct an AST from an Anna source program. The Semantic Checker
checks the static-semantics of the Ada and Anna code in the AST: it
works in both batch and incremental modes. The Pretty Printer
generates ASCII text given an AST. The AST IR interface defines the
common internal representation used by all the Anna-I tools -- routines
are exported that allow traversal and data manipulation of an AST.
The AST Disk<==>Memory package performs AST disk-to-memory conversions,
and vice versa.
The Annotation Transformer maps an Anna program to an equivalent Ada
program. That is, the Transformer replaces Anna constructs with
appropriate Ada constructs in order to build a self-checking program.
The Testing and Debugging system can then be used to monitor the
run-time behavior of the transformed program. Currently, the Testing
and Debugging system is provided with a small, command-line interface,
and for some releases, an X-Windows and Emacs editor interface.
The Anna Interactive Teaching Tutorial is an interactive tutorial for
Anna. It is designed to familiarize the user with basic Anna concepts
and language facilities. Several "hands-on" exercises are included.
Anna Teach automatically invokes other Anna tools and the Ada compiler
to check the correctness of exercises entered by the user.
We are currently developing other Anna-I tools that include:
-- Ada Logic Reasoning System (abstract PROLOG-like database)
-- Package Specification Analyzer
-- Parallel Testing and Debugging System (for Sequent Symmetry)
-- more robust incremental semantics capabilities for Ada and Anna
Available Anna Releases
-----------------------
Anna-I is immediately available for the following systems:
-- Sun/3 UNIX version 4.0.3, Verdix VADS 6.0.3(c) Ada compiler
-- Sequent Symmetry DYNIX (i386), SLI/Verdix VADS 5.5.2 Ada compiler
Anna-I is available for the Sun/3 UNIX version 3.5, Verdix VADS
5.7(d) though it is no longer supported by Stanford University.
The same is true for the Sun/3 UNIX version 4.0.3, Verdix VADS
5.7(d) release.
Contact us regarding the possibility of rehosting Anna onto different
systems.
FTP Availability
----------------
Anonymous FTP for the Anna-I environment and various Anna papers are
available on the Internet host "anna.stanford.edu" ([36.14.0.13]).
Not all Anna-I releases are available by this means. Make sure to
read the "read.me" file before transferring any files.
Also, if you do acquire the Anna tools via FTP, please let us know;
we like to keep track of who is using the tools, and how.
Acquiring the Anna-I Tools
--------------------------
If the FTP acquisition method is not a viable option, you may obtain
an Anna-I release through postal mail.
The Anna-I release requires two 9-track, 1600-bpi magnetic tapes for a
Sun/3 release (one for the Anna-I tools and one for the X-Windows
interface used by the Anna-I tools). The Anna-I Sequent Symmetry
release requires only one magnetic tape (an X-Windows interface is not
available for this release). All releases include an installation
guide and user's manual. To obtain an Anna-I release, please send us
tapes and a self-addressed, stamped, return package with applicable
postage to:
Stanford Anna Team
Computer Systems Lab, ERL 456
Stanford University
Stanford, CA 94305
NOTE: Include enough postage to cover the cost of sending the
magnetic tape(s) plus a 75 page document.
Due to the considerable time and resources required to produce an
Anna-I release, as well as the available hardware we have, we are not
currently able to produce releases of Anna-I in any other format. We
do not have a Sun/3 cartridge drive readily available. We do not have
a VAX/VMS system so we cannot provide any VAX/VMS tape format release
of the Anna-I tools.
Most of the Anna tools rely on the use of the Verdix VADS compiler.
We do not have releases for any other compiler. But see the next
section for information regarding source code releases of Anna-I.
Please inform us which version of the Anna-I tools you would like
(Sun/3 OS 4.0.3 with Verdix VADS 5.7(d), Sun/3 OS 3.5 with Verdix VADS
5.7(d), Sun/3 OS 4.0.3 with Verdix VADS 6.0 (available in mid-to-late
1990), or Sequent Symmetry DYNIX SLI/VADS 5.5.2). If you have any
questions, contact the Stanford Anna Team at (415) 723-1175.
Anna Source Code
----------------
Users who do not have a system which we currently support may wish to
inquire as to the availability of the Anna source code so that they
may port Anna-I to a different target environment. Please contact
Walter Mann or Sriram Sankar for details.
Source code releases are subject to the approval of Professor David C.
Luckham, and generally require some kind of non-disclosure agreement.
Support
-------
Support for learning Anna and the tool set is very limited. A short
one-day tutorial course will soon be available at a fee. Contact us
for details regarding Anna language and tools support.
An Anna User's Group is now being supported through Internet
electronic mail. Annoucements of new releases, new tools, bug fixes,
etc. will be posted through this medium. To obtain information about
being added to the list, please contact us as the following address,
phone, or electronic mail:
Stanford Anna Team
Computer Systems Lab, ERL 456
Stanford University
Stanford, CA 94305
(415) 723-1175 (voice)
(415) 725-7398 (fax)
anna-request@anna.stanford.edu
Bibliography
------------
_Reference Manual for the Ada Programming Language_.
U. S. Department of Defense, U. S. Government Printing Office,
ANSI/MIL-STD-1815A edition, January 1983.
Douglas L. Bryan and Geoffrey O. Mendal.
_Exploring Ada, Volume 1_.
Prentice-Hall, Englewood Cliffs, New Jersey, 1989.
Rob Chang.
"ParseGen: A LALR(1) Parser Generator".
Technical Note 85-283, Stanford University, November 1985.
G. Goos, W. A. Wulf, A. Evans Jr., and K. J. Butler.
_DIANA, An Intermediate Language for Ada_.
Volume 161 of _Lecture Notes in Computer Science_,
Springer-Verlag, 1983.
D. C. Luckham, Randall Neff, and David Rosenblum.
_An Environment for Ada Software Development Based on Formal
Specification_.
Technical Report CSL-TR-86-305, Stanford University, August 1986.
Also published as an article in Ada Letters, VII(3):94--106,
May/June 1987.
David Luckham, Sriram Sankar, and Shuzo Takahashi.
"Two Dimensional Pinpointing: An Application of Formal
Specification to Debugging Packages".
Technical Report CSL-TR-89-379, Stanford University, April 1989.
David C. Luckham.
_Programming with Specifications: An Introduction to ANNA,
A Language for Specifying Ada Programs_.
_Texts and Monographs in Computer Science_, Springer-Verlag,
October 1990, 412 pages.
David C. Luckham, Friedrich W. von Henke, Bernd Krieg-Brueckner, and Olaf
Owe.
_ANNA, A Language for Annotating Ada Programs_, Reference Manual,
Volume 260 of _Lecture Notes in Computer Science_,
Springer-Verlag, 1987, 143 pages.
Geoffrey O. Mendal.
"Designing for Ada reuse: A case study".
In _IEEE Computer Society Second International Conference on Ada
Applications and Environments_, pages 33--42, IEEE Computer Society, Miami
Beach, Florida, 8-10 April 1986.
Also published as a Stanford University Technical Report, June 1986,
CSL-86-299.
Geoffrey O. Mendal.
"The Anna-I User's Guide and Installation Manual".
Stanford University, Computer Systems Lab, ERL 456, Stanford, California,
release 3C edition, January 1990.
Randall Neff.
_Ada/Anna Specification Analysis_.
PhD thesis, Stanford University, Stanford, California, December 1989.
Also published as a Stanford University technical report, CSL-TR-89-406.
David S. Rosenblum.
_A Methodology for the Design of Ada Transformation Tools in a
DIANA Environment_.
Technical Report 85-269, Stanford University, February 1985.
Also published in IEEE Software, 2(2):24--33, March 1985.
David Rosenblum, Sriram Sankar, and David C. Luckham.
"Concurrent Runtime Checking of Annotated Ada Programs".
Technical Report CSL-TR-86-312, Stanford University, November 1986.
Sriram Sankar.
_Automatic Runtime Consistency Checking and Debugging of Formally
Specified Programs_.
PhD thesis, Stanford University, Stanford, California, July 1989.
Sriram Sankar and David Rosenblum.
"The Complete Transformation Methodology for Sequential Runtime
Checking of An Anna Subset".
Technical Report CSL-86-301, Stanford University, June 1986.