Re: Does anyone use Anna?

[Lao Xiao Hai <laoxhai@ix.netcom.com>]

JF Harrison wrote:

> Hi,
>   While searching through Amazon.com I found the following text: "Anna : A
> Language for Annotating Ada Programs : A Reference Manual (Lecture Notes in
> Computer Science, Vol 260)" by David Luckham.  Is this used much in the
> industry?  If not, does it look like it will be?
>
> Regards,
> JF Harrison

The Center for Reliable Computing at Stanford University had some researchers,
Doug Bryan and Geoff Mendal, working on ANNA.   Both have left the Ada community

and there seems to be no effort currently in place.  I don't think ANNA has ever
been
updated to correspond to Ada 95.  This would make a really good research project

for someone if there were any possibility of getting it funded.

Richard Riehle


>
> From the book description at
> http://www.amazon.com/exec/obidos/ASIN/0387179801/qid=975111777/sr=1-4/104-1
> 905124-4917565
>
> "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. The current ANNA design includes annotations
> of all ADA constructs except tasking. Similar extensions for formal
> specification can be made to other Algol-like languages such as Pascal,
> PL/1, Concurrent Pascal, and Modula; essentially, these extensions would be
> subsets of ANNA. The design of ANNA was undertaken from the beginning with
> four principal considerations: 1. Constructing annotations should be easy
> for the ADA programmer and should depend as much as possible on notation and
> concepts of ADA. 2. ANNA should possess language features that are widely
> used in the specification and documentation of programs. 3. ANNA should
> provide a framework within which the various established theories of
> formally specifying programs may be applied to ADA. 4. Annotations should be
> equally well suited for different possible applications during the life
> cycle of a program. Such applications include not only testing, debugging
> and formal verification of a finished program, but also specification of
> program parts during the earlier stages of requirements analysis and program
> design."