Slashdot Mirror

Jack Ganssle writes "High Integrity Software: the title alone got me interested in this book by John Barnes. Subtitled "The SPARK Approach to Safety and Security," the book is a description of the SPARK programming language's syntax and rationale. The very first page quotes C.A.R Hoare's famous and profound statement:'There are two ways of constructing a software design. One way is to make it so simple that there are obviously no deficiencies. And the other way is to make it so complicated that there are no obvious deficiencies.' This meme has always rung true, and is one measure I use when looking at the quality of code. It's the basis of the SPARK philosophy." Read on for more of Ganssle's review of the book, and some more on the SPARK language. 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.

Embedded Geek writes "While digging around Jack Ganssle's site, I came across an amusing prank from days gone by. In 1972 Signetics recognized April Fools day by printing a full color datasheet (scanned sheet 1 and sheet 2 here) for a Write-Only Memory (which accepts data but never reads it back), a considerable effort when documents were made via literal "cut and paste". Packed with jokes both obvious (a graph of "number of pins left versus number of insertions") and subtle ("Vdd = 0V +/- 2%") it's worth a chuckle."

Embedded Geek writes "While digging around Jack Ganssle's site, I came across an amusing prank from days gone by. In 1972 Signetics recognized April Fools day by printing a full color datasheet (scanned sheet 1 and sheet 2 here) for a Write-Only Memory (which accepts data but never reads it back), a considerable effort when documents were made via literal "cut and paste". Packed with jokes both obvious (a graph of "number of pins left versus number of insertions") and subtle ("Vdd = 0V +/- 2%") it's worth a chuckle."

Embedded Geek writes "While digging around Jack Ganssle's site, I came across an amusing prank from days gone by. In 1972 Signetics recognized April Fools day by printing a full color datasheet (scanned sheet 1 and sheet 2 here) for a Write-Only Memory (which accepts data but never reads it back), a considerable effort when documents were made via literal "cut and paste". Packed with jokes both obvious (a graph of "number of pins left versus number of insertions") and subtle ("Vdd = 0V +/- 2%") it's worth a chuckle."

Embedded Geek writes "Jack Ganssle has posted a column at embedded.com pondering whether Red Hat and other open source companies serving the embedded community are due a shakeout similar to the dot com collapse. He cites Red Hat's March cuts in their embedded division and their losses of $80M to $140M a year. He admits, though, that because the embedded market is smaller and many companies are privately held it is difficult to get a pulse on what's going on behind closed doors. "

Embedded Geek asks: "There's an interesting opinion piece at Embedded Systems Magazine about [embedded] programming being a dead end job. The author cites burnout ('Pushing ones and zeroes around doesn't sound like a lot of work, but getting each and every one of a hundred million perfect is tremendously difficult.'), prestige, and skill obsolescence as big reasons for programmers to quit or to go 'over to the dark side' and join management or marketing positions. While the piece primarily addresses embedded programmers, the issue is rising for IT workers and other tech workers. When the age issue is combined with the export of jobs offshore, it makes me nervous just to be pushing 35..." Even though the market is going thru a rough patch, and the number of detrimental aspects to programming are increasing (ageism and so forth), I still do not feel that programming is a dead end job. Computers are going nowhere folks, and as long as they are around, programmers will be necessary. People who are in this career for the money or the prestige may not like it after a while, but the people who are in this for something else will tolerate quite a bit before deciding to opt out. The simple measure here: "as long as you love doing it, you'll keep doing it." Isn't this true for any career?