Where is "Anna" -- an old Ada language extenstion

Where is "Anna" -- an old Ada language extenstion

[Stefan Lucks]

Hi all,

Anna is an old language extension of Ada (Ada 83, as I believe) to include 
facilities for formally specifying the intended behavior of Ada programs.

As understand, Anna is bit like today's SPARK. See
   http://pavg.stanford.edu/previous_research/index.html

Unfortunately, I cannot find her on the Web -- both documents and software 
seem to have disappeared. Can anybody tell me where I could find Anna? I 
would like to explore the tools and to compare them with SPARK.

Thank you


-- 
Stefan Lucks      Th. Informatik, Univ. Mannheim, 68131 Mannheim, Germany
             e-mail: lucks@th.informatik.uni-mannheim.de
             home: http://th.informatik.uni-mannheim.de/people/lucks/
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------

Re: Where is "Anna" -- an old Ada language extenstion

[Lutz Donnerhacke]

* Stefan Lucks wrote:
> Unfortunately, I cannot find her on the Web -- both documents and software 
> seem to have disappeared. Can anybody tell me where I could find Anna? I 
> would like to explore the tools and to compare them with SPARK.

Most of the publish material was available from archive.org about four years
ago.

Re: Where is "Anna" -- an old Ada language extenstion

[Manuel Collado]

Stefan Lucks escribi�:
> Hi all,
> 
> Anna is an old language extension of Ada (Ada 83, as I believe) to 
> include facilities for formally specifying the intended behavior of Ada 
> programs.
> 
> As understand, Anna is bit like today's SPARK. See
>   http://pavg.stanford.edu/previous_research/index.html
> 
> Unfortunately, I cannot find her on the Web -- both documents and 
> software seem to have disappeared...

Have you attempted to follow the given links?

> ... Can anybody tell me where I could 
> find Anna? I would like to explore the tools and to compare them with 
> SPARK.

It seems that the files are still there:

    ftp://pavg.stanford.edu/pub/anna/read.me
    ftp://pavg.stanford.edu/pub/anna/
    ...

Regards.
-- 
Manuel Collado - http://lml.ls.fi.upm.es/~mcollado

Re: Where is "Anna" -- an old Ada language extenstion

[Peter Amey]

Stefan Lucks wrote:
> Hi all,
> 
> Anna is an old language extension of Ada (Ada 83, as I believe) to 
> include facilities for formally specifying the intended behavior of Ada 
> programs.
> 
> As understand, Anna is bit like today's SPARK. See
>   http://pavg.stanford.edu/previous_research/index.html
> 
> [snip]

I can't help you with the location of the Anna archives (although others 
have) but I can help with its relationship with SPARK.  ANNA is an 
acronym which is something like "Annotation Language for Ada".  Like 
SPARK, the idea was to add annotations (e.g. pre/post conditions) to 
subprograms to facilitate proof using Hoare logic.  ANNA was more 
ambitious than SPARK because it attempted to cover the entire Ada 
language.  I am not sure there ever were any ANNA tools.

When we designed SPARK we found it necessary to limit the full Ada 
language in various ways to make it unambiguous so that the proofs 
actually meant something!

Peter Amey

www.sparkada.com

Re: Where is "Anna" -- an old Ada language extenstion

[Ed Falis]

On Sat, 12 May 2007 16:19:37 -0400, Peter Amey  
<peter.amey@praxis-cs.co.uk> wrote:

> I am not sure there ever were any ANNA tools.

There were.  I was on the team in 82-3.