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-Language: ENGLISH,ASCII
Path: 
 g2news1.google.com!postnews.google.com!c36g2000yqn.googlegroups.com!not-for-mail
From: info@midoan.com
Newsgroups: comp.lang.ada
Subject: Re: Checking Ada against formal specifications.
Date: Wed, 27 May 2009 06:47:20 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <87e61b7c-5d08-49b2-83bb-2fac472ac94c@c36g2000yqn.googlegroups.com>
References: 
 <83d47b94-64bd-41ab-8efe-f142e64bf0f5@s20g2000vbp.googlegroups.com>
	<1da5985e-5e35-48c3-a362-db440c1fae2b@t10g2000vbg.googlegroups.com>
NNTP-Posting-Host: 89.101.123.118
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1243432040 21990 127.0.0.1 (27 May 2009 13:47:20
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Wed, 27 May 2009 13:47:20 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: c36g2000yqn.googlegroups.com; posting-host=89.101.123.118;
	posting-account=X24XNwoAAACSn_ecescZSCM9-2ONsCM_
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB;
 rv:1.9.0.10)
	Gecko/2009042316 Firefox/3.0.10 GTB5 (.NET CLR 3.5.30729),gzip(gfe),gzip(gfe)
Xref: g2news1.google.com comp.lang.ada:5067
Date: 2009-05-27T06:47:20-07:00
List-Id: <comp.lang.ada>

On May 27, 1:26=A0pm, Martin <martin.do...@btopenworld.com> wrote:
> On May 27, 1:19=A0pm, xorquew...@googlemail.com wrote:
>
> > Hello.
>
> > Are there any free tools for checking Ada against external
> > formal specifications (perhaps written in Z or some other
> > language) or annotations?
>
> > I see there used to be one called Anna but the site hosted
> > on stanford.edu seems to have vanished.
>
> > I'm not counting SPARK as a free tool (regardless, the SPARK
> > binaries crash on my copy of debian and don't work at all on
> > my actual development platform (FreeBSD)).
>
> I haven't heard of such a thing for ages...late 80's.
>
> Napier University in Edinburgh, Scotland had a tool that took Z,
> converted that to SML/NJ and then on to Ada83 - don't think it was
> ever release into the open though...
>
> I'd be interested in anything that you uncover!
>
> Cheers
> -- Martin

It really depends what you what the tool to do. If it is total
correctness you are after then, no , no such tool exist for any
programming language.

If you want to check expected properties anywhere in the code then
indeed Spark Ada could help but at the effort involded in not
insignificant.

Otherwise Mika our tool can help if what you want to check can be
expressed in Ada. For example:

...Ada Code
if (your_property)
then Put_line(your_true_message);
else Put_line(your_false_message);
end if;
...Ada Code

Since Mika generates tests for all branches you will get test input
data that makes your_property true (and false) exactly where you want
it.

We will create a better example and put it in http://www.midoan.com/mika.ht=
ml
...

regards,
Midoan