Re: Lost in translation (with SPARK user rules)

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Wed, 26 May 2010 16:15:41 +0200, Pascal Obry <pascal@obry.net> a écrit:

Hi Pascal,

> Maybe you were expecting something that SPARK is not. SPARK is not a
> replacement for Ada.
Yes, I understand that, I did not had another believe with this

> SPARK is designed for highly secure software.
That is where I was not agree with a previous similar sentence from  
someone else. I don't see a reason why only critical applications should  
benefit of verifiability. This would not be a waste to apply standard  
logic to program construction, and I even feel this should be an expected  
minimum.

> You
> won't create a Web server, an XML parser or even some kind of simulation
> and GUI with it. In those application domains you need full Ada (binding
> to external libraries, generics, full OO, standard libraries Ada.*,
> Interfaces.* and possibly GNAT.*, full text and stream IO...).
For IO, there are ways to have a specification and hide an implementation,  
like SPARK_IO do. For simulation, depends on simulation of what. For GUI,  
I agree, as this mostly have to be plastic. For an XML parser, this should  
be OK, as this is mainly a kind of state-machine. For a web-server, I  
don't have an idea (may be yes for some parts, not for some others).

> I had to create a binding to the OS sockets in SPARK, I can tell you
> that it was not easy... Especially as this was my first experience with
> SPARK!
Well, I was trying to prove a personal implementation of a Deflate stream  
(RFC 1951), decocer/encoder.

What matters did you encounter with the OS socket binding ? (if this can  
be drawn with no excessive difficulties)

> For embedded control-command application that's another story. I think
> that SPARK has something invaluable to offer.
>
> I have also thought that you can mix SPARK and Ada in the same
> application. Using SPARK in the critical part, and Ada for the rest...
> Don't know how well this would work as I have not gone through this yet.
OK, but what made me disappointed, is mainly that I could not make it  
learn/use new rules really properly (well, and the probably coming trouble  
with generics as well). I'm pretty sure that if it would be possible it  
could be used in many more cases than only the so called high-critical  
ones.

> Just my 2 cents of course!
No, was valuable


I may try again, and see can what can be done with this rules problem.


-- 
There is even better than a pragma Assert: a SPARK --# check.