Re: A case where Ada defaults to unsafe?

["Nick Roberts" <nickroberts@adaos.worldonline.co.uk>]

"Simon Wright" <simon@pushface.org> wrote in message
news:x7vn0ztysj6.fsf@smaug.pushface.org...

> I find it quite hard to imagine this scenario, I must say.
>
> We have a safety-related system where it is important that the
> extinguisher is set off as soon as possible and activating the gearbox
> alert takes sufficiently long that it can delay the extinguisher
> activation beyond tolerance[1]. And we are allowing a programmer to
> change this code without any process to ensure that the safety
> properties of the system aren't compromised?

You are probably quite right! This is a failure of my example, rather than
of the point it was intended to illustrate. For many kinds of less
safety-critical Ada software such an elaborate software process is not
warranted, and my argument would apply better.

> [1] If I'm wrong about why you think your example causes a problem,
> that (to my mind) reinforces the point that making subtle deductions
> about the intent of the designer from details of the implementation is
> a big mistake.

It does reinforce the point. You are wrong (you might have been right if the
changed version were the original and vice versa). The problem I was
assuming the original version might be percieved as suffering from was that,
in accordance with the principle 'make indications code precede actions',
the action code Activate_Extinguisher(...) might get stuck (if it has a
bug), and dangerously delay the indication code Display.Activate(...). This
idea does depend on the assumption that the indicator code (having much less
to do) is much less likely to have a bug that would cause it to get stuck.

In reality, one might well use ATC time-outs to protect vital code like this
from being baulked. Furthermore, I suspect indicator code would in reality
be very separate from emergency actions code (different tasks, or probably
different devices).

Perhaps I would have done better to present the example thus:


Original code:


   if A and B then -- L1
      P;
   end if;
   if B then -- L2
      Q;
   end if;


Supposing a programmer, for whatever reasons, would like to make the
following improvement:


   if B then -- L2
      Q;
   end if;
   if A and B then -- L1
      P;
   end if;


Based on the simple deduction that since the call to B could be made before
the call to A in line L1, she can assume that A does not need to be called
before B, and that it is therefore
safe to move the call the B in line L2 to precede the call to A in line L1.

If line L1 had contained "and then" instead of "and", she would not have
been able to make this deduction, and may have felt unable to make the
improvement to the code.

--
Best wishes,
Nick Roberts