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: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public From: Karel Th�nissen Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/17 Message-ID: <33CE14E3.603@hello.nl>#1/1 X-Deja-AN: 257420888 References: <33CD1722.2D24@calfp.co.uk> <33CE082E.65FF@calfp.co.uk> <33CE0BB7.10CE@XYZZYcalfp.com> Organization: Hello Technologies, Netherlands Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-17T00:00:00+00:00 List-Id: Richie Bielak wrote: > > Nick Leaton wrote: > > From other posters, it seems that with life critical systems (avionics) > > that this is an important consideration. Am I the only one who finds > > this worrying, that systems you have to trust depend on some calculation > > as to how the program is going to run? What happens if a new compiler > > comes out that has a different optimisation technique? > I always thought it would be nice to have postconditions of the form: > > ensure > execution_time < 10 -- 10 milliseconds, let's say > > So an exception would be raised if the routine took too long > to execute. I agree with aforementioned posters that timing dependency should be made explicit in a formal way. In general it is not good engineering if the correctness of a program depends in undocumented ways on the compilers, its optimiser, the use of assertions in production code, the clock frequency, etc. I do agree with Ken and Robert that assertions do effect timing and caching, so that assertions in production code may be impossible, and that even testing with assertions included my give unpredicatable results. 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). However, it can very well be that this assertion cannot be used in the production code for the very same reason that non-timing assertions cannot be included. I imagine that in avionics the code is made for a very specific hardware configuration and with a very well defined set of development tools. So the dependency on compiler, hardware platform, etc., may not be a problem there. This difference has other consequences, I understood from Ken. A programmer for say an IS is not designing for a particular platform, so assumptions can sometimes be necessary, and should then be documented (possibly with assertions that are propagated up). However, with avionics, everything is known in advance so there is no reason to make assumptions about the platform and tools. The same thing applies to the specifications of the other systems in the plain it is connected with: assumptions are never wanted and never necessary. Groeten, Karel