[SystemSafety] systemsafety Digest, Vol 66, Issue 5

[Derek M Jones]

Rod,

Does "100% OK" mean that 2 faults per thousand lines of code
are OK?

This is the fault rate found in the paper:
"Tokeneer: Beyond Formal Program Verification"
www.open-do.org/wp-content/uploads/2010/04/ERTS2010_final.pdf

> the SPARK theorem prover ... the teams at Altran use "proof 
> completeness" (i.e.
> essentially the false alarm rate of the prover) as a pre-commit target. 
> Bottom line -
> either the theorem prover says your code is 100% OK with no false 
> alarms, or it doesn't
> go into CM.

-- 
Derek M. Jones           Software analysis
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com