Certified C compilers for safety-critical embedded systems - Page 8

Do you have a question? Post it now! No Registration Necessary

Translate This Thread From English to

Threaded View
Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

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,
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

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

Quoted text here. Click to load it

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

Quoted text here. Click to load it

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.

Quoted text here. Click to load it

I completely agree.

Quoted text here. Click to load it

-CRM



Re: Certified C compilers for safety-critical embedded systems
:
:> Chad R. Meiners wrote:
:>
:> > 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

Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it
Turing

<humor>
Of course you can SAY it! I just did ;-)
</humor>

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



Re: Certified C compilers for safety-critical embedded systems




Quoted text here. Click to load it

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 in the Reference
Manual to solve the Halting problem, but we still dance around saying
that. In Ada you can write expressions which will be evaluated at
compile time, and the compiler must decide whether to accept or reject a
program based on the results of those computations. (Did someone say
Gödel numbers?) I once wrote a joke compiler "benchmark" that used a
series expansion to compute Pi to 50 places. (Our compiler compiled it
correctly, but took about 20 minutes.)

Actually Dave Emery and Rich Hilliard a few years later came up with an
even more torturous compiler test.  I think Dave wrote:

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,
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

   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.

Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

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

--
Aatu Koskensilta ( snipped-for-privacy@xortec.fi)

"Wovon man nicht sprechen kann, daruber muss man schweigen"
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it
specifications
Quoted text here. Click to load it
code
Quoted text here. Click to load it

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.

Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it
... snip ...
Quoted text here. Click to load it

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 ( snipped-for-privacy@yahoo.com) ( snipped-for-privacy@worldnet.att.net)
   Available for consulting/temporary embedded and systems.
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

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!

Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it


with Get_Key, Process;
--  Assuming appropriate declarations elsewhere

procedure Do_it is
     Key: Character;
     Exit_Key : constant Character := 'X';
begin
    loop
        Key := Get_Key;
    exit when Key = Exit_Key;
       Process (Key);
    end loop;
end Do_It;

An extra few lines.

- Ed

Re: Certified C compilers for safety-critical embedded systems

[...]
Quoted text here. Click to load it

Thanks.  It was a serious question.  I did want to know.

Though structurally, this reminds me of

   while (1)  /* or for (;;) if you like obscure syntax */
   {
      key = get_key();
      if (key == EXIT_KEY) break;
      process(key);
   }

which tends to be discouraged.

Another question:  Note that in C, even though get_key takes no
parameters, it is called with empty parentheses, while Get_Key in Ada
looks (syntactically) like any other variable.  ISTR that in Modula-2,
a function that takes no paramters could be called either way (with or
without empty parentheses).  Is this true in Ada?  FWIW, I like the
empty parens because they signal to the reader that something special
is going on.

Regards,

                               -=Dave
--
Change is inevitable, progress is not.

Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

This is a matter of language-specific idioms, I'd say.   The exit from the
statement list of a loop is the most flexible Ada iteration form, but it
isn't used all that often - the other forms are more common since they
cover most cases.

Quoted text here. Click to load it

The empty parens are not allowed in Ada.  Bob Eachus or someone else might
be able to give some of the rationale.  It's a case similar to the choice
of () for array indexing rather than [].  In Ada, a function result is
considered conceptually similar to a constant, as are enumeration
literals, and many of the same rules apply to them and their use.  I
suspect the syntax is intended to reinforce this.

- Ed

Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Depends on your programming style (and the type of programs you write)
how often it occurs.  I always use it for "n and a half" type loops, and
for tasks where the main body is a loop that is only exited in special
circumstances.  Certainly in Ada, such loop are not discouraged,
although some people get bent out of shape if you have two exits in a
loop.  I certainly am not going to get upset, or even be mildly
concerned about:

loop
   Input := Next_Char;
   exit when Input = 'X';
   exit when Input = 'x';
   Process_Input;
end loop;

vs.

loop
   Input := Next_Char;
   exit when Input = 'X' or else Input = 'x';
   Process_Input;
end loop;

In fact I slightly prefer the first form.

Quoted text here. Click to load it

There was a time when the parenthesis were required.  I think it made it
from Preliminary Ada into Ada 80, but definitely was gone before Ada 82.
  The argument against the empty parentheses was mostly stylistic, but
the equivalence of enumeration and other literals to function calls was
the real killer.  A rule that determine when the empty parentheses were
required was considered to be a burden on users, but it also would have
been a burden on implementors and the ARG. ;-)

Incidently there are a few cases in Ada where a function result is
equivalent to a variable not a constant.  Read about return by reference
for more details.  And of course you can have cases where a function
returns an access value, and can appear in a name on the left hand side
of an assignment statement:

function Predecessor(Node: Item_Access) return Item_Access;
...
Temp, New_Node: Item_Access;
...
New_Node.Next := Temp;
Predecessor(Temp).Next := New_Node;

Of course, this is a much more common use of functions in variable names
  than return by reference functions.

--
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture,
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it


I suspect that the use of () instead of [] has more to do with 7-bit
character sets for European languages. See
    http://archive.adaic.com/standards/83rat/html/ratl-02-01.html
and ISO 646. Same problem that gave us C trigraphs


--
    mac the naďf

Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

IMO the appropriate C phrasing is:

   while ( (EXIT_KEY != (key = get_key())) ) {
      process(key);
   }

and we should assume that get_key returns EXIT_KEY for EOF.

--
Chuck F ( snipped-for-privacy@yahoo.com) ( snipped-for-privacy@worldnet.att.net)
   Available for consulting/temporary embedded and systems.
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Your are kidding. And you realy want to use a language which can not
distinquish between a number and a character for safety-critical systems?

Quoted text here. Click to load it


I does not realy speak in favour of C if in 2003 there is still no major
compiler to meet the 1999 standarts.

But then amost nobody knows the standart anyway. Even if you are prepared to
pay the $18 to actulay see it, you are hard pressed to find the place where
you can actually order it.

The Ada standart, however, is available for all:

http://adaic.org/standards/95lrm/html/RM-TTL.html

With Regards

Martin

--
mailto:// snipped-for-privacy@users.sourceforge.net
http://www.ada.krischik.com


Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Martin...

The link in my sig leads to another that'll take you directly to
the ANSI on-line store where (for US$18) you can download it in
PDF format. I keep mine on a business card sized CD-ROM with
copies of Acrobat Reader and xpdf.
--
Morris Dovey
West Des Moines, Iowa USA
We've slightly trimmed the long signature. Click to see the full one.
Re: Certified C compilers for safety-critical embedded systems

Quoted text here. Click to load it

Thanks.


--
mailto:// snipped-for-privacy@users.sourceforge.net
http://www.ada.krischik.com


Re: Certified C compilers for safety-critical embedded systems
Quoted text here. Click to load it

"singed" char? Perhaps there is a distinction between sung and unsung chars.



Site Timeline