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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,f7e8ad90820a834d X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news1.google.com!news4.google.com!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Peter Amey Newsgroups: comp.lang.ada Subject: Re: Where is "Anna" -- an old Ada language extenstion Date: Sat, 12 May 2007 21:19:37 +0100 Message-ID: <46462159.80806@praxis-cs.co.uk> References: Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Trace: individual.net +yXJtJMP+052HkxMtZTd6Az5HL4f7DLNI7urEC6NuwmeZpbVw= User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-US; rv:1.0.2) Gecko/20030208 Netscape/7.02 X-Accept-Language: en-us, en Xref: g2news1.google.com comp.lang.ada:15787 Date: 2007-05-12T21:19:37+01:00 List-Id: 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