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-Thread: a07f3367d7,ec6f74e58e86b38b X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news4.google.com!proxad.net!feeder1-2.proxad.net!193.252.117.184.MISMATCH!feeder.news.orange.fr!not-for-mail Date: Wed, 26 May 2010 21:32:02 +0200 From: Pascal Obry Organization: Home - http://www.obry.net User-Agent: Mozilla/5.0 (Windows; U; Windows NT 6.0; fr-FR; rv:1.8.1.22) Gecko/20090605 Thunderbird/2.0.0.22 Mnenhy/0.7.5.0 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Lost in translation (with SPARK user rules) References: <0466e131-cc80-4db4-b080-eec9aefcb1c7@z17g2000vbd.googlegroups.com> <4bfd2d05$0$27598$ba4acef3@reader.news.orange.fr> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-15 Content-Transfer-Encoding: 7bit Message-ID: <4bfd7728$0$27592$ba4acef3@reader.news.orange.fr> NNTP-Posting-Date: 26 May 2010 21:31:52 CEST NNTP-Posting-Host: 82.124.201.147 X-Trace: 1274902312 reader.news.orange.fr 27592 82.124.201.147:4253 X-Complaints-To: abuse@orange.fr Xref: g2news2.google.com comp.lang.ada:12047 Date: 2010-05-26T21:31:52+02:00 List-Id: Yannick, > 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. Right. I think the response to this is pragmatism and cost. For non critical softwares do you think it is reasonable to use SPARK? This is only a matter of trade-off I think. > What matters did you encounter with the OS socket binding ? (if this can > be drawn with no excessive difficulties) The fact that your are working on a boundary. The secure SPARK on one side and the OS non-SPARK foreign world. One difficult part was that this is IO (stream like) where data are read from the same socket but two consecutive read won't return the same value. There is way in SPARK to deal with that, to avoid SPARK complaining that you have ineffective code... not straight forward! Pascal. -- --|------------------------------------------------------ --| Pascal Obry Team-Ada Member --| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE --|------------------------------------------------------ --| http://www.obry.net - http://v2p.fr.eu.org --| "The best way to travel is by means of imagination" --| --| gpg --keyserver keys.gnupg.net --recv-key F949BD3B