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=-1.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,3d3f20d31be1c33a
X-Google-Attributes: gid103376,public
From: "Marin David Condic, 561.796.8997, M/S 731-96" <condicma@PWFL.COM>
Subject: Re: Safety-critical development in Ada and Eiffel
Date: 1997/07/18
Message-ID: <97071810325536@psavax.pwfl.com>#1/1
X-Deja-AN: 257630611
Sender: Ada programming language <INFO-ADA@LISTSERV.NODAK.EDU>
Comments: Gated by NETNEWS@AUVM.AMERICAN.EDU
X-Vms-To: SMTP%"INFO-ADA@VM1.NODAK.EDU"
Newsgroups: comp.lang.ada
X-Vms-Cc: CONDIC
Date: 1997-07-18T00:00:00+00:00
List-Id: <comp.lang.ada>


Karel Thvnissen <thoenissen@HELLO.NL> writes:
>
>Richie's proposal has a nice property: if we include assertions during
>testing, then if the additional coding affects the timing in an unwanted
>way, then the timing assertion will fail and the problem is revealed. It
>should be clear that in that case the system cannot be tested with
>assertions switched on, and no logical assumptions as described by the
>other assertions can be tested, but at least we know it, and we shall
>have no suprises of unexplanable difference between testing (with
>assertions) and production (without assertions).
>
    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.

    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.

    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.

    MDC

Marin David Condic, Senior Computer Engineer     ATT:        561.796.8997
Pratt & Whitney GESP, M/S 731-96, P.O.B. 109600  Fax:        561.796.4669
West Palm Beach, FL, 33410-9600                  Internet:   CONDICMA@PWFL.COM
===============================================================================
    "A government that is big enough to give you all you want is big
    enough to take it all away."
        --  Barry Goldwater
===============================================================================