From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-0.8 required=5.0 tests=BAYES_00,INVALID_DATE autolearn=no autolearn_force=no version=3.4.4 Xref: utzoo comp.lang.ada:4692 comp.specification:243 Path: utzoo!censor!geac!torsqnt!lethe!yunexus!ists!helios.physics.utoronto.ca!news-server.csri.toronto.edu!cs.utexas.edu!wuarchive!zaphod.mps.ohio-state.edu!uwm.edu!bionet!agate!shelby!neon!sankar From: sankar@Neon.Stanford.EDU (Sriram Sankar) Newsgroups: comp.lang.ada,comp.specification Subject: The Stanford University Anna Toolset (info follows) Message-ID: <1991Jan8.183238.15124@Neon.Stanford.EDU> Date: 8 Jan 91 18:32:38 GMT Sender: sankar@Neon.Stanford.EDU (Sriram Sankar) Organization: Computer Science Department, Stanford University List-Id: 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.