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,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,ec6f74e58e86b38b X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!news4.google.com!feeder2.cambriumusenet.nl!feed.tweaknews.nl!193.201.147.84.MISMATCH!xlned.com!feeder1.xlned.com!news.netcologne.de!newsfeed-fusi2.netcologne.de!newsfeed.straub-nv.de!news.mb-net.net!open-news-network.org!aioe.org!not-for-mail From: =?iso-8859-15?Q?Yannick_Duch=EAne_=28Hibou57=29?= Newsgroups: comp.lang.ada Subject: Re: Lost in translation (with SPARK user rules) Date: Wed, 26 May 2010 21:16:06 +0200 Organization: Ada At Home Message-ID: References: <0466e131-cc80-4db4-b080-eec9aefcb1c7@z17g2000vbd.googlegroups.com> <4bfd2d05$0$27598$ba4acef3@reader.news.orange.fr> NNTP-Posting-Host: VsdMw8HJ6uo7b6guDb/gnA.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-15; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable X-Complaints-To: abuse@aioe.org X-Notice: Filtered by postfilter v. 0.8.2 User-Agent: Opera Mail/10.53 (Win32) Xref: g2news2.google.com comp.lang.ada:12044 Date: 2010-05-26T21:16:06+02:00 List-Id: Le Wed, 26 May 2010 16:15:41 +0200, Pascal Obry a =E9c= rit: 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 expecte= d = minimum. > You > won't create a Web server, an XML parser or even some kind of simulati= on > and GUI with it. In those application domains you need full Ada (bindi= ng > 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 implementatio= n, = 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 shou= ld = 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 wit= h > SPARK! Well, I was trying to prove a personal implementation of a Deflate strea= m = (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 ye= t. 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 troub= le = 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.