From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.5 required=5.0 tests=BAYES_00,INVALID_MSGID,
	PP_MIME_FAKE_ASCII_TEXT autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII
X-Google-Thread: 103376,3d3f20d31be1c33a
X-Google-Attributes: gid103376,public
From: Karel Th�nissen <thoenissen@hello.nl>
Subject: Re: Safety-critical development in Ada and Eiffel
Date: 1997/07/22
Message-ID: <33D4B733.51A2@hello.nl>#1/1
X-Deja-AN: 258133493
References: <97071810325536@psavax.pwfl.com>
Organization: Hello Technologies, Netherlands
Newsgroups: comp.lang.ada
Date: 1997-07-22T00:00:00+00:00
List-Id: <comp.lang.ada>


Marin David Condic, 561.796.8997, M/S 731-96 wrote:

[snip on the use of special assertions for timings]

>     It's a nice idea which, unfortunately can't be done. It's often
>     not well understood by those who are mostly used to some version
>     of workstation or pc based development why you can't test the code
>     with compiler option X then recompile you're code with options A,
>     B and C and pass it on as "production" software.

Sure, you only want to deliver as tested.

>     You might do this for some form of "informal" testing - maybe what
>     we took to calling "smoke testing". (Since all electronics works
>     on the principle of smoke - if you let the smoke out, it stops
>     working - the first test is to power it up and see if any smoke
>     comes out.) Under those conditions, you could compile any way you
>     like, find your problems, fix them and recompile for the "real"
>     tests.

Yes, smoke testing, I must remember that.
 
>     Once you start any sort of formal verification for a safety
>     critical system you cannot change any of the bits in the program
>     image without having to reverify the image. How much
>     reverification you do depends on lots of factors, but it's always
>     very expensive and you don't do it lightly.
> 
>     One other thing you want to consider is this: If the code *can*
>     run with runtime checks enabled, then you probably don't want to
>     turn it off for "production" anyway. What do you gain? The only
>     reason for turning it off is because it *can't* run with the
>     checks on.

Granted, but think of the additional weight of those assertions on board
of aircraft and spacecraft.

Groeten, Karel Th�nissen