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.9 required=5.0 tests=BAYES_00 autolearn=ham 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: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public From: paul.johnson@gecm.com (Paul Johnson) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/21 Message-ID: <5r028q$qoa$1@miranda.gmrc.gecm.com> X-Deja-AN: 257995179 References: <5qi26c$8ll$2@miranda.gmrc.gecm.com> <33CD6207.6007@flash.net> <5qkla1$4el$1@miranda.gmrc.gecm.com> <33CEB334.44C5@flash.net> <5qnab3$ft$3@miranda.gmrc.gecm.com> <33CFF256.61B4@flash.net> Organization: GEC-Marconi Research Centre Newsgroups: comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-21T00:00:00+00:00 List-Id: In article <33CFF256.61B4@flash.net>, kennieg@flash.net says... > >Paul Johnson wrote: > How? It sounds like you would have to have internal and external >> versions of all routines, all suitably redefined in the presence of >> inheritance. This is not a trivial suggestion. >Seems fairly trivial to me, particularly since I only have to worry >about this in certain cases. Hmmm. I'd be interested to see a framework in Ada which lets you do all the things with assertions that Eiffel does. There is quite a lot of stuff to do. Some of it can be automated, some has to depend on coding rules, and some requires new "special" variables or types (e.g. "require") which will be recognised by language tools. Any single part of the Eiffel behaviour can be brought in fairly easily, but the whole thing is starting to look rather clumsy. >Since I can structure me system to only perform the invariant from >an external call, this doesn't seem to be a big issue... How does a routine distinguish between internal and external calls? Or are you going to have two versions of each call? An internal one without assertion checks, and an external one which wraps the checks around the internal one? Or is there some nifty Ada Guru trick for making this happen :-) > The only difference is that Ada does internal >checks by defaults, Eiffel requires extra code if you want the internal >checks. I'm not so sure about this. Ada's main contribution to internal checks are its subrange types. I grant that declaring a subrange type is a bit quicker and easier than putting an invariant in, but ultimately there is not a lot of difference. Meanwhile the emphasis on putting the interfaces to routines in their assertions tends to reduce the number of explicit range checks required on variables. For instance array bound checks are carried out by preconditions on the "array" routines. Ada has a small edge here with numeric data, but anything more complex presents problems. To extend the array subscript example, how would you express the fact that the "item" routine of a hash table requires the argument value to be contained in the hash table? Eiffel just adds a "has(value)" precondition. >You have to write the appropriate assertions in the ancestor, in >either Ada or Eiffel. >To repeat: Why do I have to _duplicate_ assertions in Ada? Yes, but when you redefine the routine, you need to redefine its interface. Software Contracting (the Eiffel approach to the LSP) states that you can: 1. Weaken the preconditions (so the routine may handle a wider range of data, 2. Strengthen the postconditions (so the routine makes stronger guarantees about its effects). To express this in Eiffel you use the "require else" and "ensure then" clauses. In Ada you would have to copy the pre and post conditions, including the modifications. >ah... assert : require := (a > b); > >However, this shouldn't be optimized out if an exception is possible, I >don't think. (I'd have to go look back at chapter 11 to be sure...) I believe you are correct. Point conceeded. >> I agree that timing variations can cause different results, but why would >> they cause incorrect results? > >Because you made a mistake, of course! A mistake which will be hidden >during >your testing, but become (potentially fatally) obvious during >operational use. >This is considered a Bad Thing. Umm. Yes. So bad that I would prefer a testing regime which at least reduces the probability that it can occur. How about a special stochastic scheduler that simulates a wide variety of timing effects during testing. I must confess I would have thought that this would be a good idea. Lots of things can cause timing changes. >> [...] but why does the ability to enable and disable assertions >> cause any new problems? > >Because I have seen compilers that generate correct code with one set of >compiler options enabled, and a different (incorrect) set with a >different set of options enabled. [...] >Again, this is a Bad Thing for safety-critical systems. Agreed. I believe that the SCS people are looking at systems to verify the object code against the source, as a way of getting around this problem in general. Of course the verifier may have bugs of its own, but it is such a different piece of software to the compiler that the two bug sets are unlikely to overlap. Also it won't suffer from optimiser induced bugs. Inheritance causes headaches here because you have to reconstruct the inheritance hierarchy from the optimised jump tables. But then inheritance causes problems in SCS anyway. >Eiffel claims it's big advantage over other >languages (including Ada) in this domain is stronger assertions. This is >not a particularly useful claim if there are serious problems with using >assertions extensively in such systems, is it? Eiffel assertions are also part of the specification of classes. It is this that makes them significantly more powerful than Ada ranged types and implementation assertions. An Eiffel compiler is more likely to generate correct code with assertions removed than with them enabled, because the code required for correct assertion behaviour is quite complex. However in the general case I conceed your point. >> Hence you have doubled the associated >> work, and increased the risk of an error. Eiffel requires that you write >> the contract once, and uses the text for both purposes. > >Which is less writing, but may also require the user to see details that >are not necessary. Such as? I'm sorry, but I don't quite see what sort of details you have in mind. Have you read Meyer's discussion of assertions and correctness in OOSC? There are rules about this sort of thing (principally: the client must be able to check the precondition before calling, and verify the postcondition afterwards. No private features are allowed in the public assertions) Paul. -- Paul Johnson | GEC-Marconi Ltd is not responsible for my opinions. | +44 1245 242244 +-----------+-----------------------------------------+ Work: | You are lost in a twisty maze of little Home: | standards, all different.