Re: Ada UK conference: SPARK safety: is no delivery better than 1 defect?

["Michael" <fvit@shaw.ca>]

Hi all,



Thank you for the question Bill.



iFACTS deficiencies and delays are not due to Ada, (the software engineering 
language), but more likely from the SPARK constraints and limitations.

SPARK is made from a subset of Ada and use specific annotations (e.g.: data 
flow or pre and post conditions assertions) to establish a mathematical 
proof of the code correctness.

http://www.adacore.com/wp-content/uploads/2008/10/11_safe_secure_ada_2005_certified_safe_with_spark.pdf



Within large projects, when using C/C++ it becomes increasingly difficult to 
clearly separate design concerns that are scattered into classes.

("The high-integrity C++ coding standard manual" won't help that much 
http://www.literateprogramming.com/CppHighIntegrity.pdf)



Within large projects, when using SPARK it becomes increasingly difficult to 
focus on establishing abstract proof of correctness without compromising 
testing effectiveness.

("Is Proof More Cost Effective than Testing?" won't help either

http://www.praxis-his.com/pdfs/cost_effective_proof.pdf)



Working on too strong abstractions will not left much tools and utilities 
for the operational problems' emulation and testing. Within a proof of 
correctness context, verification and validation procedures might more 
likely be concerned about monitoring divergences than ensuring 
specifications' compliances.



At the opposite Ada is a powerful engineering tool which allows engineers to 
know what they are doing.  And when complexity is increasing, doing it right 
and doing the right think is mostly a consequence of experiences and of a 
mature software engineering process.



The next Ada UK Conference is an opportunity for Praxis to clarifying the 
SPARK capabilities (Tookeneer) and limitations (iFACTS).

http://www.ada-uk-conference.co.uk/programme.html



Cheers



Michael,

Vancouver, BC



CC: to Rod Chapman and Janet Barnes



>
> Do you have any evidence that iFACTS problems are due to the Ada language?
>
> -- 
> Bill Findlay