From: Peter Amey <peter.amey@praxis-cs.co.uk>
Subject: Re: Where is "Anna" -- an old Ada language extenstion
Date: Sat, 12 May 2007 21:19:37 +0100
Date: 2007-05-12T21:19:37+01:00 [thread overview]
Message-ID: <46462159.80806@praxis-cs.co.uk> (raw)
In-Reply-To: Pine.LNX.4.64.0705111029090.31686@th.informatik.uni-mannheim.de
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
next prev parent reply other threads:[~2007-05-12 20:19 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2007-05-11 8:35 Where is "Anna" -- an old Ada language extenstion Stefan Lucks
2007-05-11 9:00 ` Lutz Donnerhacke
2007-05-11 17:43 ` Manuel Collado
2007-05-12 20:19 ` Peter Amey [this message]
2007-05-12 21:56 ` Ed Falis
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox