Re: Certified C compilers for safety-critical embedded systems

["Robert I. Eachus" <rieachus@comcast.net>]

Robert A Duff wrote:

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

Ah, but the mistake required all valid Ada 80 compilers to solve the 
halting problem.  The solution was to remove that requirement.

And that is my point, when specifying programming languages such issues 
are a (maybe not common but occasional) occurance.

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

I chose my words carefully. RM 10.2 (27) "The implementation shall 
ensure that all compilation units included in a partition are consistent 
with one another, and are legal according to the rules of the language." 
  Often failure of the compiler to determine that there is a consistent 
elaboration order means that there is no valid elaboration order.  But 
we allow the compiler to reject a program if it didn't find a valid 
order.  Why?  See above.  Requiring the compiler to find a valid order 
requires solving the halting problem.  (Note that an implementation MAY 
choose an order that cannot be shown to be inconsistant, and provide 
code that causes Program_Error if access before elaboration occurs.) 
But if there is no valid elaboration order, and the compiler detects 
that, the program is illegal.

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

There is no requirement to OPTIMALLY solve the bin-packing problem, 
true.  But if there is a size clause applied to the record, then we do 
require the compiler to find a consistant solution if one exists.

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

I agree with you on this case.  I was thinking about the case where the 
implementation detects that there is no LEGAL elaboration order.  Such a 
program is illegal and may be rejected.  If it cannot be detected 
whether a valid elaboration order exists, then the compiler MUST 
generate code to raise Program_Error if an illegal elaboration order 
occurs.  The "classic" case is a program that has a library unit that 
reads in input from the user, (in the sequence of statements in the 
program body) and either makes or doesn't make a call to the main 
program before it is elaborated.

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

Agreed.

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

Go back and read G�del.  He uses a clever encoding of a logical calculus 
in the factors of (large) numbers (G�del numbering) to show that 
arbitrary statements can be encoded in an arithmetic formula with a 
limited number of terms.  That showed that recursion is not necessary to 
cause a language to accept contradictory statements.

-- 
                                           Robert I. Eachus

"The war on terror is a different kind of war, waged capture by capture, 
cell by cell, and victory by victory. Our security is assured by our 
perseverance and by our sure belief in the success of liberty." -- 
George W. Bush