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.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC 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: 1108a1,2c6139ce13be9980 X-Google-Attributes: gid1108a1,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public From: donh@syd.csa.com.au (Don Harrison) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/17 Message-ID: X-Deja-AN: 257387607 Sender: news@syd.csa.com.au X-Nntp-Posting-Host: dev50 References: Organization: CSC Australia, Sydney Reply-To: donh@syd.csa.com.au Newsgroups: comp.object,comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-17T00:00:00+00:00 List-Id: Sorry, this response is interminably long... Warwick Pulley wrote: :Don Harrison wrote: :> BTW, how do call a procedure under different names in Ada? : :By declaring a procedure that "renames" the old one, eg... Yes, I should have realised! It's the old workaround to the infuriating Ada83 visibility problem of not being able to see the predefined operators of a user-defined(?) type in client code. In spite of already with-ing the supplier module (which I don't think you should have to do, anyway - if you *use* features exported by a package, explicitly importing it is redundant), you can't see (hence, use) the imported operators. While Ada95 has ameliorated this restriction via the "with "(?) statement, it doesn't go far enough, IMO. Better would be removing the need for any explicit importation of operators. Even better, IMO, would be removing explicit imports of everything (including packages). However, I guess the existence of "use" clauses would then create ambiguity problems. Never did like "use" clauses. Interestingly, this issue reveals a benefit of unifying module and type. A unified model that dictates unique class names (eg. Eiffel's) simplifies things by allowing class names to serve a twofold purpose in clients - importing modules and entity (variable or routine parameter) declarations. In one fell swoop, the need for import statements ("with"), visibility statements ("use"), and module prefixes for diambiguation disappear. WRT renaming operations, I'm not sure whether the current semantics provide the same capability as Eiffel. For that to be the case, it would need to allow synonyms in *declarations* as in the Eiffel declaration of the equality operator (overlooking the anchored type): equal, frozen standard_equal (some: ANY; other like some): BOOLEAN is.. [This declaration gives you a common declaration for a redefinable - "equal" - and a non-redefinable operation - "standard_equal". In a mission-critical system, where you wanted to force static binding, you could use the frozen version in calls and use the redefinable version to specialise when inheriting.] A cursory glance at the Rationale - 8.3 suggests you may be able to do this but I'm not sure. BTW, I recall reading somewhere in the Rationale that Ada allows some sort of anchored type declaration. Anyone care to give an example?.. :> Yes, timing *is* something to be concerned about when applied to realtime :> systems. That's why I suggested not using assertions in the hard realtime :> threads of a process. BTW, software designed using DBC may actually run *faster* :> than code without it because you get to strip out all the defensive validity :> checks. You have already ascertained during development that operations are :> called in valid contexts so you don't have to check the context. : :In Eiffel that may be true provided that removal of assertion checks doesn't :significantly affect the performance of the code in any way. The issue of timing, :mentioned by Ken above, is a good example). Yes, that's particularly an issue in mission-critical HRT domains such as Ken's (spacecraft(?)..). For domains where timing is less critical such as ours (simulators), it becomes a viable tool. I should reiterate (in case it's been forgotten) my original suggestion that individual threads *within* an HRT system may be medium RT and hence candidates for Eiffel-style contracting. This implies an architecture in which threads may be allocated to specific processors of multi-processor hardware. In this way, the HRT threads can happily do their stuff without risk of interference from slower threads. This reality of this scenario depends, of course, on the timing requirements of inter-thread communication. :I imagine that one needs to take special care when using assertions in :languages that don't fully support them. Definitely, and I would hope GNAT, for example, allows you to use assertions without enclosing if-statements or compiler directives like begin assert () -- precondition ... -- actual body of routine assert () -- postcondition end; and allows you to turn them on or off via a compiler switch. Is this true? :From my (sorely lacking!!) knowledge :of Eiffel, clauses that define the precondition and postcondition of an :operation contain exactly one boolean statement which automatically restricts :the coder from including procedural code within these sections. Yes, the above would look like require -- precondition do ... -- actual body of routine ensure -- postcondition end; :While this argument favours Eiffel in terms of assertions, it doesn't :mean that porting this functionality to Ada will not introduce other faults. Sure. It's best to use a technique that minimises the risks - hence my expectation of what GNAT provides. :With Don's demonstration of assertions last Friday (Jul 11 18:05:13 EST) the :postcondition was implemented in the form: : :if and then : raise :end if; : :The implementation of the assertion is done with multiple statements, so :there is the possibility of important sections of code being inadvertently :added within the if-statement which would then be removed when assertions :are disabled. I agree and this certainly isn't my prefered way of emulating assertions. I would much prefer to use the technique I described above but doing so with our Ada83 Verdix compiler would require using compiler directives to wrap each assertions. As this, would be messy, I chose to use if-statements where the conditional expression was a short-circuit boolean expression. This represented a minimal risk to correctness (the first component is Assertions_On so the rest is ignored if set to False) and a small execution overhead acceptable for our medium RT domain. :I have seen this happen at least once, where an executable was released to :the test group which AFAIK was only tested with assertions enabled, and then :it was discovered that a crucial line of code was removed because it was :within an assertion block and once this error was encountered the executable :didn't crash but its functionality was imparired severely enough so that :it had to be run again. I expect you are referring to my own error (actually it was two) in which I coded the incorrect logic. I hope you'll allow me a few mistakes. After all, these were the only two extant miskakes following integration out of 172 such statements. That implies 98.84% were logically correct which, you'll agree, isn't too bad. What this does reinforce is that assertions do not obviate the need for testing but are a tool to help facilitate it. BTW, assuming what you say is correct, the assertions were turned off and the code handed over to the testers without my knowledge. I would have tested it first. :Even one error, however minor, is enough to warrant another round of :testing after assertions are removed: at least for languages that don't :fully support assertions. ..*especially* for such languages. :Even if no errors are discovered in the process :I would consider it a worthwhile exercise, if only to convince myself that :the software functions how I intended. Certainly. :A suggestion: to avoid some of these problems one could have written two :procedures, say 'precondition' and 'postcondition', each having an 'in' :boolean parameter. Each procedure should do nothing if assertions are :disabled, but if they are enabled then they would raise the appropriate :exception if the 'in' parameter was false. : :Then rather than the above block, one could evaluate a postcondition :by the call: : :postcondition(); : :and similiarly for preconditions. A sample implementation of 'postcondition' :(in pseudo-Ada) is: : :-------------------------------------------------------------------------------- : :procedure postcondition(requirement: in boolean) is :begin : :# if then : : -- check condition and raise exception if violated : if not requirement then : raise : end if; : :# else : : null; : :# end if; : :end postcondition; :pragma INLINE(postcondition); :-------------------------------------------------------------------------------- : :So when exceptions are disabled (via a compiler directive), 'postcondition' :would have a null body, and since it's inline there would be no unwanted :procedure call. It also means that you can conditionally compile :assertions without having to surround each assertion with conditional :compilation directives. Neat idea. What a pity you didn't think of it back in February! Maybe we could use it next time if we don't have something better.. :Naturally, my suggestion above still fails to prevent the addition of code :before a precondition check, or after a postcondition check, etc. Yes, although the amount of self-discipline to use it effectively is small. To eliminate that entirely, best use the real thing. :) :Yes, if you know the compiler has a bug in the first place. The trouble is :that you don't know it's a problem until it occurs, and a compiler could :have a subtle bug that only occurs in very particular circumstances. : :Although any respectable compiler has minimal bugs if any, if we don't test :our products after assertions are suppressed then we unnecessarily transform :our confidence in, into dependence on, the vendor's compiler to function :correctly. Sure. I suppose if anyone is going to emulate assertions in ways that may affected by compiler optimisations, it would be wise to become acquainted with these so you know what you're in for. :It would be irresponsible to deliver software that has only been tested with :assertions enabled, knowing that if an error occurs in the released version :then it's "not my fault". So for this reason, and for peace of mind, I would :certainly test the version of the software to be delivered to the customer. :Since we expect not to find more errors, this last phase would run smoothly :and quickly. Yes, I suspect this is usual practice. :> :Another consequence of using assertions is that you have to develop and :> :test the :> :assertions. :> :> Correct. My initial reaction when I started using them was "Gee, I've got to :> do this extra work on top of writing the "real" code! However, I found I was :> spending about a third of the time integrating compared with my colleagues :> which meant I was saving time overall and producing more reliable code to boot. : :Why should a short integration period automatically imply code reliability? Your right - this is mis-phrased. It should be: "However, I found I was spending about a third of the time integrating compared with my colleagues which meant I was saving time overall. Despite spending less time integrating, my code was more reliable." [...] :BTW, how do you verify the correctness of your assertions, You already have a built-in assertion checking mechanism in the code proper because if an assertion is incorrectly coded, it will raise an exception in *valid* circumstances rather than invalid ones. If you know that the context is correct, examination of the boolean expression cin the assertion will very quickly show you what the problem is. The upshot is that you have to think catefully about what the valid underlying assumptions are in the first place and debug assertions that reveal incorrect assumptions or simply coding errors. :and that there are :no errors that the assertions didn't find? You can't verify that of course. You can't express everything as an assertion and their use doesn't obviate the need for testing. Rather, they help facilitate testing. :Do you prefer code inspection, :or if you do your verification by executing the program itself, how do you :ensure that each section of code is exercised? Both of these. To ensure code coverage, I used the debugger to check that the right brancehes were executed in the right circumstances. :Either way, a documentation :of your method would provide a good test which can then be reproduced should :the software be modified. Yes, that would be a good idea. Not just now though - I have some test reports to write! :) Don. =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Don Harrison donh@syd.csa.com.au