Re: Not intended for use in medical devices

[dewar@merv.cs.nyu.edu (Robert Dewar)]

Kaz says

<<<<I agree with R. Dewar: your concerns are misplaced, and don't make a good case
for avoiding inspections of the object code. In a safety critical system, an
incorrect translation of a correct program could lead to death, injury or
property damage. There is no other way to catch this sort of error except to
compile the code and then inspect the results of the translation.>>

  I certainly agree with this. In fact I never heard of a people using a
  process for generating safety-critical code that did not require this
  kind of review, and certainly the formal standards require this.

<<In some ways, this could make somewhat of a case for using assembly language in
the first place, since in the process of reviewing object code, you have to
acquire an understanding of the program at the machine language level anyway.
I can at least appreciate where this extreme viewpoint is coming from.>>

  I strongly disagree with this, and find it surprising that anyone would
  suggest this. The review of the object code is just one of many aspects
  of the total methodology required for safety critical code. Another
  important aspect is more emphasis on the use of formal methods in
  developing and analyzing the code at a high level, and these are
  very much language dependent, and make assembly language quite useless.

  The object code review is oriented to making sure that the code reflects
  the high level intent correctly, and the objectives used in analyzing
  this code are directly derived from the original high level code. This
  is why Annex H in the RM requires Ada compilers to provide assistance
  in correlating the object output to the source (see annex H if you have
  not read it!)

How many of Ada's advantages over something like C are still relevant when you
have to inspect the object code instruction by instruction?

  All of them, and in fact they are probably more relevant than in other
  domains. Eliminating all possibilities of error from a program is 
  achieved by a layered approach, and the help that an Ada compiler
  gives in smoking out typing errors etc, and the help that the high
  level Ada semantics give in forumulating appropriate conditions for
  verification etc are of *especially* important value in SC systems.

  Also, see annex H which is oriented towards requiring that Ada tools
  have suitable facilities. For example, a validated C compiler may not
  even have a capability at all for examining the generated assembly code.
  But a 100% conforming Ada compiler (including conformance to Annex H)
  MUST have such a capability. For example, the -S and -g switches in
  GNAT that generate assembly language annotated with source line and
  label information is not just a nice-to-have feature in the context
  of annex H, it is a *required* feature.