High Integrity Software

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.

Comments

hmmm

[Anonymous Coward]

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?"

question

[Anonymous Coward]

Do these authors actually employ the mentioned practices with any success on a daily basis?

Or do they sit around thinking of methodologies to write books about?

Those who can, do, those who can't, teach?

Re:question

[deepchasm]

Yes, they do.

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.

A _review_?

[Caine]

Seriously, I'm not one to complain, but this isn't a review; it's a guy saying "WOW" repeatedly.

heheh

[grub]

"High Integrity Software"

SCO should adopt that as their motto. :)

But what..

[Anonymous Coward]

..if the contract itself is wrong?

Re:But what..

[AlecC]

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.

Re:But what..

[bcrowell]

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).
Yeah, the article's statement, "The book describes a language that insures programs are inherently correct," is really misleading. Very few real-world programs have ever been proved correct, and the reasons for that are language-independent. Very few real-world problems even lend themselves to a precise mathematical statement of what "correct" would mean. What would it mean for mozilla to be "correct?" Even if your code is running a nuclear reactor, the code can only be as "correct" as the accuracy of the assumptions and engineering data that went into the spec.

In many real-life projects, the nastiest bugs come from requirements that change after the first version has already been written. Proving that a program correctly implements a spec doesn't help if the spec changes.

What horseshit

[Anonymous Coward]

The book describes a language that insures programs are inherently correct.

Now, is there a language to ensure that your boss asks you to program the right thing?

References to the story

[SamiousHaze]

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. "

"no obvious deficiencies"

[tcopeland]

Cue Hitchhiker's Guide on the Sirius Cybernetics Corporation:

In other words - and this is the rock solid principle on which the whole of the Corporation's Galaxy-wide success is founded - their fundamental design flaws are completely hidden by their superficial design flaws.

Wrong order - first test, than code

[tcopeland]

modern Agile methods which stress cranking a lot of code fast and then making it work via testing.

No, instead, they stress writing a test, then writing code to make the test pass. Big difference there.

Eurofighter

[Anonymous Coward]

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.

Re:Eurofighter

[SheldonYoung]

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.

This type of unprofessional crap is the reason people have such low expectations of software. You didn't want to use the tool because it was a "pain to type"?! If the length of time it takes you to type your code is a bottleneck then you're not doing enough thinking before you type. The extar effort requierd to type more verbose code is close to zero. You're coming across like an aeronatical engineer would if they tightened a critical bolt to only 90% of the required torque because it was less effort.

By saying very rarely comes up with any real problems" means it found some, and those problems may have been easily been overlooked by other types of testing. And what are problems wouldn't be "real" in saefty critical code?! Yes, there are other tools besides SPARK that could have been used but the principles should have been the same.

Don't ever forget you're talking about a serious piece of hardware and there's a human being sitting in the pointy end. If I was a pilot of something that had a bug in it's safety critical software because of your lack of pride I would kick your ass.

Re:Eurofighter

[yermoungder]

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.

Free download of a similar system for Java

[Animats]

We did this twenty years ago, for a dialect of Pascal. See Practical Program Verification. Back then, you could do it, but it was rather slow. Today, with machines thousands of times faster than the VAX 11/780 we used back then, it's much more feasible. But you need a language suitable for verification. C and C++ are hopeless - the semantics of the language are ambiguous. (Casts, pointer arithmetic, and "void *", make the typing system unreliable.) The Pascal/Modula/Ada family are suitable, with modifications and limitations. Eiffel and Sather do well, but few use them. Java, though, is both verifiable and widely used.

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.

Re:public class interfaces

[happyfrogcow]

Ok, I know nothing about SPARK, so forgive my ignorance.

me neither, me too...

my understanding is that the contract has hard requirements on specific input and specific output for results. all of which are defined prior to executing that code. something like "we require an incomming integer with a value that is between zero and fifteen. we gaurantee that an integer value will be returned that is either zero or one"

with a public class interface you can write a peice of code that does this, but it won't gaurantee anything. it's up to the developer to exhaustively test all situations and make sure that it happens. in a contract based language, i would guess that the program either won't compile, won't run, or will fail in obvious ways in the development stage if the requirements are not met. i'm not sure how they handle requirements that aren't met.

Re:public class interfaces

[William Tanksley]

Design By Contract was not invented by SPARK; the name was popularised by Bertrand Meyer, who added it to his "Eiffel" language.

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 /anything/ about how sqrt is computed, you can use it in powerful ways. Preconditions and postconditions can't always be as informative as the ones above are (the ones above define everything about the integer sqrt function), but they can give useful information.

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

using ada is enough

[acomj]

I've been using ada for a little while now. Its actually a good language, with many features that provided self checking code. SPARK seems a bit excessive.

For example ada already had constrained types (x :integer range 0..15) . If x goes above 15 or under 0 during runtime you get a constraint error.

The ada compiler checks alot of things during compile time that I've never seen before.

Re:Proving sqrt() correctness?

[Suslik]

To prove the correctness of an (Integer) square root routine you would specify something like:

procedure Sqrt(X : in Integer; Y : out Integer)
--# derives Y from X;
--# pre X >= 0;
--# post (Y*Y <= X) and ((Y+1)*(Y+1) > X);

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