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,c59f452174bd555 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,c59f452174bd555 X-Google-Attributes: gid103376,public From: Nick Leaton Subject: Re: Use of DBC as "executable SRS": scaling problems Date: 1997/08/12 Message-ID: <33F0263B.56B6@calfp.co.uk>#1/1 X-Deja-AN: 263727745 References: <870209420.19031@dejanews.com> <33DF0010.3545@calfp.co.uk> <33E0A26B.1630@flash.net> <33EF20DF.5390@calfp.co.uk> <33EFD297.3663@flash.net> X-NNTP-Posting-Host: calfp.demon.co.uk [158.152.70.168] Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-08-12T00:00:00+00:00 List-Id: Ken Garlington wrote: [snip] > > I would believe you should be writting all. In practice they are > > probably written > > by different people, so make the assumptions transparent and executable > > is good > > practice. > > "Executable," unfortunately, doesn't help the reviewer, which was the > subject of my discussion. It also doesn't help if the invalid input is > not seen prior to operation. > > I don't know exactly what you mean by "transparent," but I assume you > mean "easy to read." However, that's not the issue. Consider the > proposed Ariane-5 Eiffel solution. The assertion #3 ( X <= Maximum ) > is certainly easy to read. Now, prove whether or not X _will_ > exceed Maximum for the Ariane-5. That's much more complicated, > since there may be a great deal of complexity hiding between the > system environment inputs and the value of X when it reaches this > assertion. Note that assertion #1 may be based on different criteria > than #3, so #1 may pass while #3 fail. So, adding more assertions > doesn't help here; in fact, it dilutes the review effort. By transparent in the case of Eiffel assertions I mean that they are clearly visible to the reader of the code. 1) They are in set places 2) They are in the code 3) They have a standard form (logical expression) Compare this to the situation where they are in some other documentation. 1) They are not in set places. They may be on one project, but they are not in set places for all projects 2) They may be in the code, but as comments. 3) They don't have a standard form. They probably are in English. English is prone to ambiguity. Having coded assertions in any language a least make sure they compile, and so are in some standard form. So Eiffel helps 1 and 2. 3 is applicable to any language. > > > > > > 2) Writting assertions forces you to consider if the requirements > > > > are well formed. If you can't write an assertion, has the requirement > > > > been stated in an unambiguous way? Is it realisable? etc ... > > > > > > However, they cannot usually detect _missing_ requirements (Ariane 5 > > > case). > > > > Yes. Do you have a method that does? > > Actually, there are such techniques. Failure Modes and Effects Testing > is very powerful for determining systems that are missing critical > fault-detection and fault-tolerance requirements, for example. Nothing stops you using this. Coming back to the general point, DBC only adds to the software development process. It is optional. However, I do agree with Meyer in that you ignore it at your peril. If you are worried about timing being critical, which is the only valid point that I have read, I have some concerns. Writing safety critical software where getting something to work within a set period, and you don't have a large safety margin to spare worrying. Similarly if you have to rely on software timings extensively. Getting faster chips strikes me as a better idea, or waiting till they become available. If you can't, you have a research project not a production system. I would be interested in knowing more about the patterns that you use to handle exceptions when they happen. -- Nick