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

[Giant Panda]

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

Re:question

[kunudo]

There is, just leave it at 1.

Re:question

[DrEldarion]

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

Those who can't teach, teach theory.

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.

Re:question

[Anonymous Coward]

| 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

[yermoungder]

Not every job in the world advertises on Jobserve but granted the number of SPARK jobs out there is small... but growing!

If you have any SPARK experience I know several places that would be interested in a CV.

Re:question

[yermoungder]

...and Baysian Probability will bite yer bum! You can _never_ prove the absense of run-time errors by testing. You can prove it using static analysis tools such as SPARK, or those provided by PolySpace (Ada, C, C++) or SofCheck (Java). Personally, I find testing as exciting as drying paint, so I'm totally behind using these static analysis tools but it seems there are a lot of people who enjoy unit testing out there...

Re:question

[yermoungder]

Yeah, now what you mean... But the low salary is "Programming Language Independent"! :-( Bet you get to turn out any old sh*t too!

Re:question

[yermoungder]

They're only buzz words if you don't understand what they mean... ...and since when did "Baysian Probability" become a 'buzz' word!! :-O

Re:question

[yermoungder]

Actually, that's exactly what I do and have done for the last 16 years - all in aerospace.

Re:question

[rahard]

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

: Those who can't teach, teach theory.

Actually, those who can't, consult!

A man goes to a pet store and found an expensive monkey. He asks the store owner, "how come that monkey is so expensive?".
Store owner: "He can program in Basic!"
The man goes to another cage. The monkey is more expensive. He asks the same question.
Store owner: "He can program in C!"
Then they go to the last cage. The monkey is outrageously expensive. The man asks again.
Store owner: "Well, he does consulting!"

-- br

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:question

[boots@work]

I think it would be really interesting to work in a place that genuinely and deeply cares about quality. (Or maybe it would be really frustrating. Either way.)

Maybe when I get older and more curmudgeonly...

A _review_?

[Caine]

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

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:A _review_?

[Anonymous Coward]

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

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

[happyfrogcow]

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

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

Re:But what..

[Waffle Iron]

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

Re:But what..

[Mikkeles]

SPARK only covers programme verification. There are other formal methods which cover specification (e.g. Z) as well as various theorem provers which can link all these parts together to ensure no contradictions, etc.

A search on Google for formal methods will give you a lot of stuff. The first site that comes up is a good starting point.

Note that at some point, one has to hope that what the client wants is what he has described. A tax calculation programme will not be of use if he really wanted a customer relations management system :^)

Re:But what..

[Fearless Freep]

But all this does is push the problem one level higher.

One advantage to doing it that way is that by pushing it higher you push it earlier in the process, were it will be cheaper and easier to fix...and hopefully more obvious as well

Re:But what..

[Beryllium Sphere(tm)]

>.if the contract itself is wrong?

In real life that's what usually kills people.

_Safeware_ by Nancy Leveson looked at several software-related disasters. Only one disaster, the Therac radiation machine that fried several patients, was the result of actual bugs (and those bugs were race conditions). The rest consisted of software obediently and disastrously doing exactly what it was supposed to do, like the black lab at #7 in http://www.dorsai.org/~walts/darwin.html.

If you build safety-critical software be sure to have some organized way to flush out what-if questions and hidden assumptions.

Re:But what..

[AdaDaddy]

_Safeware_ by Nancy Leveson looked at several software-related disasters. Only one disaster, the Therac radiation machine that fried several patients, was the result of actual bugs (and those bugs were race conditions).

The Leveson book is informative but not exhaustive. There have been several software safety incidents not covered by the book. It is not advisable to assume _Safeware_ describes all software failure modes.

Race conditions are only one of many dangerous failures in safety critical systems. Others (also not an exhaustive list) include deadlocks, timing skew, unhandled exhaustion of resources (memory, file space, fuel, power), buffer overflows, numeric underflows or overflows, and unexpected values from implicit conversions.

Remember the Mars rover last year. It had a nearly total failure of control software due to a full file system. The problematic behavior was not a case of properly executing the requirements. It was a violation of requirements not caught during testing because the duration of testing was significantly shorter than the duration of the actual mission.

The SPARK approach does flush out a lot of what-if questions. While going through the exercise of trying to formally prove compliance with requirements, the developer exposes ambiguous, poorly expressed, and contradictory requirements. Nancy Leveson also promotes a rather formal analysis of system requirements. That analysis is necessary both in builing a correct system and in identifying the safety hazards inherent in the requirements.

Car Whores?

[SirChris]

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.

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

[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

Re:public class interfaces

[William Tanksley]

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

Re:public class interfaces

[joggle]

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"

Like CORBA 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:public class interfaces

[gewalker]

I'm not so sure about Eiffel. In Eiffel, you can declare class invariants, which are contracts that must apply to your class and all inherited classes. Sounds like it includes OOPL contracts to me. Eiffel also has loop invarints.

Anyway, I see nothing new in DBC in SPARK not already in Eiffel.

Re:public class interfaces

[Fearless Freep]

Or more like Eiffel with pre and post conditions, etc...

or a ot of other languages with data validation written at the begging and ending of each method

Re:public class interfaces

[William Tanksley]

Er... Read my message again. I wasn't knocking Eiffel; on the contrary, I was giving Bertrand credit for having DBC nailed before SPARK came along.

I also wasn't talking about Eiffel's support for DBC; I was describing DBC in general, or more accurately DBC without OO support. I didn't claim that OO isn't possible with DBC (on the contrary, I stated that it was, and I would explain it if asked). I didn't claim that Eiffel didn't have OO.

And finally, the huge thing that's new in SPARK that isn't in Eiffel is static contract checking. That's not present in Eiffel, for all its wonderful features.

-Billy

Re:public class interfaces

[arn@lesto]

The problem with contract programming is that most people are incredibly bad at describing preconditions and postconditions. They either over specify or worse leave something out; the result is that the contract is invalid.

The code gets written and it turns out to have bugs anyway. We go back to examine everything and notice missing details in the contracts. We fix those problems, the code gets re-written and the cycle continues. In the end we've not achieved much in the way of program correctness, efficiency of code, or reduction of the programers time.

Trivial examples all show the benifits of whatever new language feature has been added. It's really only after significant use and experience that we can judge how good something is in a large scale appplication.

I remember getting excited about the "Z specification" language in 1986, but in the end it was just too damn
hard for everyone. The programs were absolutely correct but if you wanted to change something later, you were back to square one. Forget about anything large involving multiple people.

Correctness isn't always necessary, some times good enough is all that is required. If you want to spend a couple of months proving that your implementation of sqrt() is correct I hope you have the funding (I see government money... enough said). Most of us can't afford this level of correctness.

Give me a sandbox, lego bricks, and let me play.. go away I don't like your rules.

Re:public class interfaces

[William Tanksley]

Your point that "correctness isn't always necessary" is well taken. The more you need the more you have to pay, and not every project can afford the price.

The rest of your post absolutely requires the absence of a tool like SPARK. Throw SPARK into the mix, and all your grounding assumptions are absolutely wrong -- the specifications _do_ describe the interfaces, and the interfaces _do_ work together, and the code _does_ implement the specifications, and there are no possible exceptions.

Trivial examples all show the benifits of whatever new language feature has been added. It's really only after significant use and experience that we can judge how good something is in a large scale appplication.

So tell me -- how long has SPARK been around? How many projects has it been used in? With what level of success?

Are you judging it without knowledge?

I remember getting excited about the "Z specification" language in 1986, but in the end it was just too damn
hard for everyone. The programs were absolutely correct but if you wanted to change something later, you were back to square one. Forget about anything large involving multiple people.

I've seen it used too. And I agree.

I find SPARK different -- rather than a mathematical expression of operation, it allows you to build a mathematical specification (which is easier), and tie it provably to a computation (which is fun). It's still not easy, but it's easier.

Give me a sandbox, lego bricks, and let me play.. go away I don't like your rules.

No problem. I don't like embedded programming; some people do.

-Billy

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?

Re:What horseshit

[grasshoppa]

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

Never underestimate a BOFH.

Re:What horseshit

[gr8_phk]

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

Unit testing has been shown to find something like 10% of all bugs. Forcing this crap on the programmer is not very effective and will probably lead to more confusion. People I talk to are generally in favor of less exacting languages because they are easier to work with.

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.

Well, that put Microsoft in it's place

[Anonymous Coward]

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

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

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

Re:Eurofighter

[RAMMS EIN]

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

[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

[Anonymous Coward]

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

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:Eurofighter

[Anonymous Coward]

That is what is so cool about the defense industry -- projects delivered at 1/100 the defect rate, with 1000* the manpower requirements and 5000 * the cost. Most excellent for those of us in the software business...

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.

Re:Eurofighter

[yermoungder]

Now you know that we have 1000*the man power requirements but only ever get 0.5*the men! ;-)

Re:Eurofighter

[MourningBlade]

You didn't want to use the tool because it was a "pain to type"?!

Boilerplate code, near cut-and-paste code, and highly verbose code produce greater errors, and induce programmer fatigue.

In addition, they make the code harder to understand at first glance.

That's quite important. Much is made of how unreadable Perl can be, but sitting down and trying to figure out the logic and nuances behind a bit of C code is often much, much worse. This is because the C is usually more verbose to do the same thing.

I'm not saying SPARK is worse than Perl, I am just discussing why "verbose code" can be a bad thing.

Another thing: if you ever want to change the code, add on things, etc. -- which, as we all know, happens routinely -- then the less verbose your code, the more flexible it will be.

Not really much worse or more error-prone than having to rewrite several hundred lines of code to tweak something.

With these tools there needs to be an emphasis on getting as much information as possible from the code itself. Sometimes, that isn't possible. And sometimes it is.

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:Eurofighter

[Bozdune]

It's funny how history repeats itself. I remember as a young lad in 1977 being part of a study that evaluated various software engineering design methodologies for DoD. All the aerospace companies were claiming great things for PSL/PSA, RSL/RSA, and the other methodologies of the day. Hard figures, too, like you're quoting here. So you'll have to pardon my skepticism, because I've seen similar arguments (and hard figures) like this many times before, and they've all evaporated like the morning mist.

And, call me a cynic, but I can't help being suspicious of anyone who trots out a new software development tool targeted specifically at Ada. It smells too much like an attempt to milk the DoD money machine, which is easy enough to do, rather than sell the idea on its own merit.

Re:Eurofighter

[HeyLaughingBoy]

it very rarely comes up with any real problems in the code

Do you mean that it can't find problems in the code because it's useless, or that there are no problems in the code for it to find? There's a substantial difference between the two. As someone who codes for devices where patient safety is critical, I find tools like this very interesting.

VLISP sounds much more interesting

[fuzzy12345]

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?

Re:VLISP sounds much more interesting

[Rod Chapman]

Cool! Please contact us!
- Rod (SPARK Team, Praxis Critical Systems)

Ok...

[dioscaido]

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

[William Tanksley]

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

Re:Ok...

[wintermute42]

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.

I'm not sure what you meant by formal specification here. As I recall someone did a huge denotational semantic specification of Ada. In theory this massive specification defined exactly what Ada's semantics are. The only problem is that such a specification is, in practice, useless. For even simple constructs, the denotational semantic description is huge. And as with any formalism, there is always the opportunity for error. Given the complexity of denotational semantics I suspect that few people other than the author ever read the whole thing.

So that fact that Ada had DoD funding for a denotational semantic specification and Java does not does have such a specification does not make Ada more portable and reliable (in the sense that a piece of code will produce the same result on different platforms).

The idea of adding assertions and other formal descriptions of the intended semantics has some merit. But the realization is SPARC is unfortunate.

As I recall, the gang at Sun who did Java mentioned that they used C/C++ as the basis for Java because they wanted the language to be used. Choosing Ada as the basis for anything guarantees that few people will use it. The module paradigm for languages (used by Ada and Modula-2) is not as powerful as the object model. This is one reason that C++/Java have caught on and Ada/Modula-2 are consigned to history.

Finally, just because you have a specification and code that exactly implements this specification does not mean that the application will not result in unintended results (e.g., the death of users or others). Frequently the problems encountered with software are a result of conditions that the designers did not forsee. That is, things that were not defined in the specification.

Re:Ok...

[raduf]

Nobody's stopping you to use contracts, they are actually quite a piece of software engineering. As a rule you should know pre and post conditions for your methods, and definitely should write them down (comments) for library methods.
Enforcing them it's a different matter. You can cheat easy anyway (someone said in another comment that one way is to use the error messages) and if a programmer is used to know his contracts enforcing them brings very little.

But I suppose there will always be a market for things like this, like with managers/clients who want to feel secure about their code.

Re:Ok...

[yermoungder]

The "no dynamic memory allocation" is also useful for avoiding fragmenting RAM - pilots get grouchy about that sort of thing! ;-)

Re:Ok...

[yermoungder]

Er, you obviously missed out on Ada95 which add OO (yes, polymorphism/inheritance) to the language. Ada0Y (scheduled for 2005) looks very likely to add Java-style "interfaces".

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

[imbaczek]

You seem to suggest that Java or C++ are type-safe.

Re:Ok...

[wintermute42]

Yes, I admit it! It's true that I have not kept up with developments in Ada. I'm still scared by horror inflicted by the original version. And the trauma produced by the Ada design philosophy which produced languages like VHDL.

OK, so they added objects, interfaces and other wonders of modern languages. But it still does not change the fact that Ada is not exactly in the main stream. To continue my walk out on the limbs of issues with which I am only shallowly familiar, I'll speculate that very few people would use Ada if it was not mandated by their sponsors (e.g., the Dept. of Defense).

Re:Ok...

[William Tanksley]

So that fact that Ada had DoD funding for a denotational semantic specification and Java does not does have such a specification does not make Ada more portable and reliable (in the sense that a piece of code will produce the same result on different platforms).

You're right that the phrase "formal specification" was a bad choice on my part. Ada doesn't have an official formal specification (although SPARK does); what Ada has is a highly formal official specification, automatically verified by an extensive validation suite that every compiler must pass.

This official requirement made writing Ada compilers VERY hard (a big reason why Ada wasn't successful), but it also makes it possible to write unambiguous formal semantics for a clean, useful subset of Ada. This is what SPARK uses.

And SPARK does formally guarantee precisely what you claim it can't: that a piece of code will produce the same result on different platforms, and even on different compilers. Once you've verified that the code is valid SPARK, you also know that it's valid Ada, and that it's totally and purely portable. No annotations or theorem proving needed.

Choosing Ada as the basis for anything guarantees that few people will use it.

That's easy to say, but there's no choice here. It was Ada, an ad-hoc language, or no solution at all. Put that way, the choice is extremely simple.

I would argue with your statement on other facets, but you've left it ambiguous enough that you could claim it's correct no matter what the facts are. (All you have to do is say, "That's not what I meant by "few people.") Let me just say that SPARK appears to be the only product in its solution domain -- that is, there's no choice if you need to be 100% certain that your code won't throw an exception and give you an Arianne 5.

The module paradigm for languages (used by Ada and Modula-2)

Stop right there. Ada doesn't use "the module paradigm". It's a full-power object oriented standard, and has been since Ada 95. It's had genericity and static polymorphism since the original Ada.

Finally, just because you have a specification and code that exactly implements this specification does not mean that the application will not result in unintended results (e.g., the death of users or others).

There's no doubt of that. Or those results may have been the INTENDED results (military applications) -- the compiler can't tell the difference.

So I have to agree with you.

Frequently the problems encountered with software are a result of conditions that the designers did not forsee. That is, things that were not defined in the specification.

But using SPARK does mean that you DON'T have "problems encountered with software." If you have a problem, you know good and well where it came from -- bad specifications, not bad software. That's a huge improvement, wouldn't you agree? Narrowing down the location of the fault is the first step toward fixing it.

-Billy

Re:Ok...

[yermoungder]

Probably true - but then being popular doesn't make something 'good' or 'worthwhile'. Ada83 certainly had a lot going /against/ it - lousey and very expensive compilers for one. This is simply not true of Ada95 compilers as a) the language was improved; and b) the compilers got a lot better and a lot cheaper (including free).

Theorem proving languages

[Believe]

This sounds a bit like Alloy. 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 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

[killjoe]

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.

Re:Theorem proving languages

[Elbows]

It's actually quite different. Eiffel lets you embed contracts in your code which are (optionally) checked at run-time. Even with contracts, your program can pass all its tests and still have hidden bugs.

Alloy lets you model a system (Alloy code isn't executable), and statically prove properties about the model. Once you verify the model, you prove that it's correct for all possible runs (but you still have to implement it correctly).

Re:Theorem proving languages

[yermoungder]

Say "hello" to Alloy-SPARK! :-) http://www.cee.hw.ac.uk/~air/

Programming by Contract?

[RAMMS EIN]

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?

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

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:Programming by Contract?

[RAMMS EIN]

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

[Mikkeles]

For example; see this demo on insertion sort (amongst other things) which is proved to: a) sort and b) produce a permutation of the input.

It uses acl2, a lisp language based prover.

Re:Programming by Contract?

[Suslik]

Ada functions can have side effects; SPARK functions can't (that is, if they do have side effects, these will be detected by the analysis tool and generate an error). Also, you can't have recursive subprograms (directly or indirectly recursive). :-)

Postconditions are useful for proving partial correctness, i.e. correct if the subprogram terminates. They are useful because, in general, it is easier to specify a constraint than implement it - see how much easier it is to program in declarative (functional) languages than in imperative. (And Ada allows fixed point arithmetic, which is easy to reason about, and floating point arithmetic, which is harder to reason about but not impossible).

Disclaimer: SPARK hacker for the past 6 years.

Re:Programming by Contract?

[TheLink]

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

That's like saying disk mirroring and ECC is a waste of time.

The value of writing things twice or thrice is when it turns out it's not the same thing after all. Then you know you have a problem (whether you can fix it there and then is a different problem ;) ).

If it's significantly easier to write one of the "checks" that'll be rather useful.

Re:Programming by Contract?

[sql*kitten]

Apart from the syntactic sugar, how does that differ from C's assert.h macro?

Re:Programming by Contract?

[RAMMS EIN]

``That's like saying disk mirroring and ECC is a waste of time.''

Oh, come on. It's not the same at all; disk mirroring, ECC and such is redundancy automatically generated from the original source.

``The value of writing things twice or thrice is when it turns out it's not the same thing after all. Then you know you have a problem''

And I'm saying it's a waste of time. Most of the time, your first attempt will be right, and duplication is senseless overhead. In cases where your first attempt is wrong, you have no guarantee that the contract will catch it. The only thing you know for sure is that you wasted time writing contracts for the parts that do work.

Re:Programming by Contract?

[William Tanksley]

SPARK's assertions differ from C's because SPARK's are gueranteed to be complete and correct, otherwise the verifier won't let you past.

You could, in theory, use to do design by contract, but you'd have to be very careful to put your assertions in the right places, make sure that none of them have side effects, and manually do a few other things that a DbC language automatically takes care of for you. It'd be risky, but it's possible. It becomes MUCH harder when you add object orientation, though; managing inheritance of invariants becomes very difficult.

-Billy

Re:Programming by Contract?

[TheLink]

"Oh, come on. It's not the same at all; disk mirroring, ECC and such is redundancy automatically generated from the original source."

Same sort of thing. You say it's not worth it and that may be true for you. But there are people who claim it is worth it to them - many are just trying to find better methods.

Error checking is not worth it for many. Most of the time the transmission will be right and duplication/redundancy is senseless overhead. In cases where the transmission is wrong, you have no guarantee that error checking will catch it. The only thing you know for sure is that you wasted time and resources doing error checking for the parts that do work.

Seriously tho it's just a matter of how good this method is (not all ECC methods are good or practical) - if it takes too many bits for the error detection and correction it does then it isn't very good at all. But if it really doesn't take that many bits for each actual data byte then it will be useful for many.

Re:Not so impressive

[Anonymous Coward]

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

Re:Reminds me of the real estate guys

[symbolic]

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

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:Free download of a similar system for Java

[Curtis Clifton]

ESC/Java has been picked up by a group based at the University of Nijmegan. Their new version, cleverly called ESC/Java2, supports the full syntax of JML for writing specifications and is more expressive than the last version from Compaq/SRC. The JML project also provides tools for runtime testing of assertions in Java code (like Java 1.4's assert, but much more expressive), and for automatically generating unit tests from method specifications.

Both the JML tools and ESC/Java2 are open source. ESC/Java2 is based on patches applied to the source available from Compaq/SRC; a combined binary download is available.

If you're interested you can get ESC/Java 2 or the JML tools by following the links.

Full disclosure (or shameless plug): The JML tools are developed primarily by my adviser's research group at Iowa State University. The tools run on top of the MultiJava compiler that I developed as part of my M.S. degree. JML works with pure Java, but you might be interested in the MultiJava language, which adds multiple dispatch and open classes to Java. More info. on Multijava is available from MultiJava.org.

Re:Free download of a similar system for Java

[Animats]

I'm glad to see someone is working on that.

If you're involved in that, you might want to look into how we avoided the "false axiom" problem that makes ESC/Java unsound. ESC/Java has an Oppen/Nelson type prover. So did we. But we also used the Boyer-Moore theorem prover, which understands recursion, to prove more difficult theorems. This removed the need for users to add "axioms".

There's so much that could be done in this area. We really do know in theory how to eliminate bugs. Somebody needs to make that a usable technology.

Re:Free download of a similar system for Java

[AdaDaddy]

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.

The problem with such a tool is its limitation to static checking. Many of the most pernicious errors are dynamic. Consider race conditions, timing skew, and deadlocks. SPARK is more than a set of tools. It is also a specification of a subset of Ada. That subset was carefully chosen to avoid many of those dynamic errors.

While Java is statically verifiable and widely used, it is also not dynamically verifiable. The performance of a Java program on a given hardware platform is highly dependent upon the particular JVM the program runs in. More than that, Java synchronization is not temporally deterministic. It is relialble on the average. Being reliable on the average is simply not good enough for many safety critical real time systems.

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

Re:Sounds like Resolve

[mdf356]

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?

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

Re:Why not make the tester the compiler?

[tcopeland]

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

[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:Software deserves more respect

[Anonymous Coward]

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

[NineNine]

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.

Re:Software deserves more respect

[radish]

Ever notice how the services performed by such "professionals" as lawyers tend to cost a small fortune? People want their software to stay cheap...witness the whole outsourcing debacle - this is never going to fly.

Re:Software deserves more respect

[bigberk]

Maybe the increased cost is worth it? If industry loses billions of dollars a day due to spam (which is carried through insecured Windows hosts) and associated viruses, worms, and intrusions, then aren't you paying for the cheap software in another way?

Re:Software deserves more respect

[plopez]

Lot of good suing the software vendor does you when you're dead. Also you may not have been the person who purchased and there is no guarantee that the purchaser knew what they were buying.

UNIX:
runs databases (commercial)
runs manufacturing equipment (industrial)
runs handheld portable units (specialized) and I've seen it used on a SPRC box as a controller for BAS (big ass switches)
and it is currently easy to get a copy of Linux, BSD or Solaris running in your bedroom.

Your arguments do not hold water.

Re:Software deserves more respect

[kaladorn]

Engineers are a profession. They get paid like one, have legally protections and responsibilities, and are pretty picky about who they let in. Stuff developed with proper engineering method costs $$$. So, if we put software in this category, your web browser would cost $900, it would be updated once every year for another $400, and it might or might not interoperate with any other software. If the engineers (following proper engineering method and using design-for-testability or design-by-contract or inherently correct languages) had been the sole force in computer development, the PC would still be 60 pounds and run a 8 MHz. It'd be robust and stable, and no threat to public safety, and you could play a nice VGA game on it, if anyone was insane enough to write games in its underlying language, and they'd go broke doing it. This is no disrespect to engineers - there are types of software where this approach is not only merited, but required. Their professional standards and legal liability make them careful about what they put their name to or what they let pass through their hands. But a lot of the software *has* no public safety issue. Public safety and the safety of your bank account *may not be equivalent*. And we always (WE, the Consumers!) want the newest game, the newest graphics, the best sound, the newest networking, blah blah blah - WE drive the development world by buying what it offers and demanding what it has barely thought of. I'm all in favour of a rigorous development approach for mission critical software for police, fire departments, hospitals and the military. Oddly, this is where we see a lot of this stuff being done now. But I'm not in favour of requiring every PC user to invest $10000 to buy a 486-speed machine and another $1000 a year for the annual software update to the THREE programs anyone has ever written. We need to develop software by having an eye to what the software must do, the market it must address, and the need for it to be robust vs. the cost to make it so. By en large, the world as it stands with all the spam and viruses and such *seems to be working*. Yes, money is wasted, but the world keeps on turning, and a lot of security IT guys are employed, Network Nazis get extra large overtime paychecks, and the average user still manages to clunk ahead. Rarely do lives hang int he balance or does the world grind to a halt. So, would I like to see a more stable and secure windows OS? Sure. Have I ran Windows (98, then NT4, then 2000, then WinXP Pro) for many years and NEVER had a virus strike or hacker zombify my boxes? Yes, I have. Do I security patch? Intermittently. But I do run a firewall or two (software, all), and I do follow some basic precautions. But with that, I've survived with little crisis. So, is the problem causing the world to grind to a halt? No. A net slowdown or two until the head net engineers get some patches in place, but we can live with that. It's annoying, but hardly worth upending the entire model of how software is developed and why....

Re:Software deserves more respect

[ttys00]

There is no such accountability for software development.

If there was, it would take a lot longer to churn out. Companies/management want their software now, now, now.

Look at Microsoft Windows, that our banks and governments rely upon!

Banks and governments rely upon mainframes that were made and certified by engineers. They expect Windows to fail as often as we expect it to.

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!

General Motors isn't liable when our cars break, why should Microsoft be liable when its software crashes?

A product as complex as Windows XP would take a century to write properly. Time to market is a stronger influence in software development than in most engineering projects.

The software development industry as a whole is still in its infancy. And infants are generally not held legally liable for their actions.

Delphi Assert

[tcdk]

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

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

Re:Delphi Assert

[dioscaido]

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.

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

[Col Bat Guano]

but only if the idiots who managed the Arrianne 5 project require you to use software from another rocket (Arianne 4) without testing the code on a static work bench.

Unbelievable but true.

Re:using ada is enough

[polar bear]

Disclaimer: Praxis employee, used Spark on several high integrity projects, love it.

Image your plane is flying along, and then x becomes 16 because of a scenario you didn't think of and thus didn't test. Constraint error, and program stops.

The Spark version has a PROOF that this cannot happen. You can thus fly your plane knowing that the software is NEVER going to raise a constraint error.

This makes me a happier passenger!

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

Re:Ummmmm...

[rpg25]

Actually, I've seen a bunch of safety-critical systems that were written in Pascal or some godawful assembler, so I don't think complaining about B&D languages is a big issue for high-reliability systems.

That whole, "if this fails, people die," thing takes a lot of fun out of the process. You're just not going to add much back. And it's not at all clear you ought to. Perl is pretty far from a B&D language, but I'd sure hate to see an autopilot written in perl, no matter how productive or satisfied it made the coder.

Re:Ummmmm...

[randombit]

Actually, I've seen a bunch of safety-critical systems that were written in Pascal or some godawful assembler

My Dad hand-patches microcode on 60s-era safety systems in a chemical plant for a living. It's pretty intense. :)

Perl is pretty far from a B&D language, but I'd sure hate to see an autopilot written in perl, no matter how productive or satisfied it made the coder.

The happiness of the coder is not really the issue. If we could get safe, secure, reliable software by coding them in restrictive languages (or beating the programmers with sticks, whatever), then by all means we should, if it's worth what it will cost.

The first problem is that nobody has any really convincing evidence that, all other things being equal (testing, design methods, skill of people involved, time/money available), SPARK or similiarly restricted languages actually gets you any meaningful improvment in security as compared to, say, Pascal, Ada95, C++, Java, O'Caml, or a similiarly "full of pointy bits" language.

Secondly, the languages restrictions mean the programmers/designers have to spend more time (ie, money) working around the limitations of said language. It's economics. If a particular application (Word or Photoshop or your firewall or what have you), *never* crashed or failed in any way, would you be willing to pay 1000 times as much for it? 100x? 10x? Twice as much, even? For an autopilot, it might make sense. For 99% of the stuff that's out there, it doesn't (read Ross Anderson's papers on the economics of security for some good details on this area), because the cost of a failure (for the people writing/selling the code) is between zero and tiny, and the cost of making it not fail is high. It's cheaper to write crappy software, unless your legal/political liability is so fscking high that you *have* to make in safe.

Re:Ummmmm...

[yermoungder]

FYI, tasking (a Ravenscar profile of tasking anyway) has just been added to SPARK. Adding generics (that's templates to C++-types) is a medium term goal.

Re:Ummmmm...

[Indigo]

"The first problem is that nobody has any really convincing evidence that, all other things being equal (testing, design methods, skill of people involved, time/money available), SPARK or similiarly restricted languages actually gets you any meaningful improvment in security as compared to, say, Pascal, Ada95, C++, Java, O'Caml, or a similiarly "full of pointy bits" language."

Maybe not, but I can offer my anecdotal evidence that avionics software written in Ada is a hell of a lot more understandable that avionics software written in C / C++. Ada may be boring, but it isn't plain mean :-)

Honestly, I always disliked Ada on general principles. But after working with a few hundred thousand lines of the stuff, I've changed my mind because "what you see is what you get." You don't have to worry about a lot of invisible and semantically subtle things happening behind your back (thinking of C++ here in particular). Ada has its own issues, but that isn't one of them.

With all that, I've discovered over time that the real problems (the ones that cause me personal heartburn) tend to be in ambigous or poorly specified requirements, and in interaction with other systems (which again often is due to requirements). At best the code is solid enough that you can look for requirement or interface issues without wondering what the code is doing, that you don't see.

Re:Ummmmm...

[john.r.strohm]

The first problem is that nobody has any really convincing evidence that, all other things being equal (testing, design methods, skill of people involved, time/money available), SPARK or similiarly restricted languages actually gets you any meaningful improvment in security as compared to, say, Pascal, Ada95, C++, Java, O'Caml, or a similiarly "full of pointy bits" language.

I'm sorry, but that statement is factually incorrect.

Pratt & Whitney collected metrics on jet engine controller software development, over multiple projects, over a period of ten years. The military controllers were all in Ada, the civilian engine controllers were in various things, with C/C++ heavily represented. The team capabilities were about equal across the board. After they crunched the data down, they discovered that Ada was giving them twice the programmer productivity and 1/4 the defect density.

They now do ALL of their jet engine controller software in Ada.

There have been a number of other studies and experiments, and they ALL have yielded similar kinds of results. In theory, language shouldn't matter, but in practice, it does.

Re:Ummmmm...

[joib]

The military controllers were all in Ada, the civilian engine controllers were in various things, with C/C++ heavily represented. The team capabilities were about equal across the board. After they crunched the data down, they discovered that Ada was giving them twice the programmer productivity and 1/4 the defect density.


On an offtopic note, I remember a study comparing Fortran 77 and C in a scientific/techical setting, and the conclusion of that was that Fortran codes had 1/2 the defects of comparable C codes.

C/C++ does have its uses, but writing reliable, easy to maintain software doesn't seem to be one of them.

Re:Ummmmm...

[rpg25]

I don't think we're in as much disagreement as you do.

I write tons of perl. Why? Because the vast majority of my code is not mission-critical. I'm not about to start writing even Ada, much less SPARK because, as you point out, it's not worth the cost.

The next question is whether B&D languages are worth the cost for mission-critical applications. I'm inclined to think that they are --- perhaps.

The "perhaps" has to do with what we take out of a language to make it a B&D language. There are lots of things I think are not worth removing. But I can think of some things that are a slam-dunk. For example, C and C++ have way too many ways to give aliases to a memory location. I'm inclined also to think that while C's type coercion is mostly benign, when you apply that liberal stance to C++, which has a far richer type system, it's a mistake. Making people responsible for turning floats into integers and vice versa doesn't seem too bad.

For that matter, unit discipline seems like a B&D thing that's way overdue. Losing the Mars probe is yet another wake-up call that we've slept through. Values should have units, and if you try to combine values with different units, the compiler should either barf, or add code to do the conversion.

The second "perhaps," is how do we evaluate these B&D languages? I'm actually not very optimistic about there being any quick answer from experimentation. There are way too many variables for us to expect quick answers from experimental studies any time soon. So we're going to have to muddle through on judgment. And in judgment, as you so clearly point out, we must weigh the costs against the benefits.

A last word about the costs, though. Right now we're only paying attention to the costs to the producer of the code. You point this out yourself when you say:

It's cheaper to write crappy software, unless your legal/political liability is so fscking high that you *have* to make in safe.

This is not a great way for a society to make decisions, and the plethora of spam, worms, and viruses makes that abundantly clear. Sooner or later, some high-stakes control application is going to sneak onto the internet, and then we'll really hurt. Another problem is that you and I may know that our code is not of a quality appropriate for a mission-critical application, but there's no reason to believe that the user shares this appreciation. There are all too many examples of people putting mission-critical applications on the same OS with applications that are not up to that standard. Then problems with the low-security applications (including the pests that plague them) get to have their chance at the mission-critical app. Think of the CIA director pulling classified files onto his Mac laptop and taking them home with him....

Somehow, we have to get a consideration for social costs into the decision-making of software producers. Maybe by fixing our liability system (software producers really don't have any appreciable legal liability now), maybe by regulation. I tend to favor the former, although that's very unfashionable these days. But we should be having that conversation now. When somebody blows up a nuclear power plant, refinery, or tanker full of LNG, it will be too late to have a rational discussion, and we'll get a bad answer.

Re:Ummmmm...

[randombit]

The team capabilities were about equal across the board. After they crunched the data down, they discovered that Ada was giving them twice the programmer productivity and 1/4 the defect density.

AAAAAHHHH! Look at the list I provided. You'll note that Ada95 was in there. I am not saying anything bad about Ada (still haven't learned it, but I should). What we're talking about is SPARK, which is basically an Ada subset. Do you really think that a language without recursion, dynamic memory allocation, or function side-effects is going to be as productive as a language that does? Of course languages built for programming with side-effects (O'Caml, Lisp, etc) that's not a restriction, but in an imperative language it's not going to be very fun.

A comparison of Ada and C/C++ is very interesting, but not terribly applicable when the language under discussion is a language which looks rather like Ada but with many language features removed. Most of those features were not removed because they are inherently insecure, but because nobody has figured out how to write a correctness prover for a program which uses those features.

Re:Ummmmm...

[john.r.strohm]

OK, I see your argument a bit more clearly now.

The statement AS YOU POSTED IT is *STILL* factually incorrect, although you have to go back a few more years.

In 1982 or 1983, Don Good's group at UT Austin delivered the Message Flow Modulator to the United States Navy, for acceptance testing at Patuxent River Naval Air Station. This was a relatively small piece of code, running in (as I recall) an LSI-11.

The acceptance test suite was developed by a different company. No one in Don's group saw the acceptance test suite before the official test at PAX River, and (obviously) there had not been any "dry runs".

They passed, on the first try, with no exceptions, no deviations, no waivers, no "yeah but", no NOTHING. They passed.

This had NEVER happened before in military computing, on ANY project, of ANY size, large or small, from ANY contractor, EVER. As far as I know, it had never happened before on any civilian projects, either.

Read the paragraph again. There were NO bugs in that code. There were NO surprises. THERE WERE NO HOLES.

Now the punchline. They were working in a language called Gypsy, which was derived from PASCAL, but had certain things removed, and a lot of specification constructs added, that made it quite a bit like SPARK. Gypsy did have tasking, with special buffers between tasks (and no global variables at all), but I don't think the MFM used tasking for anything. Gypsy did not have dynamic memory allocation or function side-effects; I don't recall whether it had recursion. (I tend to doubt it, since recursion implies dynamic memory allocation "under the hood".) The whole point of the Gypsy feature set was that the features were ONLY those for which proof rules were known.

Now, we come to the crux of the matter. To paraphrase Gerald Weinberg, I can get wonderful programmer productivity, in any language you like, if the resulting program doesn't have to be correct. If you are willing to tolerate random bugs and random security holes and random system crashes, possibly resulting in random loss of human life, then there is no reason to go to something rigorous. If, however, the program must be correct, must not contain random bugs, must not crash at random moments, must not spray lethal doses of radiation into randomly-chosen therapy patients, then there does exist concrete evidence to suggest that those freedoms and powerful features are both unnecessary and dangerous.

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:Newspeak

[SimonWright]

"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

If the software in question is running a heart pacemaker or the engine controls of the aircraft I'm flying in or the car I'm driving, I would very much rather have the creativity of programming killed than me or my family.

Eiffel and Sather

[Jecel Assumpcao Jr]

People interested in this should also check out Eiffel and Sather as well.

I needed this six months ago

[spun]

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.

Re:question - Answer

[mykepredko]

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

IMHO the only way to go

[Alwin Henseler]

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.

Re:IMHO the only way to go

[Elbows]

Having (briefly) done some research in program verification, I'd have to disagree with you.
Proving non-trivial programs correct is nearly always intractable, if not strictly speaking impossible. We simply don't have the computing power to do it for larger programs, and (IMO) we probably never will.

Re:IMHO the only way to go

[yermoungder]

Hmmm, there are certainly people out there who disagree with you! :-) Not just SPARK guys but also PolySpace and SofCheck.

Proving sqrt() correctness?

[GGardner]

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

Re:Proving sqrt() correctness?

[yermoungder]

It doesn't - that's not what statis analysis is about. To show that what you writen is what was required (i.e. 1+1=2) you still need to do dynamic testing. These are complimentary tools, not competing.

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

Re:Proving sqrt() correctness?

[boots@work]

I'm mildly amused that one person could like both Perl and SPARK.

Just a toy, or what?

[jbaltz]

Does the book go into whether or not SPARK is used anywhere in practice, or is it someone's toy compiler?

//jbaltz

Re:Just a toy, or what?

[yermoungder]

Yes it is used extensively on the EuroFighter Typhoon aircraft, Airienne space rocket, Mondex cash cards, etc.

Parent not offtopic

[gumpish]

I see, so theSpoke is an MS "community" site where one can find polls like "what car would Visual Basic be?" and view entries in the Imagine Cup short film festival which has a logo very much like the XBox.

How crappy.

Thanks for the linkage.

design by contract: D Programming Language

[reubgr]

The D programming language has design by contract. It seems pretty similar to the SPARK idea...

Check this out.

It's part of a presentation that can be found here


-Reuben

The D Programming Language

[WalterBright]

already has, as part of the language, Design by Contract and unit testing. The D Programming Language. These provide the robustness capabilities, but while having the power of a C++ like language.

It's been done

[WalterBright]

and it's called the D Programming Language. It has Design by Contract and unit testing built in to a C++ like language.

Homeland Security

[yermoungder]

WRT: SPARK check out this report: http://www.cyberpartnership.org/SDLCFULL.pdf The report's task force was co-chaired by Microsoft and Computer Associates people and is being submitted to the DHS. It explicitly recommends SPARK as one method of increasing reliability/security. It also states "A programming language with significantly fewer possibilities for mistakes than C or C++ should be used where possible."

Knuth said it best...

[KurtP]

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

Re:Can you have high-integrity without…

[yermoungder]

In aerospace, there is rarely any need for dynamic memory management (post "initialisation") - you know how many of any kind of object you are going to be dealing with at compilation time. In Ada you just don't need to resort to pointers 99 times out of 100 as the compiler will hid all that for you.

Re:Another ADA proselytizer

[Bill, Shooter of Bul]

Yeah, they can be a little intense. Ada was the first language they taught at my college. Avoided it like the plauge it is. It was incredible what students didn't know how to do after two years of ada. Good programers can program in ada while ada programers can... program in ada.

Re:Can you have high-integrity without…

[AlecC]

Or rather, in aerospace, safety critical system have been limited to the kind of problem that can be solved without dynamic memory management.

I could imagine plenty of problems which are open-ended, safety critical, which you might want to build a computer system to solve, but dare not. Free routing, for example. Every plane has a GPS and tells every other plane where it is and where it is goint, and all the planes agree to adjusrt their speeds to avoid each other. Unlimited number of other planes transmitting routes of arbitrary complexity - and if you get it wrong, doom. On the other hand, in crowded airspace, fuel savings of up to 25% - big bucks. But too dangerous for today's software technologies. The hardware is up to it, but we cannot write the software.

Re:Peer Review Request

[flockofseagulls]

> while 10 do ...
> How can I ensure that this cannot be exploited?

First ensure that it does what you expect. You wrote an endless loop. Who needs hackers to exploit code when programmers can't even write code that works?

Check out D

[mcoupland]

The D programming language includes language support for design-by-contract but, unlike SPARK, it's a sane language. (It's C++ without the suck and with some more modern features.) I'm still investigating it, and it's still under development , but I strongly recommend checking it out, C++ fan or not.

Here's a (necessarily trivial) example, taken from the website:

long square_root(long x)
in
{
assert(x >= 0);
}
out (result)
{
assert((result * result) == x);
}
body
{
return math.sqrt(x);
}

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

Re: the limits of proof

[wintermute42]

To expand on the point made above...

Let us assume that we have a magic proof system that will prove that our software matches our specification.

So what do we use to define the specification? Certainly not a natural language like english. Natural languages are full of ambiguity. So we'll use a formal specification language. However, such a language is basicly like a programming language, perhaps supporting more mathematical formalism (maybe single assignment). While our formal proof system can prove that the specification is equal to our executable software, we still can't show that the specification is what we intended (e.g., the specification may have bugs).

Even if our specification is magically guaranteed to be exactly what we intended, properly specifying the design as we understand it, this does not address the problem that systems fail because of the unexpected.

There are language systems that allow some level of proof. For example, in logic synthesis, where binary logic networks for VLSI can be generated from the subsets of Verilog and VHDL languages, it is possible to prove that two designs are or are not the same by using logical reduction. This can be useful in verification and testing. But it does not change the fact that VLSI designs, just like software designs, have bugs (also known as design errors).

Even leaving the concerns about the notation to specify a problem, software perfection could only be theoretically achieved when the problem can be completely specified. Many of the critical systems where there is a lot of interest in software correctness are very complicated (e.g., modern fighter jets). The exact requirements for these systems cannot be specified since their behavior under all conditions cannot be known. So the software will always be imperfect. What we hope is that the software is not imperfect in ways that cause death.

Agile methods

[JacobO]

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

I have to disagree here, the agile methodologies I'm aware of stress automated unit testing to ensure the code that follows meets the specifications. They are agile because the "contract" enforced by the unit tests allow you to see what you have broken easily after a change. If your unit tests pass then you've either not broken anything or your test coverage is insufficient. It seems that these SPARK "tags" have some of the benefits and all the problems that a good suite of automated unit tests provides.

I do however like the idea that your assumptions and dependencies are explicitly mentioned nearby where they occur. These are things that definitely sting you, especially in code you are new to (written by someone else.) All the little interdependencies and unexpected side-effects that make their way into code can really make life difficult sometimes.

I have a feeling though that this would take discipline, and if all team members were skilled and disciplined then you would likely have much of these things stated anyway.

Re: the limits of proof

[Indigo]

"What we hope is that the software is not imperfect in ways that cause death." I'm copying that into my code file. That really says it.

I agree with your other points by the way. The code is the least of your worries. If it does what the requirements says, that leaves you more time to worry about whether the requirements are right, especially in the face of all the things that can screw up while it is running.

constraint errors are exceptions in ada

[acomj]

replying to an AC....

In our ada code constraint errors are handled by the exception handling. Also note that a lot of our messages/values are comming from hardware from external hardware, so we have little control over what we're getting, so read in the message into unconstrained types and then convert. We test each potential incomming message against max/min theoretically posibly values. So we think we have most of it handled.

I'm not saying I'm against the idea of SPARK, it just seems to duplicate all the testing we do. If I have a procedure that returns a float from 1.0 to 5.0 I don't need to test if its going to kick back a 6.0.

Re:GNU Nana for C++

[Animats]

Eiffel's Bertrand Meyer is considered father of Design by Contract methodologies.

No, he's just the publicity guru of them. He came late to that technology. C.A. Hoare is probably the "father", back in the 1970s.

Oracle PL/SQL packages do something similar

[gentlewizard]

Oracle's proprietary extension to SQL, PL/SQL, is based on Ada. Its "package" concept borrows the contract/implementation dichotomy. First the public interfaces to the package are declared in the PACKAGE object; then the implementation is defined in the matching PACKAGE BODY.

This enables procedures to be public in scope (present in both PACKAGE and PACKAGE BODY) or private in scope (present in PACKAGE BODY only). Other elements, such as user-defined data types, constants and cursor definitions, can be part of a package as well as procedures and functions. Overloading is supported by creating multiple definitions in the PACKAGE with different "signatures" (name plus calling sequence).

So, yes, this concept is being used every day, though not with the extensive rigor of SPARKS.

25 years after the first type inferencing systems.

[Baldrson]

We are now poised to move forward with type inference based on full blown inference engines, thereby dispensing with the nonterminating arguments over statically vs dynamically typed languages that allowed Steve Jobs's spawn such as Object-Pascal/Objective-C/Java to get its nose in the tent. If you want to declare a "type" in a declarative language, just make another declaration and let the inference engine figure out what it can do with that information prior to run time. See how easy that was? Well, there is more to it than that, but not that much: Assertions have implications and assertions made prior to run time have implications prior to run time. Live with it and don't repeat the mistakes of the past.

Engineering?

[TheLink]

I am not an authority in programming/engineering, but here's my guess why most software is crap despite all that talk of Software Engineering and those brilliant ideas:

Engineering World:
1) design
2) blueprint
3) plastic/clay/3D models
4) Real Thing

Software World:
1) design
2) Sell as version 1.0
3) Sell as version 2.0
4) Sell as version 3.1

Here's the biggie: the blueprints, plastic models cost about the same amount to make as the "real thing".

Willing to pay X times more for software and wait Y times longer? Will programming teams actually be allowed to do those Engineering steps?

No? Well you have to settle for the crappy plastic model then, or the scribbles on a sheet of blue paper.

Debugging will always be with us.

[billtom]

As soon as we started programming, we found to our surprise that it wasn't as easy to get programs right as we had thought. Debugging had to be discovered. I can remember the exact instant when I realized that a large part of my life from then on was going to be spent in finding mistakes in my own programs.
-- Maurice Wilkes

Re:Debugging will always be with us.

[krischik]

You are right. However I have also learned that the choice of programming language influences the amount of debugging needed.

One study says that the amount of bugs in Ada is 1/10 of that in C. And SPARC 1/10 of Ada.

I would also venture that the amount of debugging needed in Ada is 1/10 of that in C.

And while you still have to debuig an Ada programmer does not not spend a large part his life from then on in finding mistakes in his own programs.

With Regards

Martin

Re:GNU Nana for C++

[booch]

Damn, my mod points just expired, and the parent post is VERY informative to anyone interested in this thread. And it's too late to hope than other moderators might be reading this thread.

Spark is not Turing-complete.

[Vintermann]

As I understand it, Spark is not Turing-complete. You can't make dynamic data structures in Spark. Otherwise, the halting problem would still be unsolvable in this subset of Ada, and so the strict verification which is the purpose of Spark would be impossible.

So yes, it's definitely not a general purpose PL, but for those rare applications where it is warranted, it does what it's supposed to (give immunity from a large class of software problems in exchange for a _lot_ of hard work). Perhaps you're not convinced, but they seem to be at lockheed martin etc.