Slashdot Mirror
High Integrity Software
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.
The very first page quotes C.A.R Hoare's famous and profound statement
Not to be confused with C.A.M. Hoare's famous and profound statement: "Want to see my boobies?"
Or do they sit around thinking of methodologies to write books about?
Those who can, do, those who can't, teach?
Seriously, I'm not one to complain, but this isn't a review; it's a guy saying "WOW" repeatedly.
In General, if you want info, RTFA. However for those of you who just want some links to check things out quickly:
Hereis 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 (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. "
The Army reading list
The Army reading list
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.
I agree that this is actually the problem. As I understand it, the high-reliability people have more-or-less solved the problem of enduring the code follows the specification (though at a cost that woul deter for less critical applications). But all this does is push the problem one level higher.
In the early days of compilers, one of the claims for compilers was that they would make mistakes impossible. Of course, all they did was make one class of stupid assembler mistakes impossible.
The reason for the verbosity of COBOL is the idea that it would be so like business English that management could read it, if not write it.
Eash time we get a tool that removes one class of mistakes, all we do is increase the systen m complexity until the level of mistakes returns to the previous level of near-unacceptability. "Snafu" is the normal state of the programmers universe - it is only a case of how large a system you build before it all fouls up.
Having said that, Design By Contract is a good idea. While accepting that it is always going to turn to ratshit, you might as well do so at a higher level as a lower one. However, it isn't new: look at Eiffel and Aspect Java for instance.
Consciousness is an illusion caused by an excess of self consciousness.
The best available modern system for formal verification is the Extended Static Checking system for Java developed at DEC SRL. This was developed at DEC before HP shut down that research operation. It's still available as a free download.
What all this machinery does is put teeth into "design by contract". With systems like this, you can tell if a function implements its contract, and you can tell if a caller complies with the contract of each thing they call. Before running the program.
Developing in this mode means spending forever getting rid of the static analysis errors. Then, the program usually just runs. That's exactly what you want for embedded systems. But it's painful for low-grade programming like web site development, where "cosmetic errors" are tolerable and time-to-market matters more than correctness.