Checking Ada against formal specifications.

Checking Ada against formal specifications.

[xorquewasp]

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)).

Re: Checking Ada against formal specifications.

[Martin]

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

Re: Checking Ada against formal specifications.

[info]

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

Re: Checking Ada against formal specifications.

[Georg Bauhaus]

xorquewasp@googlemail.com schrieb:
>(regardless, the SPARK
> binaries crash on my copy of debian

Try increasing the stack limit.  Has worked for me.

> and don't work at all on
> my actual development platform (FreeBSD)).

Re: Checking Ada against formal specifications.

[xorquewasp]

Georg Bauhaus wrote:
> xorquewasp@googlemail.com schrieb:
> >(regardless, the SPARK
> > binaries crash on my copy of debian
>
> Try increasing the stack limit.  Has worked for me.

I'll give it a go, but it's an actual Segmentation Fault
as opposed to a Storage_Error so I'm more suspicious
of some sort of strange binary incompatibility.

Re: Checking Ada against formal specifications.

[Georg Bauhaus]

xorquewasp@googlemail.com schrieb:
> Georg Bauhaus wrote:
>> xorquewasp@googlemail.com schrieb:
>>> (regardless, the SPARK
>>> binaries crash on my copy of debian
>> Try increasing the stack limit.  Has worked for me.
> 
> I'll give it a go, but it's an actual Segmentation Fault

Yes, likely -fstack-check had not been enabled
when building the SPARK programs (spark, sparksimp, etc.).
There will be a Segmentation Fault then, not Storage_Error
whenever there is a storage error caused by default stack size.

> as opposed to a Storage_Error so I'm more suspicious
> of some sort of strange binary incompatibility.

Re: Checking Ada against formal specifications.

[xorquewasp]

http://libre.adacore.com/libre/tools/spark-gpl-edition/

Well, that shut me up.

Re: Checking Ada against formal specifications.

[roderick.chapman]

On Jun 4, 8:06 pm, xorquew...@googlemail.com wrote:
> http://libre.adacore.com/libre/tools/spark-gpl-edition/
>
> Well, that shut me up.

Err...yeah...congratulations on being the first person on c.l.a to
spot this... :-)
 - Rod Chapman, SPARK Team

Re: Checking Ada against formal specifications.

[xorquewasp]

roderick.chap...@googlemail.com wrote:
> Err...yeah...congratulations on being the first person on c.l.a to
> spot this... :-)
>  - Rod Chapman, SPARK Team

Thanks for the excellent work, Rod.

I'll be attempting to port this to FreeBSD in due course.

Re: Checking Ada against formal specifications.

[roderick.chapman]

On Jun 4, 9:05 pm, xorquew...@googlemail.com wrote:
> roderick.chap...@googlemail.com wrote:
> > Err...yeah...congratulations on being the first person on c.l.a to
> > spot this... :-)
> >  - Rod Chapman, SPARK Team
>
> Thanks for the excellent work, Rod.
>
> I'll be attempting to port this to FreeBSD in due course.

The Ada-based tools should be trivial to port - we've worked
really hard to make this work on all platforms straight out of the
box with GNAT GPL 2009 or almost any recent build of GNAT Pro.

The PROLOG-based tools (Simplifier and Checker) could be
more problematical, since we currently use the SICSTUS PROLOG
compiler.  A port to GNU PROLOG would be an interesting little
project to try.

All the best,
 Rod