Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!snorkelwacker.mit.edu!apple!agate!shelby!neon!sankar
From: sankar@Neon.Stanford.EDU (Sriram Sankar)
Newsgroups: comp.specification
Subject: re. survey on spec. languages (Anna references)
Message-ID: <1990Dec26.183630.11596@Neon.Stanford.EDU>
Date: 26 Dec 90 18:36:30 GMT
Sender: sankar@Neon.Stanford.EDU (Sriram Sankar)
Organization: Computer Science Department, Stanford University
Lines: 54


There is a new book out on Anna, details of which are included below.
For a complete survey on Anna, you may need many more references -
the book lists many of them.  If someone wants more info on these
other references, they should send me mail.

Sriram Sankar
Research Associate
ERL449, Computer Systems Lab
Stanford University
Stanford, CA94305

sankar@cs.stanford.edu

============================

"Programming with Specifications
 An Introduction to Anna,
 A Language for Specifying Ada Programs"
             by
       David Luckham

 published by Springer Verlag in "Texts and Monographs
 in Computer Science", 416 pages, Oct 1990.

>From the book's cover:

Specifications express information about a program that is not
normally part of the program, and often cannot be expressed in a
programming language.  This book describes how to write specifications
in Anna, and how to use specifications in the process of building
programs, debugging them, and interfacing them with other programs.
"Programming with specifications" opens up a whole new area of
programming, describing new strategies and styles of programming that
utilize specifications.

In order to present programming with specifications in the context of
building and testing modern large modular systems, the book focusses
on the use of specifications to develop Ada programs.  Specifications
are written in a machine - processable language called Anna, which is
an extension of Ada.  This book explains Anna and describes methods of
using it. Topics covered include simple annotations for the Pascal -
like subset of Ada, annotation of exceptions, package specifications,
annotation and construction of package bodies, and rigorous software
development methods that utilize specifications.

The methods of programming with specifications can be applied to other
programming languages such as Pascal, C++, and Modula-2. The reader
will easily be able to adapt these methods to any programming language
of choice.

This book is intended for use by professional software engineers,
students in computer science and software engineering, and programmers
who wish to become more disciplined in their programming methods.