High Integrity Software 238
| High Integrity Software | |
| author | John Barnes |
| pages | 448 |
| publisher | Addison-Wesley |
| rating | 8 |
| reviewer | Jack Ganssle |
| ISBN | 0321136160 |
| summary | The book describes a language that insures programs are inherently correct. |
What is SPARK? It's a language, a subset of Ada that will run on any Ada compiler, with extensions that automated tools can analyze to prove the correctness of programs. As the author says in his Preface, "I would like my programs to work without spending ages debugging the wretched things." SPARK is designed to minimize debugging time (which averages 50% of a project's duration in most cases).
SPARK relies on Ada's idea of "programming by contract," which separates the ability to describe a software interface (the contract) from its implementation (the code). This permits each to be compiled and analyzed separately.
It specifically attempts to insure the program is correct as built, in contrast to modern Agile methods which stress cranking a lot of code fast and then making it work via testing. Though Agility is appealing in some areas, I believe that, especially for safety critical system, focus on careful design and implementation beats a code-centric view hands down.
SPARK mandates adding numerous instrumentation constructs to the code for the sake of analysis. An example from the book:
Procedure Add(X: In Integer);
--#global in out Total;
--#post Total=Total~ + X;
--#pre X > 0;
The procedure definition statement is pure Ada, but the following three statements SPARK-specific tags. The first tells the analysis tool that the only global used is Total, and that it's both an input and output variable. The next tag tells the tool how the procedure will use and modify Total. Finally a precondition is specified for the passed argument X.
Wow! Sounds like a TON of work! Not only do we have to write all of the normal code, we're also constructing an almost parallel pseudo-execution stream for the analysis tool. But isn't this what we do (much more crudely) when building unit tests? In effect we're putting the system specification into the code, in a clear manner that the tool can use to automatically check against the code. What a powerful and interesting idea!
And it's similar to some approaches we already use, like strong typing and function prototyping (though God knows C mandates nothing and encourages any level of software anarchy).
There's no dynamic memory usage in SPARK -- not that malloc() is inherently evil, but because use of those sorts of constructs can't be automatically analyzed. SPARK's philosophy is one of provable correctness. Again -- WOW!
SPARK isn't perfect, of course. It's possible for a code terrorist to cheat the language, defining, for instance, that all globals are used everywhere as in and out parameters. A good program of code inspections would serve as a valuable deterrent to lazy abuse. And it is very wordy; in some cases the excess of instrumentation seems to make the software less readable. Yet SPARK is still concise compared to, say, the specifications document. Where C allows a starkness that makes code incomprehensible, SPARK lies in a domain between absolute computerese and some level of embedded specification.
The book has some flaws: it assumes the reader knows Ada, or can at least stumble through the language. That's not a valid assumption any more. And I'd like to see real-life examples of SPARK's successes, though there's more info on that at www.sparkada.com.
I found myself making hundreds of comments and annotations in the book, underlining powerful points and turning down corners of pages I wanted to reread and think about more deeply.
A great deal of the book covers SPARK's syntax and the use of the automated analysis tools. If you're not planning to actually use the language, your eyes may glaze over in these chapters. But Part 1 of the tome, the first 80 pages which describes the philosophy and fundamentals of the language and the tools, is breathtaking. I'd love to see Mr. Barnes publish just this section as a manifesto of sorts, a document for advocates of great software to rally around. For I fear the real issue facing software development today is a focus on code ueber alles, versus creating provably correct code from the outset.
You can purchase High Integrity Software from bn.com. Slashdot welcomes readers' book reviews -- to see your own review here, carefully read the book review guidelines, then visit the submission page.
References to the story (Score:5, Informative)
Here [praxis-cs.co.uk]is a PDF that contains samble chapters of the book reviewed.
Also from the same site is the following text and links for those of you wanting "real world examples":
"Industrial Experience with SPARK [praxis-cs.co.uk] (PDF 234kb) Dr. Roderick Chapman, Praxis Critical Systems Limted. Presented at ACM SigAda 2000 conference. This paper discusses three large, real-world projects (C130J, SHOLIS and the MULTOS CA) where SPARK has made a contribution to meeting stringent software engineering standards. "
Eurofighter (Score:5, Informative)
SPARK is used heavily in the safety critical software in the Eurofighter amongst other projects. It is a complete pain to type all of the annotation, takes forever to run the tool and it very rarely comes up with any real problems in the code. I would pay good money never to have to go near it again. It was used to meet contractual requirements, not engineering requirements.
One neat trick is to generate a large proportion of the annotation from the output error messages. Sort of defeats using the tool though but since it doesn't find much anyway the time freed up can be used to do some real testing.
Theorem proving languages (Score:2, Informative)
Alloy's cool because you can use it to model code at a very abstract, high level (much like SPARK, it seems), although with Alloy you aren't tied to any specific language. The downside is that since the model isn't embedded in the code it's more useful as a design tool than something which will "guarantee" correctness every time you compile.
Re:question (Score:5, Informative)
SPARK Ada came from Praxis Critical Systems. (http://www.praxis-cs.co.uk/). Go take a look. You can read about how SPARK Ada is used in things like aircraft, and (increasingly) in the automotive industry.
Re:Why not make the tester the compiler? (Score:3, Informative)
> to get both the test and the code that
> passes the test!
This came up on the Extreme Programming list a while back. I think the Java IDE IDEA [jetbrains.com] does something like this, in that you can write a test and it'll generate the source code for the method signatures that you're trying to test. Then you fill in the implementation. *Disclaimer - I haven't used that feature so I don't know how well it works*
One problem with this, though, is that code can pass a test but still be lousy. For example, say you've got a test case for a Stack:So the generator comes up with a Stack implementation - but the first thing it does is allocate a new array of size Integer.MAX_INT to hold the items. The tests pass... but memory usage is ridiculous.
You could go at it by writing a genetic algorithm [rubyforge.org] to evolve code that better fit the requirements... but I'm not sure that'd get you much further.
Fun stuff!
Re:public class interfaces (Score:5, Informative)
Anyhow, DBC is totally distinct from object orientation. In DBC, each component in your software comes with a "contract" that states "if I am called when the _preconditions_ are true, I promise that after I run the _postconditions_ will be true."
The preconditions and postconditions are a group of logical statements, hopefully ones which are useful to your program
Let me give a little example.
function: sqrt( x )
preconditions:
- integer (x)
- positive (x)
postconditions:
- result > 0
- result * result x
Do you see what's happening there? Without knowing
Adding in object orientation support to DBC is a little more complex, but I won't go into that unless asked.
Traditional DBC systems, including Eiffel, couldn't verify your contracts, so most of them would translate the contracts into code, and include that code in the executable; if a contract failed, the code would throw an exception or otherwise fail. SPARK is interesting because it can detect contract failures without running the code; it can also detect when your contracts fail to promise enough.
-Billy
Re:Ok... (Score:4, Informative)
I would have been interested if all this instrumentation had been grafted onto a language like Java, or C++. But to have to switch to Ada just to be able to add in instrumentation that helps in code analysis?
Switching languages is a tiny effort compared to the change required to design your code for static validation. The SPARK people strongly recommend against trying to "switch" to SPARK; if you want the benefits, you have to code with it from the start. It's kind of like taking a 100,000 line C program written by 30 programmers over 10 years and trying to "switch" it to C++ -- it's theoretically possible, but in practice it's easier to start over.
And what they did in Ada would have been impossible in C++. It's significant that SPARK code will run EXACTLY the same on all compliant Ada compilers. No platform dependancies, no ambiguities, no undefined behavior... ALWAYS the same. You simply can't possibly define a subset of C++ which would be able to make those promises. I don't know if it would be possible with Java; since there's no formal specification of Java, probably not.
It's also funny that he WOW's at the idea of no dynamic memory allocation...
I felt that way too
The reason they did it is simple, though -- they wanted to be able to set absolute bounds on when a SPARK program will or will not fail (throw an exception). There's no way to do that with dynamic memory allocation as it's defined in Ada and most other languages.
Yes, that's limiting; no argument. But for some problems, particularly ones solvable by programs managing their own memory, the limitation doesn't matter compared to the benefits -- a SPARK program can execute without any runtime support code.
Why not just use a type safe language?
No such thing -- type safety is an uncomputable problem.
If you meant strongly typed, that's easy; Ada was already strongly typed. SPARK just guerantees that the programs will always run the same, and SPARK's verifier guarantees that the types are chosen and described correctly.
-Billy
Eiffel and Sather (Score:2, Informative)
Re:Eurofighter (Score:1, Informative)
Quite obvious you have never used the tool. We are talking about many hundreds, if not thousands, of lines of annotation for a few tens of lines of code by the time you reach the higher level modules. Hardly zero, quite the opposite. In my experience no defect found by the SPARK tool was not detected via other methods.
People have low expectations of software because they have experienced it. You get what you pay for. Building software to the reliability standards required in safety critical systems is hideously expensive. You paying?, though not somehow.
You are not a pilot. I am an aerospace engineer and I don't worry about the software when I fly. Uncontained engine failures are another matter...
Re:IMHO the only way to go (Score:3, Informative)
Proving non-trivial programs correct is nearly always intractable, if not strictly speaking impossible. We simply don't have the computing power to do it for larger programs, and (IMO) we probably never will.
Re:But what.. (Score:3, Informative)
A search on Google for formal methods [google.com] will give you a lot of stuff. The first site [ox.ac.uk] that comes up is a good starting point.
Note that at some point, one has to hope that what the client wants is what he has described. A tax calculation programme will not be of use if he really wanted a customer relations management system :^)
Re:Just a toy, or what? (Score:2, Informative)
Re:Proving sqrt() correctness? (Score:4, Informative)
i.e. Y, your sqrt, is no more than X when squared, but increase it by 1 and it is more than X. You require X to be non-negative.
Assuming that your implementation implements an initial guess at Y and then repeatedly increments it, you would specify a loop invariant that shows that your guess at Y (say 'Z') is such that (Z+1)*(Z+1) For more information on what's practicable in a customer-specified system, read the peer-reviewed publications...
Disclaimer: SPARK hacker for 6 years
Re:public class interfaces (Score:2, Informative)
or a ot of other languages with data validation written at the begging and ending of each method
Re:But what.. (Score:4, Informative)
In real life that's what usually kills people.
_Safeware_ by Nancy Leveson looked at several software-related disasters. Only one disaster, the Therac radiation machine that fried several patients, was the result of actual bugs (and those bugs were race conditions). The rest consisted of software obediently and disastrously doing exactly what it was supposed to do, like the black lab at #7 in http://www.dorsai.org/~walts/darwin.html.
If you build safety-critical software be sure to have some organized way to flush out what-if questions and hidden assumptions.
Re:Programming by Contract? (Score:3, Informative)
You could, in theory, use to do design by contract, but you'd have to be very careful to put your assertions in the right places, make sure that none of them have side effects, and manually do a few other things that a DbC language automatically takes care of for you. It'd be risky, but it's possible. It becomes MUCH harder when you add object orientation, though; managing inheritance of invariants becomes very difficult.
-Billy