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

public class interfaces

[Anonymous Coward]

Ok, I know nothing about SPARK, so forgive my ignorance. Why is the "contract" paradigm different from standard object oriented languages with public class interfaces?

Re:public class interfaces

[iabervon]

You don't really mean public class interfaces (per se), you mean function prototypes, which are available in C (for example). The difference is really that you can specify arbitrary information about what the function is supposed to do, rather than just a few particular things. E.g., the usual API for mod is something like

int mod(int num, int den)

This lets you add

den != 0

(den = 0)

Then the compiler could automatically write the check for division by 0, and could optimize it out in cases when it can statically prove it is unnecessary.

Of course, it's easy to get excessive in writing the contracts, such that the contracts are no simpler or more informative than the implementation. The trick is to have your contracts specify inportant information about the behavior of the code without going into so much detail that the contract is unclear to the user or not what you intended.

Re:A _review_?

[InternationalCow]

You're right. I still do not know whether or not this book is any good if you're interested in SPARK or Ada and want to learn. Wow. This is not a review but a rave. However, the author obviously knows what he's talking about so I would welcome an actual review on Slashdot.

Re:A _review_?

[Anonymous Coward]

He says it exactly twice. Seems like you ARE one to complain.

Re:Eurofighter

[tcopeland]

> It was used to meet contractual
> requirements, not engineering requirements.

There be dragons.

> One neat trick is to generate a large
> proportion of the annotation from the
> output error messages

That's classic. It makes sense, though - kind of like running a code reformatter rather than running a "code format checker". Every night, the code gets reformatted to meet the style guide... no nagging emails, just silent enforcement.

Re:Eurofighter

[Anonymous Coward]

The people who wrote the contract might have a different opinion. It seems to me I could claim cutting corners on the kind of cement wasn't important and just a contractual obligation not a design consideration. Are you saying that you can get the exact same kind of fault tolerance as a correctly used spark affords, and have the same level of confidence?

Sounds like Resolve

[etcshadow]

This sounds very much like (looks very much like, as well) a project that some of my professors were working on a few years back at Ohio State University, called Resolve C++. I also recall that they were working with another university (can't remember which... maybe U Penn?) on Resolve Ada.

The basic idea was that they added a whole ton of syntactic sugar to C++ (not by structured comments, but by adding a bunch of key words that were #defined into nothing). I'm curious if this is related to that work at all. (At the time I was convinced that it was total crap, but several years of experience have shown me what they were trying to accomplish, if poorly.)

Why not make the tester the compiler?

[192939495969798999]

Whatever the test application is doing to run those tests, why not just convert its output to an EXE/binary and use THAT as the program? Then you only have to write the tests to get both the test and the code that passes the test! That's copyright me, today, by the way.

Software deserves more respect

[bigberk]

Crappy software is all around us (obviously). It may not seem like a huge tragedy that, say, Microsoft Windows has so many security problems but the unfortunate reality is that the entire Western Economy heavily relies upon software that is so fragile that fresh installations become compromised within minutes.

Since so much of what we depend on these days is powered by software, I can't help but feel that industrial software development should be taken under the wing of Engineering. Why, you say? Well, professional fields like medicine, law, and engineering associate a duty to public safety with the job, and the regulatory bodies for the professions ensure that individuals who practice irresponsibly will lose their profesional status.

There is no such accountability for software development. Look at Microsoft Windows, that our banks and governments rely upon! I think such a product would be much higher quality if the coders working on it were professionals and had to adhere to Codes; violating their professional duties would mean severe personal consequences. And the firm itself (Microsoft) would be legally liable if it produced a shoddy, dangerous product!

Re:Programming by Contract?

[pedantic bore]

This is a very simple case, and so it is not surprising that the contract and the code look similar. The proof of the pudding is whether this works for non-trivial specifications and algorithms.

For example, will this work with your favorite sorting algorithm? Presumably all sorting algorithms for sets drawn from a given domain will have the same pre and post conditions, but very different algorithms.

Re:Programming by Contract?

[Anonymous Coward]

Definitely. You can either code the function in the post section, which means it will have the exact same deficiencies as the function, or you code an approximation, in which case it becomes rapidly useless. Everybody remembers their numerical methods, right? You know, all that stuff about propagating error? Just imagine how quickly an approximation of a recursive function would go wrong.

Besides that, it doesn't look like Ada is a functional language, so doesn't it also have side effects? While it's all fine and well to try to prove the program is correct, it's extremely difficult to do when your functions have side effects. It's the side effects that can really screw you up, not the function interface.

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.

Ummmmm...

[randombit]

One thing I note that the review does not mention is the fact that SPARK is, while Turing-complete, not very much fun to program in. Starting with Ada, a pretty B&D langauge to start with, SPARK removes all the remaining pointy bits, including: "the goto statement, aliasing, default parameters for subprograms (i.e. procedures and functions), side-effects in functions, recursion, tasks, user-defined exceptions, exception handlers and generics" (list taken from here, emphasis mine), plus dynamic allocation, which is mentioned in the review.

Basically the only excuse you could possibly have for writing something in SPARK is extremely critical code (ie, if it fails, many people die). Even then I'd be skeptical it would provide much benefit, but at least it would provide some ass-covering ability. :)

For a alternatve view of the practicality of correctness proofs, see chapter 4 of Peter Guttman's thesis. IIRC there was a book review of it on /. a while back (which I didn't read). Even if you did read it, read it again.

"No programming language can save you from yourself."
- Me

Newspeak

[quixoticsycophant]

"Many computer scientists have fallen into the trap of trying to define languages like George Orwell's Newspeak, in which it is impossible to think bad thoughts. What they end up doing is killing the creativity of programming." --Larry Wall

SPARK seems to be an extreme example. Though I've never used it, I venture to guess that in a quixotic effort to avoid all bugs SPARK only buries real bugs underneath a mountain of its own pedantry.

Re:Programming by Contract?

[Flamerule]

SPARK mandates adding numerous instrumentation constructs to the code for the sake of analysis.

This seems rather a waste of time. You either first describe exactly what the code does, then write the code, or you write a simplification of what the code does, then the code.

I'm not an expert on any of this stuff, but allow me to point out the misunderstanding I think you're operating under. Programming by contract isn't concerned with what the code does inside a function, per se. It simply tries to ensure that a function adheres to its contract conditions on expected input/output. Pre/post conditions... you know. So a function, on beginning execution, can expect the program state it is given to obey the precondition properties. In turn, on ending execution, the function must leave the program state as specified by the postcondition.

In the first case, you write the exact same thing twice, in different languages. That sounds like an immense waste of time to me.

No, you don't specify everything the code does.

In the second case, your specification does not cover every aspect, which introduces loopholes, defeating the purpose of the contract.

As I said, the contract isn't a "simplification" of the code. But anyway, you're kind of saying here that this technique doesn't totally prevent all mistakes, so it's worthless. Harsh.

In either case, you get in trouble if there are errors in the contract.

Clearly. I think it's useful to explicitly detail the contract, however. It forces you to think about something you might not have considered otherwise.

Re:Programming by Contract?

[William Tanksley]

This seems rather a waste of time. You either first describe exactly what the code does, then write the code, or you write a simplification of what the code does, then the code.

It's not a waste of time to describe what a function does. It's essential to keep "what" a function does distinct from "how" it does it. That's the whole point of interface versus implementation.

Consider a function with the following contract:

function: sqrt( x )
preconditions:
- integer (x)
- positive (x)
postconditions:
- result > 0
- result * result <= x
- (result+1) * (result+1) > x

Now, can you see how that's useful? And do you see that this tells you something _completely_ different than what you'd know if you read the actual source code for that function (perhaps an implementation of Newton's method)?

In the second case, your specification does not cover every aspect, which introduces loopholes, defeating the purpose of the contract.

That's what SPARK's automatic verifier is for -- to prove that there are no loopholes.

-Billy

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.

Re:Ok...

[yermoungder]

Or the companies who want to save money by not having to do so many man-hour hungry unit tests or post-release bug fixes... LockheadMartin have presented project using the highest level of DO-178B as cost 1/4 of (yes, "of" not "off") of similar non-Level A projects. There were many reasons for that, of course, but I'm sure that SPARK and similar tools played their part.

Re:Eurofighter

[Theodrake]

The real nightmare comes when the specification changes. So instead of just changing your code. You have to also change this psuedo code, oops contract. Plus I'm guessing you still have end-to-end tests, all of which get rewritten. All this may eliminate are the unit tests, which for me were the easiest to code and in many cases a visual inspection would do. Now you have to maintain this contract and your code. Seems like more trouble then it is worth.

Re:Eurofighter

[daksis]

This type of unprofessional crap is the reason people have such low expectations of software.

I think people have such low expectations of software because for the most part, software doesn't meet their expectations, and the expectations people have of software are often unrealistic. Software is like everything else - built with the trade off of cost versus utility.

Knuth said it best...

[KurtP]

"Beware of bugs in the above code. I have only proven it correct, not tested it."

Re:question

[AdaDaddy]

Actually, yes.
These people have successfully used SPARK on many projects. They also provide the tools making the SPARK approach feasible.

The SPARK approach causes discomfort for many software developers because its approach diverges from that of the various agile development processes.

If you read the book you will discover that the author's claims are supported by real data from real projects.

The SPARK approach is extremely formal. It has frequently been used on the safety critical portions of larger systems.

Remember that SPARK is intended for use primarily on real time safety critical systems. Such systems control energy sources. Failure of such systems carries a high probability of injury or death to people.

Re:Eurofighter

[Doctor Faustus]

They discovered the delivered Ada projects had a defect rate 1/10 that...

Lockheed has done some really cool things over the years, but I just don't buy this. If they could positively identify the defect rates of these programs, they could just get rid of the bugs in the first place, in the SPARK projects *and* in the C projects. It's more likely they've got some sort of automated checked that catches exactly the same sort of thing that SPARK itself does.

Really, it looks like the SPARK program basically consists of the same program written twice, with the two versions compared for mismatches. This may be a useful tool, but it will only catch low-level errors. It would be more useful to write the program twice with different designs (and different teams), run them both, and report on when they came out with different answers.

Re:Check out D

[krischik]

Yes D is interesting. Only, like Eiffel, it concentrates only on procedural contracts and lacks type contract.

SPARC, being based on Ada does have type contracts:

type Day_Of_Month is range 1 ..31;

BTW: The example won't work. It does not take into account the fact that math.sqrt(x) only calculates an approximation - which is truncated to long. Correct examples have been posted before - by SPARC hackers.

It is not a good sign that the D developers made such an obvious mistake.

With Regards

Martin