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

From: David Crocker < >
Date: Wed, 26 Feb 2014 17:36:45 +0000

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.

The System Safety Mailing List
systemsafety_at_xxxxxx Received on Wed Feb 26 2014 - 18:37:00 CET

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:06 CEST