[SystemSafety] Scalability of Formal Methods [was: Logic]

[David Crocker]

On 26/02/2014 17:30, Martyn Thomas wrote:
>
> The proof obligations from SPARK are free-standing, in that proving
> them requires no knowledge of the project, the application or the
> software, and they contain no proprietary information. Proving them
> can therefore be easily subcontracted. I expect that the same is true
> for Atelier B.
>
> Martyn
>
That is only true when the obligations are provable. My experience with
annotated development system (admittedly not SPARK) is that developers
often fail to provide some of the trivial preconditions, postconditions,
and in particular loop invariants that are needed to make the proof
possible. Adding these missing annotations without knowledge of the
project/application/software is not necessarily advisable or a safe
thing to do.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20140226/6a1ff2bc/attachment.html>