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,d1df6bc3799debed X-Google-Attributes: gid103376,public From: kaz@vision.crest.nt.com (Kaz Kylheku) Subject: Re: Not intended for use in medical, Date: 1997/05/01 Message-ID: <5kbak0$2em@bcrkh13.bnr.ca>#1/1 X-Deja-AN: 238773167 References: <3.0.32.19970423164855.00746db8@mail.4dcomm.com> <5k5ifi$8db@bcrkh13.bnr.ca> <3367CE1E.5ED1@die_spammer.dasd.honeywell.com> Organization: Prism Systems Inc. Newsgroups: comp.lang.ada Date: 1997-05-01T00:00:00+00:00 List-Id: In article <3367CE1E.5ED1@die_spammer.dasd.honeywell.com>, John Apa wrote: >Kaz Kylheku wrote: >> >> In article , Robert Dewar wrote: >> >John said >> > >> ><> >Make use of Appendix H (Safety and Security) in Ada95. >> >Review the object code. >> >And then test the hell out of it like my life depended on it.>> >> > >> >This sounds like depending on testing too much, and on formal methods >> >too little -- there is a balance sure, but the above seems unbalanced. >> >> Reviewing the object code is (or can be) a formal method. Maybe the >> use of the word ``hell'' shifts the perception of balance. :) > >Yes, perhaps I added emphasis to the wrong part. Formal methods are a >great thing if you can get everyone to follow them. To me it seems as if The trick with formal verification is to ``program by contract''. You identify the weakest preconditions for the operation of every component, and verify that it satisfies the postconditions. Once you verify that a component does the right thing for every valid input, you can verify the higher levels that use the components without again looking into the internals of the previously tested components. The individual tests could be done empirically (set up every possible precondition and execute the component) or they can be done formally (prove that the component arrives at the post-conditions if the pre-conditions are satisfied). I like the language feature in Eiffel which lets you codify pre- and post-conditions, and turn on their verification. The problem is identifying what those conditions are. Ideally, they should be codified in some way so that testing can be automated. I've written code in the past where I simply stated what the conditions were in a comment. That's obviously of little use except in a peer code review. >many people talk about it yet few actually follow it. This is bad. A >team using a well defined and accepted development process and formal >methods can do great things. But it only takes one of the team to "just >make a quick fix" and then the fun begins. > >In any case if my life depended on it, I would still test it beyond what >many would consider "acceptable". I have slipped my own schedules in >order to do a little extra testing or desk checking when I (or others) >owe our end users that, especially the ones who trust our work to keep >their planes in the air. > >To bad MS didn't feel that way about their products. I don't normally use ``MS'' products---I've never touched a Microsoft application such as Word and it's been years since I used DOS---but today I had the rare displeasure of using a communication program under Windows 95. Now they call this a ``platform'', but to me, the word suggests a rigid plate that a man can safely stand on. It turns out I had to reboot the system twice because even though a terminal program called ``Hyperterminal'' that became ``locked up'' was successfully aborted, the system did not release the serial device occupied up by that program. As someone from a UNIX background, I had to laugh. My Linux system at home has no trouble releasing a process' resources no matter how it terminates, and this is a freely distributed operating system written by volunteers. The X server and window manager also let me manipulate the window of a ``hosed up'' process in the usual manner; it turns out that the frozen Hyperterminal window could not be moved, closed or minimized. Incidentally, Hyperterminal froze up when I tried to send a file via Zmodem, but accidentally clicked `OK' without having specified a file name. That's robustness and reliability for you! I am surprised that people are looking to use Ada on this ``platform'', as I can tell by reading this newsgroup. What's the benefit? You might as well code in K&R C without function prototypes. The so-called platform will likely cave under before your program execution reaches the first instance of undefined behavior. It's rather like anchoring a steel-and-concrete house to loose soil.