Slashdot Mirror

For Ada, I like WikiBooks: http://en.wikibooks.org/wiki/Ada

Also useful
http://www.adaic.org/
http://www.sigada.org/
http://www.adacore.com/
http://www.sparkada.com/
https://libre.adacore.com/ (free GPL'd Ada 2005 compiler)

For high-integrity stuff, we use SPARK (http://www.sparkada.com/) - a design-by-contract subset of Ada95 that is entirely designed-from-scratch for verification purposes.
The verification system implements Hoare-logic and is supported by a theorem prover. Buffer Overflow is only one of many basic correctness properties that can be verified. Properties that can be verified are only limited to what can be expressed as an assertion in first-order logic.
SPARK is a small language (compared to C++ or Java...) but the depth and soundness of verification is unmatched by anything like FindBugs, SPLINT, ESC/Java or any of the other tools for the "popular" languages.
(If you don't know or care what soundness is in the context of static analysis, then you've probably missed the point of this post... :-) )
- Rod Chapman, Praxis

If you want software that does not crash during operation, you have to remove subroutine recursion and dynamic memory allocation so that you can guarantee an upper bound on the stack and pool usage at any time. If you're using multiple processes then you need some way of preventing deadlock and livelock. Whether you use C, C++ or Ada, you have to enforce these conventions in some way.
See the SPARK Ada site for an example of how you do this. But fundamentally, to write software that is crash free you cannot take an off-the-shelf language and off-the-shelf OS and simply hope for the best.

Agreed. Correctness is not something programmers are interested in, it seems. Why else are people still using languages that cannot assure that you do not compare metres and feet? Why are people still using languages that cannot assure you don't have buffer overflows?

Testing doesn't help, because your tests can have bugs too and are probably incomplete. It's gives a lot of peace to the mind if you hit the compile button in Eiffel and it compiles successfully.

That does not imply Eiffel is the end of the road. I would like to see something like Spark being available for Eiffel.

There is no substitute for a competent programmer if you wish to write secure code. There is equally no substitute for a well-designed language, nor for effective tools to support programming in that language.

The safety-critical software community has been tackling these very issues for the past fifteen years or more; the security community is sometimes guilty of re-inventing the safe software wheel, and doing it badly. Safety engineers have already come up with the MISRA C subset (here) and tools to enforce it, but the general conclusion appears to be that C (and C++) are inherently unsafe languages and there's only so much you can do to patch over the problems.

If programmers are serious about wanting to write correct code, they are going to have to check their egos at the door and use tools that tell them where they are going wrong as early as possible. My personal suggestion is the SPARK Ada subset and associated toolset, but then I'm biased. :-)

Take a little longer over your code. Get it right first time. Write your tests before you write the code. Use static analysis tools that are proven to pick up real errors. But enjoy what you're doing, because the best programmer in the world is still going to produce crap code if he's bored...

Adrian

I believe it supports full formal proof of correspondence between an implementation and a specification.

SPARK Ada this would never have happend.

Go static analysis!

Re: The Ada catastrophe:

It is a pity that the catastrophe of ADA brought down the idea of dimensional analysis with it. Of course Hoare's Turing award lecture (please don't use this for anything safety critical the compilers are certain to be full of bugs) gave a salutary warning on unbounded complexity.

Gradually these objectives have been sacrificed in favour of power, supposedly achieved by a plethora of features and notational conventions, many of them unncessary and some of them, like exception handling, even dangerous.

But I come not to bury Hoare, but to praise him (Hell, he invented the case statement..):

It is not too late! I believe that by careful pruning of the Ada language, it is still possible to select a very powerful subset that would be reliable and efficient in implementation and safe and economic to use

All Software Engineers should have a look at Correctness by Construction: Better can also be Cheaper from Crosstalk the Journal of Defence Software Engineering. It contrasts the usual C approach with one using a really tight but powerful subset (SPARK) of an already pretty tight language, Ada

* SPARK code was found to have only 10 percent of the residual errors of full Ada; Ada was found to have only 10 percent of the residual errors of code written in C. This is an interesting counter to those who maintain that choice of programming language does not matter, and that critical code can be written correctly in any language : The claim may be true in principle but clearly is not commonly achieved in practice.

This isn't just an anecdote: there are documented facts. The results (for the problem domain of aircraft avionics and large systems) may not be applicable to the normal b2b and gamezware - but then again, they might. Have a look at the stuff in bold later in this post.

It's not a magic bullet : from the same article:

In December 1999 CrossTalk, David Cook provided a well-reasoned historical analysis of programming language development and considered the role languages play in the software development process. The article was valuable because it showed that programming language developments are not sufficient to ensure success; however, it would be dangerous to conclude from this that they are not necessary for success. Cook rightly identifies other issues such as requirements capture, specifications, and verification and validation (V&V) that need to be addressed.

But the real kicker, one that should cause everyone to sit up and take notice, is this:

• Code quality improved by a factor of 10 over industry norms for DO-178B Level A software.
• Productivity improved by a factor of four over previous comparable programs.
• Development costs were half that typical for non safety-critical code
• With re-use and process maturity, there was a further productivity improvement of four on the C27J airlifter program.

One more thing: the SPARK and similar RAVENSCAR ( pdf, HTML version here) subsets of Ada-95 are just that : (proper)subsets that just omit certain language constructs. Write to the profile, and the code is compileable by any Ada-95 compiler, like the downloadable Free GNU version GNAT 3.14p (though commercial users might want the latest-and-greatest non-free version 3.15a. And the ORK (Open Ravenscar Kernel) is, as the name implies, an Open Source Kernel for reliable real-time embedded systems.

Better, Cheaper, Faster, Open-Source with Free-as-in-Beer downloadable compilers. IMHO worth at least investigating, even if you decide Microsoft's latest language-du-jour is more appropriate for your situation. YMMV, and COBOL, C++, Assembler, C#, Java or even VB might be better in your case. But worth a look.

All Software Engineers should have a look at Correctness by Construction: Better can also be Cheaper from Crosstalk the Journal of Defence Software Engineering. It contrasts the usual C approach with one using a really tight but powerful subset (SPARK) of an already pretty tight language, Ada

* SPARK code was found to have only 10 percent of the residual errors of full Ada; Ada was found to have only 10 percent of the residual errors of code written in C. This is an interesting counter to those who maintain that choice of programming language does not matter, and that critical code can be written correctly in any language : The claim may be true in principle but clearly is not commonly achieved in practice.

This isn't just an anecdote: there are documented facts. The results (for the problem domain of aircraft avionics and large systems) may not be applicable to the normal b2b and gamezware - but then again, they might. Have a look at the stuff in bold later in this post.

It's not a magic bullet : from the same article:

In December 1999 CrossTalk, David Cook provided a well-reasoned historical analysis of programming language development and considered the role languages play in the software development process. The article was valuable because it showed that programming language developments are not sufficient to ensure success; however, it would be dangerous to conclude from this that they are not necessary for success. Cook rightly identifies other issues such as requirements capture, specifications, and verification and validation (V&V) that need to be addressed.

But the real kicker, one that should cause everyone to sit up and take notice, is this:

• Code quality improved by a factor of 10 over industry norms for DO-178B Level A software.
• Productivity improved by a factor of four over previous comparable programs.
• Development costs were half that typical for non safety-critical code
• With re-use and process maturity, there was a further productivity improvement of four on the C27J airlifter program.

One more thing: the SPARK and similar RAVENSCAR ( pdf, HTML version here) subsets of Ada-95 are just that : (proper)subsets that just omit certain language constructs. Write to the profile, and the code is compileable by any Ada-95 compiler, like the downloadable Free GNU version GNAT 3.14p (though commercial users might want the latest-and-greatest non-free version 3.15a. And the ORK (Open Ravenscar Kernel) is, as the name implies, an Open Source Kernel for reliable real-time embedded systems.

Better, Cheaper, Faster, Open-Source with Free-as-in-Beer downloadable compilers. IMHO worth at least investigating, even if you decide Microsoft's latest language-du-jour is more appropriate for your situation. YMMV, and COBOL, C++, Assembler, C#, Java or even VB might be better in your case. But worth a look.

I think of this whenever I read about computers used in medical, transportation, or other areas where malfunctioning software could put lives at risk.I don't believe that the "software culture" has changed significantly in this respect since then.