Beta
×

Welcome to the Slashdot Beta site -- learn more here. Use the link in the footer or click here to return to the Classic version of Slashdot.

Thank you!

Before you choose to head back to the Classic look of the site, we'd appreciate it if you share your thoughts on the Beta; your feedback is what drives our ongoing development.

Beta is different and we value you taking the time to try it out. Please take a look at the changes we've made in Beta and  learn more about it. Thanks for reading, and for making the site better!

High Integrity Software

timothy posted more than 10 years ago | from the tensegrity dept.

Programming 238

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.

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.

Sorry! There are no comments related to the filter you selected.

I for one. (-1, Offtopic)

Anonymous Coward | more than 10 years ago | (#9197475)

code with my tongue. I do. Don't laugh at me.

Re:I for one. (-1, Offtopic)

Anonymous Coward | more than 10 years ago | (#9197525)

..using a gameboy advance I guess?

hmmm (5, Funny)

Anonymous Coward | more than 10 years ago | (#9197478)

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

Re:hmmm (-1, Offtopic)

Anonymous Coward | more than 10 years ago | (#9197664)


Israel's genocidal policies continue when today they kill 10 children and teens. [cjad.com]

Way to go, Israel, slaughter children!

What does "on the spoke" mean? (-1)

Anonymous Coward | more than 10 years ago | (#9197489)

What does "on the spoke" mean?

Please cite sources.

Is it really in a Halo 2 trailer?

Thanks.

Re:What does "on the spoke" mean? (-1, Offtopic)

Anonymous Coward | more than 10 years ago | (#9197507)

GO GET EM TIGER

Re:What does "on the spoke" mean? (0, Offtopic)

Mz6 (741941) | more than 10 years ago | (#9197518)

Perhaps... here? [thespoke.net]

question (5, Insightful)

Anonymous Coward | more than 10 years ago | (#9197491)

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 (0)

Anonymous Coward | more than 10 years ago | (#9197592)

There should be a new mod option: "+0.5, Obvious but Quite Valid. Original Post Needs Work."

This is by no means "insightful".

Re:question (1)

kunudo (773239) | more than 10 years ago | (#9197660)

There is, just leave it at 1.

Re:question (1)

Giant Panda (779279) | more than 10 years ago | (#9197607)

Know what you are doing and do a lot of bug testing. There is no other realistic way.

Re:question (3, Insightful)

DrEldarion (114072) | more than 10 years ago | (#9197676)

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

Those who can't teach, teach theory.

Re:question (0)

Anonymous Coward | more than 10 years ago | (#9197846)

:gb2coupons:

Re:question - Answer (1)

mykepredko (40154) | more than 10 years ago | (#9198227)

I thought the correct quote was:

Those who can, do. Those who can't, teach.

Those who can't teach, teach gym.

(At least according to Woody Allen).

myke

Re:question (4, Informative)

deepchasm (522082) | more than 10 years ago | (#9197732)

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.

Re:Reminds me of the real estate guys (1)

symbolic (11752) | more than 10 years ago | (#9197733)

...who endlessly pitch, "Come to my free seminar and my methods well make you a millionaire!" Well, you'd think that if the methods were so flawless, they'd have a lot better things to do with their time than standing in front of an audience blabbing about it.

Re:question (2, Funny)

Anonymous Coward | more than 10 years ago | (#9197792)

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

Yes. And I regularly see job adverts specifying SPARK.

Re:question (0)

Anonymous Coward | more than 10 years ago | (#9198083)

Search on Jobserve


Ada, 26 Matching Jobs


Ada and SPARK, No jobs were found to match your search


Nuff said....

Re:question (0)

Anonymous Coward | more than 10 years ago | (#9197836)

Simple answer. No.

Have a look at the papers, you will see it's end user companies using the tool for real. Been there, done that, got out.

A _review_? (5, Insightful)

Caine (784) | more than 10 years ago | (#9197499)

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

Re:A _review_? (3, Interesting)

InternationalCow (681980) | more than 10 years ago | (#9197527)

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_? (0)

Anonymous Coward | more than 10 years ago | (#9197549)

If you want to learn Ada it's certainly the wrong book since, according to this rave/review, it assumes knowledge of Ada already.

Re:A _review_? (2, Interesting)

Anonymous Coward | more than 10 years ago | (#9197547)

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

Re:A _review_? (-1, Redundant)

digital bath (650895) | more than 10 years ago | (#9197567)

Wow, you're right! Wow!

Re:A _review_? (1, Funny)

Anonymous Coward | more than 10 years ago | (#9197574)

And even worse, he got a T-shirt for doing so!

heheh (4, Funny)

grub (11606) | more than 10 years ago | (#9197501)


"High Integrity Software"

SCO should adopt that as their motto. :)

OMG ROFFLES! (-1)

Anonymous Coward | more than 10 years ago | (#9197524)

Way to bring teh funnay.

Re:OMG ROFFLES! (-1, Flamebait)

Anonymous Coward | more than 10 years ago | (#9197694)

Can I interest you in some Grade A prime penis?

Re:heheh (-1, Redundant)

Anonymous Coward | more than 10 years ago | (#9197717)

That would be funny as hell.

But what.. (4, Insightful)

Anonymous Coward | more than 10 years ago | (#9197506)

..if the contract itself is wrong?

Re:But what.. (2, Insightful)

happyfrogcow (708359) | more than 10 years ago | (#9197619)

that's not the implementors primary concern, really. but if you have a design to begin with, atleast you can backtrack and see why the contract is wrong. change it, and implement the right contract.

Re:But what.. (5, Insightful)

AlecC (512609) | more than 10 years ago | (#9197718)

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.. (4, Insightful)

bcrowell (177657) | more than 10 years ago | (#9197807)

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.

Re:But what.. (3, Insightful)

Waffle Iron (339739) | more than 10 years ago | (#9198305)

..if the contract itself is wrong?

That's the beauty of this system. You can close out the issue in your bug tracking database anyway:

"CLOSED: Not a bug; behavior as designed."

Car Whores? (2, Funny)

SirChris (676927) | more than 10 years ago | (#9197511)

I thought car whores are the girl who pose for all the car magazines. Or the ones that sleep with the guy with the coolest car.

Re:Car Whores? (0, Offtopic)

happyfrogcow (708359) | more than 10 years ago | (#9197639)

I thought car whores are the girl who pose for all the car magazines. Or the ones that sleep with the guy with the coolest car.

i ride the subway, who do i get to sleep with? (eeewwwwwww, i don't want to know)

public class interfaces (2, Interesting)

Anonymous Coward | more than 10 years ago | (#9197516)

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 (4, Insightful)

happyfrogcow (708359) | more than 10 years ago | (#9197769)

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 (4, Informative)

William Tanksley (1752) | more than 10 years ago | (#9197881)

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

Re:public class interfaces (1)

William Tanksley (1752) | more than 10 years ago | (#9198094)

Ugh. HTML zapped my pre and post conditions. Here they are...
function: sqrt( x )
preconditions:
- integer (x)
- positive (x)
postconditions:
- result > 0
- result * result <= x
- (result+1) * (result+1) > x
-Billy

Proving sqrt() correctness? (1)

GGardner (97375) | more than 10 years ago | (#9198357)

And how, exactly, does a static compiler prove that a certain code sequence correctly computes a square root?

What horseshit (4, Insightful)

Anonymous Coward | more than 10 years ago | (#9197522)

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?

Re:What horseshit (1)

grasshoppa (657393) | more than 10 years ago | (#9197589)

Why yes, I do speak blackmail-ese. >:)

Never underestimate a BOFH.

Re:What horseshit (-1, Redundant)

Anonymous Coward | more than 10 years ago | (#9197796)

wow this was at -1 flamebait already!

References to the story (5, Informative)

SamiousHaze (212418) | more than 10 years ago | (#9197546)

In General, if you want info, RTFA. However for those of you who just want some links to check things out quickly:

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

"no obvious deficiencies" (5, Funny)

tcopeland (32225) | more than 10 years ago | (#9197552)

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.

Not so impressive (0)

Anonymous Coward | more than 10 years ago | (#9197562)

Abstracts, implements, etc. OOP langs seem to have this interface with later implementation covered. And in the java and .Net worlds, compilers can figure out much of the crap the SPARK requires that I add manually to get the same info.

Re:Not so impressive (1, Insightful)

Anonymous Coward | more than 10 years ago | (#9197688)

It's not so much that they can figure them out as it is they don't care to.

Well, that put Microsoft in it's place (1, Funny)

Anonymous Coward | more than 10 years ago | (#9197576)

Let's see: massively complex, but with obvious deficiencies.

23rd post (1)

ohsnap (775907) | more than 10 years ago | (#9197577)

Sup now, playas? Brush ya shouldas off.

Believe it or not, (-1, Offtopic)

Anonymous Coward | more than 10 years ago | (#9197653)

but

YOU FUCKING FAILED IT!

inf0ormativ(e dickdick (-1, Troll)

Anonymous Coward | more than 10 years ago | (#9197596)

as the p8emiere [goat.cx]

Can you have high-integrity without… (0)

Anonymous Coward | more than 10 years ago | (#9197600)

...ANY memory management?

Wrong order - first test, than code (5, Insightful)

tcopeland (32225) | more than 10 years ago | (#9197612)

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 (5, Informative)

Anonymous Coward | more than 10 years ago | (#9197617)

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 (3, Interesting)

tcopeland (32225) | more than 10 years ago | (#9197761)

> 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 (2, Interesting)

Anonymous Coward | more than 10 years ago | (#9197764)

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?

Re:Eurofighter (1)

RAMMS+EIN (578166) | more than 10 years ago | (#9198021)

It's just that the contracts don't add much value, compared to what they cost.

In order to really ensure that the code does the right thing, the contract has to be about as detailed as the code itself. This means that you end up writing the same thing twice, with possibilities for errors in both copies.

If you relax the contract to only partially describe what needs to happen, you create opportunities for bugs to go undetected, and lose the certainty the contracts were meant to provide.

Re:Eurofighter (4, Insightful)

SheldonYoung (25077) | more than 10 years ago | (#9198062)

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 (1, Informative)

Anonymous Coward | more than 10 years ago | (#9198283)

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

VLISP sounds much more interesting (1)

fuzzy12345 (745891) | more than 10 years ago | (#9197621)

Great, just program in a really wordy subset of Ada, with NO dynamic memory allocation, and your program will be provably... ugly.

Why not use a language that's smart enough to prove code written in a useful language, not just a toy?

This would make for a great fiction book (0, Offtopic)

FerretFrottage (714136) | more than 10 years ago | (#9197635)

"High Integrity Software, High Integrity Companies"

Re:This would make for a great fiction book (0, Troll)

Khakionion (544166) | more than 10 years ago | (#9197675)

I, for one, welcome our new High Integrity Overlords.

Peer Review Request (0)

Anonymous Coward | more than 10 years ago | (#9197651)

I have this program:

sub crazy_prog
begin
while 10 do
writeln "Hello world!";
end;

How can I ensure that this cannot be exploited?

Thank you in advance.

Re:Peer Review Request (0)

Anonymous Coward | more than 10 years ago | (#9197695)


Re-write it in VisualBASIC.

Pay loads of money to MSDN. (MS' Developers Network)

Take your MCSE "exams"

Just tell the end user it works and show your credentials. Most idiots in suits fall for that.

Re:Peer Review Request (0)

Anonymous Coward | more than 10 years ago | (#9197716)

well since it won't compile in any known language, you're safe.

Re:Peer Review Request (0)

Anonymous Coward | more than 10 years ago | (#9197734)

Whew, that's what I needed to hear. I'm sure my manager will be happy to hear that the evil Romanian hackers can't compromise our FoxPro server cluster.

Thank you, I'll add your feedback to the minutes of our developer meeting.

Re:Peer Review Request (0)

Anonymous Coward | more than 10 years ago | (#9197757)

Hm, looks kinda like Pascal to me. But it's been a while so I could be wrong.

Ok... (2)

dioscaido (541037) | more than 10 years ago | (#9197656)

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? It's also funny that he WOW's at the idea of no dynamic memory allocation... Why not just use a type safe language?

Re:Ok... (3, Informative)

William Tanksley (1752) | more than 10 years ago | (#9198037)

Two statements there.

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 :-). Odd.

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

Theorem proving languages (2, Informative)

Believe (124651) | more than 10 years ago | (#9197668)

This sounds a bit like Alloy [mit.edu] . Alloy is both a code modelling language (like UML), but structured in such a way that the model can be analysed automatically using SAT solvers (yeah, I didn't know what those were at first either. Here's a site [princeton.edu] with some good info on them).

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:Theorem proving languages (2, Insightful)

killjoe (766577) | more than 10 years ago | (#9198101)

It also sounds exactly like Eiffel.

This industried ability to continually re-invent the wheel never ceases to amaze me.

Let's go back to lisp and smalltalk every frikken language since then is just a rewrite of one or the other anyway.

HIS and HERS (0)

Anonymous Coward | more than 10 years ago | (#9197670)

HIS: High Integrity Software

HERS: Highly Erratic Random Software

SPARC suXors (-1, Flamebait)

Anonymous Coward | more than 10 years ago | (#9197671)

Get a real processor, Sun worshippers!

Programming by Contract? (3, Insightful)

RAMMS+EIN (578166) | more than 10 years ago | (#9197687)


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;


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.

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

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

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

Re:Programming by Contract? (2, Interesting)

pedantic bore (740196) | more than 10 years ago | (#9197816)

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? (1, Interesting)

Anonymous Coward | more than 10 years ago | (#9197820)

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.

Re:Programming by Contract? (3, Interesting)

Flamerule (467257) | more than 10 years ago | (#9198088)

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? (1)

RAMMS+EIN (578166) | more than 10 years ago | (#9198347)

``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.''

And that's exactly where the loopholes are. In functional programming, all there is to a function is what goes in and what comes out. However, I SPARK being a subset of ADA, I think we can safely assume there will be lots of side effects, and reliance on side effects. This makes specifying only pre- and postconditions not enough.

``But anyway, you're kind of saying here that this technique doesn't totally prevent all mistakes, so it's worthless. Harsh.''

That is indeed quite harsh, but consider this:

In most cases, there will be nothing wrong with the code once the syntax errors (the vast majority of mistakes I make are typos and omissions) are eliminated. For those cases, the contracts have been a waste of time.

In those cases where the code does contain flaws, the contracts won't always catch them.

So, by using contracts, you spend a lot more time, but there is no guarantee that your errors will be found. This sways my opinion against programming by contract. I think the time spent writing and debugging contracts is better spent auditing code.

Re:Programming by Contract? (3, Interesting)

William Tanksley (1752) | more than 10 years ago | (#9198129)

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

Another ADA proselytizer (-1, Flamebait)

Anonymous Coward | more than 10 years ago | (#9197725)

I swear, they're worse than Jehovah's Witnesses. Got to hide until they go away.

Free download of a similar system for Java (5, Insightful)

Animats (122034) | more than 10 years ago | (#9197735)

We did this twenty years ago, for a dialect of Pascal. See Practical Program Verification [acm.org] . 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 [hp.com] developed at DEC SRL. This was developed at DEC before HP shut down that research operation. It's still available as a free download [compaq.com] .

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.

Sounds like Resolve (2, Interesting)

etcshadow (579275) | more than 10 years ago | (#9197774)

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

Re:Sounds like Resolve (1)

mdf356 (774923) | more than 10 years ago | (#9198089)

I was a TA for the early years of Resolve, and took a precursor class in ADA.

The point of the Resolve keywords was to document some of the things that SPARK wants documented, like the use of variables. The Resolve folks also wanted pre/post conditions specified in comments in a formal language, as SPARK does. The difference, as I can see it, is that SPARK has a tool that analyzes the contract, whereas Resolve used humans to prove the code met the contract. Cheers, Matt

Why not make the tester the compiler? (2, Interesting)

192939495969798999 (58312) | more than 10 years ago | (#9197786)

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.

Re:Why not make the tester the compiler? (2, Informative)

tcopeland (32225) | more than 10 years ago | (#9197866)

> you only have to write the tests
> 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:
public void testStack() {
Stack s = new Stack();
assert(s.empty());
s.push("hello");
assert(s.pop().equals("hello"));
}
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!

Software deserves more respect (3, Interesting)

bigberk (547360) | more than 10 years ago | (#9197804)

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:Software deserves more respect (1, Insightful)

Anonymous Coward | more than 10 years ago | (#9197894)

Certification is definitely a must with certain software, and the field of Software Engineering needs some major work, but don't take it too far. If you want a program that you know is correct, you have to prove it's correct. For non-trivial programs, that is simply intractible. What's more, although you can try to create metrics to decide when a program is "good enough", there's also a good chance you'll be wrong. Let's say you somehow managed to cover 50% of the cases (very unrealistic) and decide that works. So you deploy it, people start using it, and they start to hit the remaining 50% of the cases. Unfortunately for you, one of those cases you didn't test causes the system to cease working, or worse, go into an unknown state.

There's many many many things that can be done to improve software. There's ways of adding redundancy, simplfying the source, properly reusing components, and so on. It's still going to be difficult.

If you want to do that for mission critical software, I'm all for it. But if you expect that for an application like Word, don't expect to ever see another version of Word again.

Re:Software deserves more respect (1, Insightful)

NineNine (235196) | more than 10 years ago | (#9198022)

First off, Windows is the ONLY software that's used both in commercial, industrial, specialized applications, AND on Timmy's computer in his bedroom. Of course it's going to be attacked more than say, a program that runs a CNC machine. I'm betting that many more specialized programs are even MORE vulnerable, but they're not exposed to anywhere near the abuse that Windows is. (ie: I've never heard of anybody hacking or even attemting to hack an elevator's software).

Secondly, we have the entire legal system behind software. You have a problem with the software that runs your x-ray machine? You can 1. Sue the manufacturer or 2. not buy the damn thing again. It's already in place.

Delphi Assert (1)

tcdk (173945) | more than 10 years ago | (#9197811)


Procedure Add(X: In Integer);

--#global in out Total;

--#post Total=Total~ + X;

--#pre X > 0;


1. Global vars: BAD.

2. Borland Delphi has had some of this for while with the assert [about.com] function.

It's basicly a way of making sure that all the things that can't go wrong, actually doesn't.

Re:Delphi Assert (0)

Anonymous Coward | more than 10 years ago | (#9198087)

Please read the article. The assert function is a dynamic check while SPARK programs can be checked statically.

Re:Delphi Assert (1)

dioscaido (541037) | more than 10 years ago | (#9198100)

Assert also exists in VC++, and Java, and can be quite useful.

I believe the instrumentation shown in the article is intended to be read in by an analysis tool, which should, in theory, find errors/inefficiencies that you as a programmer may not have noticed, and hence wouldn't have represented within asserts. But, as has been mentioned before in another comment, such errors are rare enough to not justify having to migrate to Ada and write so much extra instrumentation.

John Barnes (0)

Anonymous Coward | more than 10 years ago | (#9197844)

This guy played football, raps and now writing a computer book. What could possibly be next???

No Rangers, Everton and Man United fans will be buying this book thats for sure.

using ada is enough (4, Interesting)

acomj (20611) | more than 10 years ago | (#9197946)

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:using ada is enough (0)

Anonymous Coward | more than 10 years ago | (#9198284)

If x goes above 15 or under 0 during runtime you get a constraint error.

At which point your 5-billion dollar rocket goes off course and has to be destroyed from the ground.

Why not save yourself a few bucks and write a program that can't raise a constraint error at runtime? And ask SPARK to prove that this is the case.

Ummmmm... (3, Interesting)

randombit (87792) | more than 10 years ago | (#9197958)

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 [praxis-cs.co.uk] , 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 [cypherpunks.to] 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 (2, Interesting)

quixoticsycophant (729112) | more than 10 years ago | (#9198070)

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

Eiffel and Sather (2, Informative)

Jecel Assumpcao Jr (5602) | more than 10 years ago | (#9198092)

People interested in this should also check out Eiffel [eiffel.com] and Sather [berkeley.edu] as well.

I needed this six months ago (3, Funny)

spun (1352) | more than 10 years ago | (#9198179)

My last software project ran off with my wife, stole all my money, and crashed my new corvette. Damn! I really could have used this, instead I hired a bunch of Klingon programmers.

IMHO the only way to go (2, Insightful)

Alwin Henseler (640539) | more than 10 years ago | (#9198309)

First thought I had here was another quote, probably saw it before somewhere on /.:
"The true measure of a good coder is not how complex his code is, but how simple."

Today's software systems become bigger, bigger, and bigger. Maybe single components are simplified, debugged or optimised, but not a system as a hole. The results we see today, in many systems, a single slip in one place, can screw up the entire system.

IMHO the logical way to combat this, would be to design software using methods that can be formally proven to do what they're supposed to do. Such methods do exist.

Today's security measures in operating systems (like running apps as non-root user under *nix) are in place at least for one reason: an assumption is made, that as a piece of software grows bigger, it's simply not possible to guarantee that there are no bugs in there, that it will always work as expected.

That assumption is flawed: it is possible to design software such, that it always works as expected (hardware failures aside, that is). Doing so is just very hard. Not impossible.

Load More Comments
Slashdot Login

Need an Account?

Forgot your password?