Re: Checking Ada against formal specifications.

[info@midoan.com]

On May 27, 1:26 pm, Martin <martin.do...@btopenworld.com> wrote:
> On May 27, 1:19 pm, 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.html
...

regards,
Midoan