Re: Certified C compilers for safety-critical embedded systems

[Robert A Duff <bobduff@shell01.TheWorld.com>]

"Robert I. Eachus" <rieachus@comcast.net> writes:

> Aatu Koskensilta wrote:
> 
> > (#) Surely this is not the case for arbitrary formulae? If it is, Ada
> > seems rather an odd language; I've never encountered an actually used
> > computer language with correctness of a program not arithmetic.
> 
> As far as this particular case is concerned.  Yes, that is what I am
> saying.  Actually, back when MIL-STD 1815 was Ada and the ANSI standard
> effort was in progress, I wrote an example program that was legal Ada 80
> iff Fermat's Last Theorem was true.

That was simply a mistake in the wording of the Ada 80 manual.
Not a property of "all useful programming languages".

>...  There are still many cases where an Ada
> compiler is allowed to reject a program as illegal if it will always
> raise Program_Error at run-time.

No.  The Ada RM carefully distinguishes between compile-time and
run-time errors, and compilers are certainly *not* allowed to "reject as
illegal" programs that will (or might) raise exceptions.  "Reject as
illegal" means "refuse to run it".

>...  It doesn't take much work to transform
> this rule into an oracle that solves the halting problem.  Of course,
> that means that some programs will fail to compile in a reasonable
> amount of time--for any definition of reasonable.
> 
> Why does this bother you?  Remember I started this by saying that with
> Ada 95, we had deliberately accepted requiring all Ada compilers to
> solve NP-complete problems.  We know that if someone wants to he can
> write a program that transforms any NP-complete problem into a bin
> packing problem, and then writes the bin packing problem as an Ada type
> with a representation specification.  If that type declaration compiles,
> the actual layout of the type is a solution to the bin packing
> problem.

No.  There is no requirement that Ada compilers pack records optimally.
A rep-clause specifies the layout of components specified.  The compiler
must check that these do not overlap.  That can be done in linear time.
The rest of the fields can be placed anywhere the compiler likes, and
that also can be done in linear time.  There is no requirement to
(optimally) solve the bin-packing problem.

>... The program containing  the declaration just needs to print out
> the values of some static attributes.  Now does that mean that any Ada
> compiler can solve any NP-complete problem in linear time?  Not if you
> include the compile time. ;-)
> 
> I don't recommend that as a way to solve most bin-packing problems.  So
> why do we require Ada compilers to do it?  Most bin packing problems
> have easy solutions, and if you have a record declaration it seems silly
> to say that we won't require compilers to solve the easy cases because
> there are some that are hard.  Instead we warn the compiler writers
> about the tough cases, recommend an algorithm, and moved on.  If the
> user overspecifies the record layout, it might take the compiler a while
> to find an acceptable solution.
> 
> But we can't require that compilers violate G�del's Proof and we
> don't. We can't require them to solve the halting problem either, we
> just ask them to take their best shot.
> 
> RM 1.1.5(5-6): "Errors that are required to be detected at run time by
> the execution of an Ada program;
> 
> The corresponding error situations are associated with the names of the
> predefined exceptions. Every Ada compiler is required to generate code
> that raises the corresponding exception if such an error situation
> arises during program execution. If such an error situation is certain
> to arise in every execution of a construct, then an implementation is
> allowed (although not required) to report this fact at compilation time."
> 
> Translation:  There are some potential Ada programs that correspond to
> the halting problem.  If such a program will always raise Program_Error,
> the implementation is ALLOWED to reject it at compile time.  If the
> compiler can't decide, it may generate code which MAY raise
> Program_Error at run time for some inputs.

This translation is wrong.  What the RM says is that compilers can print
out a message.  It cannot "reject" such a program; it must run it.
Note "of a construct" in the RM wording.  For example:

    X := 0;
    if Some_Condition then
        X := X / X; -- divide by zero
    end if;

Every execution of the construct "X / X" will surely raise C_E, because
it divides by zero.  The compiler is allowed (but not required) to tell
you that.  It has no obligation to prove that Some_Condition will
sometimes be True.

> So a compiler can reject programs that will raise Program_Error.

No.  Compilers must *not* reject the above divide-by-zero program --
they must allow it to be run.  Even if it said "if True then" or "if
False then", it's still a legal Ada program, and we can tell that
without invoking Halting Problems.

>...  But if
> the compiler can't decide whether or not the program will, it can drop
> back and punt.  However, for any case where a compiler will ALWAYS
> reject program if it will raise Program_Error, you can do like the code
> above.  Write a partial recursive function and put the code that will
> raise Program_Error after it.  If the compiler says at compile time that
> the code will ALWAYS raise Program_Error, you know that your partial
> recursive function always halts. ;-)
> 
> The program can be messy, but take a look at 4.9.  That is the section
> that requires that static functions with static arguments be evaluated
> at compile time.

Static expressions cannot contain recursion (or even loops), so I don't
see what this has to do with Godel or the Halting Problem.

It's certainly true that some static expressions can require a huge
amount of memory to evaluate.  E.g., "2**(2**(2**(2**32)))".  I expect
any compiler to complain about that.  It's a capacity limitation, but I
don't see how it has anything to do with Godel's theorem.

>...  If you find an instance that is as elegant as the four
> line instance I found in Ada 83, we will probably "fix" it in Ada
> 1Z. (And for the same reason, to improve portability between compilers.)
> But if it takes a 500 line program, we will probably leave it alone.

- Bob