 SPARK and high integrity software
started 5/20/2004; 8:09:17 AM - last post 5/21/2004; 12:17:09 PM
|
|
Frank Atanassow - SPARK and high integrity software 
5/20/2004; 8:09:17 AM (reads: 153, responses: 5)
|
|
|
There is a discussion
on Slashdot about SPARK, the program invariant annotation software for Ada.
|
|
Frank Atanassow - Re: SPARK and high integrity software
5/20/2004; 8:16:46 AM (reads: 154, responses: 2)
|
|
|
I was struck by this comment:
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.
and this thread, which mentions similar software for Pascal and Java. One of the researchers working on the mentioned JML and ESC/Java2 is Bart Jacobs, who I think is a very clever and knowledgeable guy...
|
|
Ehud Lamm - Re: SPARK and high integrity software
5/20/2004; 9:36:59 AM (reads: 151, responses: 0)
|
|
|
SPARK was discussed here a few times in the past.
|
|
Isaac Gouy - Re: SPARK and high integrity software
5/20/2004; 9:37:24 AM (reads: 146, responses: 0)
|
|
|
|
Dominic Fox - Re: SPARK and high integrity software
5/21/2004; 2:50:47 AM (reads: 95, responses: 1)
|
|
"Static verification may yet become a sexy and fashionable practice!"
Maybe if SPARK used XML syntax...
|
|
Daniel Yokomizo - Re: SPARK and high integrity software
5/21/2004; 12:17:09 PM (reads: 79, responses: 0)
|
|
"Static verification may yet become a sexy and fashionable practice!"
Maybe if SPARK used XML syntax...
Nah, it would just make it popular. To make it sexy one should make it object-oriented...
|
|
|
|