FYI, tasking (a Ravenscar profile of tasking anyway) has just been added to SPARK. Adding generics (that's templates to C++-types) is a medium term goal.
Or the companies who want to save money by not having to do so many man-hour hungry unit tests or post-release bug fixes...
LockheadMartin have presented project using the highest level of DO-178B as cost 1/4 of (yes, "of" not "off") of similar non-Level A projects. There were many reasons for that, of course, but I'm sure that SPARK and similar tools played their part.
Er, you obviously missed out on Ada95 which add OO (yes, polymorphism/inheritance) to the language. Ada0Y (scheduled for 2005) looks very likely to add Java-style "interfaces".
Your experience flies (sorry!:-) in the face of the analysis done by LockheadMartin at Aerosystems International then...
They discovered the delivered Ada projects had a defect rate 1/10 that of delivered C projects and delivered SPARK projects had a defect rate 1/10 that of Ada!
1% of all defects found has safety implications.
It doesn't - that's not what statis analysis is about. To show that what you writen is what was required (i.e. 1+1=2) you still need to do dynamic testing.
These are complimentary tools, not competing.
...and Baysian Probability will bite yer bum!
You can _never_ prove the absense of run-time errors by testing. You can prove it using static analysis tools such as SPARK, or those provided by PolySpace (Ada, C, C++) or SofCheck (Java).
Personally, I find testing as exciting as drying paint, so I'm totally behind using these static analysis tools but it seems there are a lot of people who enjoy unit testing out there...
Slashdot Mirror
Yes it is used extensively on the EuroFighter Typhoon aircraft, Airienne space rocket, Mondex cash cards, etc.
Hmmm, there are certainly people out there who disagree with you! :-) Not just SPARK guys but also PolySpace and SofCheck.
FYI, tasking (a Ravenscar profile of tasking anyway) has just been added to SPARK. Adding generics (that's templates to C++-types) is a medium term goal.
Say "hello" to Alloy-SPARK! :-)
http://www.cee.hw.ac.uk/~air/
Or the companies who want to save money by not having to do so many man-hour hungry unit tests or post-release bug fixes... LockheadMartin have presented project using the highest level of DO-178B as cost 1/4 of (yes, "of" not "off") of similar non-Level A projects. There were many reasons for that, of course, but I'm sure that SPARK and similar tools played their part.
Er, you obviously missed out on Ada95 which add OO (yes, polymorphism/inheritance) to the language. Ada0Y (scheduled for 2005) looks very likely to add Java-style "interfaces".
The "no dynamic memory allocation" is also useful for avoiding fragmenting RAM - pilots get grouchy about that sort of thing! ;-)
Your experience flies (sorry! :-) in the face of the analysis done by LockheadMartin at Aerosystems International then...
They discovered the delivered Ada projects had a defect rate 1/10 that of delivered C projects and delivered SPARK projects had a defect rate 1/10 that of Ada!
1% of all defects found has safety implications.
It doesn't - that's not what statis analysis is about. To show that what you writen is what was required (i.e. 1+1=2) you still need to do dynamic testing. These are complimentary tools, not competing.
...and Baysian Probability will bite yer bum! You can _never_ prove the absense of run-time errors by testing. You can prove it using static analysis tools such as SPARK, or those provided by PolySpace (Ada, C, C++) or SofCheck (Java). Personally, I find testing as exciting as drying paint, so I'm totally behind using these static analysis tools but it seems there are a lot of people who enjoy unit testing out there...
Not every job in the world advertises on Jobserve but granted the number of SPARK jobs out there is small... but growing!
If you have any SPARK experience I know several places that would be interested in a CV.