Re: Lost in translation (with SPARK user rules)

[Pascal Obry <pascal@obry.net>]

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