Certified C compilers for safety-critical embedded systems

Please, let us not start this Ariane 5 discussion again. There have been at least 3 threads on this topic, and the later threads have done nothing other than rehash the arguments from the first thread. There are enough reruns on television, we don't need them in newsgroups. Unless one of us comes up with something about Ariane 5 that has not been said here before, can't we just move on?

Reply to
Frank J. Lhota
Loading thread data ...

It would seem intuitively obvious to even the most casual observer that if you're not sure what a thing is *supposed* to do, you can't possibly be sure that it does it. Unfortunately, this lesson is often learned at great financial (and sometimes human) expense.

MDC

Robert I. Eachus wrote:

--
======================================================================
Marin David Condic
 Click to see the full signature
Reply to
Marin David Condic

It's always been my contention that writing the specifications which you will then prove that a program obeys is exactly as hard as writing the program itself.

Reply to
Hyman Rosen

Well, saying they can't result in safe software would be even wronger, of course. So I guess the real idea that has to be buried is that they _will_ do so, just like that.

Or, in other words: no matter how good your tools, the GIGO principle (garbage in, garbage out) still holds.

Which would appear to be one of many special cases of what we used to call the "lemma on conservation of difficulty" among students here. In the essence it says: "No truly difficult problems ever go away just by waving some magical tool at them."

--
Hans-Bernhard Broeker (broeker@physik.rwth-aachen.de)
Even if all the snow were burnt, ashes would remain.
Reply to
Hans-Bernhard Broeker

Yes and no.

Yes, in that writing rigorous formal specifications is HARD WORK.

No, in that the effort you put into writing those rigorous formal specifications almost always translates into significantly-reduced effort when writing the code that implements those specifications, because now you have a SOLID understanding, where you used to have only a sketchy understanding.

Reply to
John R. Strohm

Depends on where you draw the line. I have been on Ada projects where more that 85% of the effort and budget went into requirements and design (through to detailed specifcations, which included writing the Ada package specs). All of them finished on time and under budget.

If you do the design right, writing, debugging and testing the package bodies is easy. But I don't recommend that you contract the coding to Primate Programmers, Inc. (PPI):

formatting link
;-)

--
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture, 
 Click to see the full signature
Reply to
Robert I. Eachus

Maybe, but nobody showed any better way. Or do you think that XP (eXtreme Programming) did?

--
Regards,
Dmitry A. Kazakov
 Click to see the full signature
Reply to
Dmitry A. Kazakov

Not always true---we can specify the Halting problem (for a Turing Equavilent machine), but we cannot implement it without an oracle.

-CRM

Reply to
Chad R. Meiners

specifications

code

It has been my observation that there's an inverse relation between the difficulty in describing what's needed and the difficulty in implementing it. Perhaps this is just another aspect of the specification difficulty -- once you've clearly specified what's needed, it's not that difficult to implement it.

Reply to
Everett M. Greene

I was once involved with a US DoD agency project that was very well specified, the specifications having been years in the making. All was going along well until two years into the implementation phase when it was "discovered" that the equipment meant to be monitored and controlled by the project's product had been removed from service several years earlier!

Reply to
Everett M. Greene

Actually not quite true. It is not hard to write a program that implements the Halting problem, and for any finite machine, it will always return the correct answer. If you allow the number of intermediate states for programs submitted to be unbounded, then you cannot bound the execution time for the (combination of) program and machine that implements the Halting problem.

The Halting problem and a real time constraint is an impossible combination. For that matter, anyone who works with hard real-time knows that you have to allow for the possibility that all of the constraints on the system cannot be met. Then you have to do the engineering part of the job and select the right tradeoff. (Which may include a higher power budget or extra weight, or even more money so you can build a custom chip.)

--
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture, 
 Click to see the full signature
Reply to
Robert I. Eachus

This would be a specification for the Halting problem for a bounded Turing Machine.

This would be the specification of the Halting problem for a Turing Equivalent machine.

Yes, that was the point. Writing the specification for the Halting problem is much easier than writing the implementation since the implementation doesn't exist.

I completely agree.

-CRM

Reply to
Chad R. Meiners

... snip ...

And at other times writing the specification becomes easy after you have implemented the widget. Maybe the key is to remember that both the specification and implementation are always subject to revision in the light of experience, deeper analysis, etc.

--
Chuck F (cbfalconer@yahoo.com) (cbfalconer@worldnet.att.net)
   Available for consulting/temporary embedded and systems.
 Click to see the full signature
Reply to
CBFalconer

:> > Not always true---we can specify the Halting problem (for a Turing :> > Equavilent machine), but we cannot implement it without an oracle. :>

:> Actually not quite true. It is not hard to write a program that :> implements the Halting problem, and for any finite machine, it will :> always return the correct answer. : : This would be a specification for the Halting problem for a bounded Turing : Machine.

Are you sure you can say that a program that implements the Halting problem for a bounded Turing machine does not implement the same problem for a Turing machine?

Georg

Reply to
Georg Bauhaus

Turing

Of course you can SAY it! I just did ;-)

It depends what you mean by implement. I tend to think of implementations as algorithms (which must halt). Therefore, since there is no algorithm that satisfies the Halting problem's specification (it is undecidable), there is not an implementation. If you want to define implementation as something else (reasonable or unreasonable), all bets are off of course.

-CRM

Reply to
Chad R. Meiners

Excatly, or anyother way of making my point. All physical machines have limits even if someone builds a self-replicating von Neuman system that keeps growing itself, it would be limited by the available matter in the universe. But in reality, for realistic time frames even the PC on your desk is a sufficiently close approximation to an infinite Turing machine. Does it really matter if I give you an implementation of the Halting problem for your PC that will always halt within a trillion years, instead of one that does not halt for some inputs? (And are you sure, if you had both in hand, you could tell which was which?)

Anyone who works on compiler front end and language definitions has to be ready to dance with Gödel, decidability issues and the whole nine yards. ANY compiler for a reasonable programming language, and even for some unreasonable ones runs right straight into Gödel's proof. It either does not accept some legal programs, accepts some illegal programs, or never halts for some inputs. (And as many of you know, early releases of compilers tend to do all three.) Gödel says that any Ada, C, C++, Fortran, or whatever compiler must have at least one of those three bugs in it. (In the Ada community, we aim for the first choice--that there will be some legal Ada programs that will be rejected due to implementation limitations.)

I thought it was wonderful about a decade ago when we made a decision to require Ada compilers to solve NP-complete problems--and were honest about it. Record representation specifications can be only partially specified, and we require the compiler to find a legal layout if one exists. This is of course a bin packing problem, and with not much work ANY bin packing or knapsack problem can be mapped to an Ada record representation clause.

However, for decades there have been requirements type Positive_Integer is range 0..2**Integer'Last-1;

by accident, and the Verdix compiler just kept churning away. (Of course the last expression was intended to be 2**Integer'Size-1 not

2**4_294_967_296-1.) I think a number of compilers now check for that error by bounding the terms if one gets too large. In this case once you get past 2**32 subtracting one can't bring the final result back in range, so you can declare an error and give up.

But there are actually programs in the Ada test suite that depend on the fact that A*X-B*Y is a small number for some integers A, B, X, and Y >

  1. With a computer you can hunt up some pretty nasty expressions that require several thousand digits in your arbitrary arithmetic package but the final result is say, 13. Why does Ada require this? Because it allows programs to be written using expressions meaningful in the problem domain. This goes back to the issue of making it easier for domain experts to validate designs and implementations.
--
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture, 
 Click to see the full signature
Reply to
Robert I. Eachus

A lemma, or consequence (if I'm not mistaken) is that you can calculate the fate, Halting or Not-Halting, of every program in a finite set of programs S, but the program that does this can't be in S. Even if the program took a trillion years, it would take them on a bigger machine than yours. Douglas Adams' _The Hitchhiker's Guide to the Galaxy_ does nice work with this in the nest of computer-designing hyper-super computers that would calculate the question to the great answer of Life, the Universe and Everything.

Regards. Mel.

Reply to
Mel Wilson

Where do you get this curious idea about Gödel's proof?

--
Aatu Koskensilta (aatu.koskensilta@xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
 Click to see the full signature
Reply to
Aatu Koskensilta

ElectronDepot website is not affiliated with any of the manufacturers or service providers discussed here. All logos and trade names are the property of their respective owners.