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,c59f452174bd555 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,c59f452174bd555 X-Google-Attributes: gid103376,public From: Ken Garlington Subject: Re: Use of DBC as "executable SRS": scaling problems Date: 1997/08/11 Message-ID: <33EFD297.3663@flash.net> X-Deja-AN: 263633013 References: <870209420.19031@dejanews.com> <33DF0010.3545@calfp.co.uk> <33E0A26B.1630@flash.net> <33EF20DF.5390@calfp.co.uk> Organization: Flashnet Communications, http://www.flash.net Reply-To: Ken.Garlington@computer.org Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-08-11T00:00:00+00:00 List-Id: Nick Leaton wrote: > [snip] > > Unfortunately, "divide and conquer" leaves open the issue of interface > > validation. In addition to showing the components are valid internally, > > you must also show their interactions are valid. DBC may be able to > > detect (at run-time) when an invalid interaction occurs, but to > > _prevent_ > > the invalid interaction requires much system-wide knowledge. This is > > particularly true of the Ariane 5 case, where something *outside the > > system* (the flight profile) was the root cause of the error. Consider > > a chain of events like: > > > > environment generates change > > sensor senses change > > I/O device reads sensor > > software gets value from I/O device > > software does set of calculations (including generation of error term) > > error term is converted to output format [failure here] > > > > To determine that the failure would occur, the manual reviewer must > > consider the full chain to trace the relationship of the environment > > definition > > to the out-of-range conversion. This is easy during execution (assuming > > you > > have a good definition of the environment), but hard for a human. And > > you have > > to do this for every thread (more or less). No one will tell you in > > advance > > "the error term conversion is where the error is, now just figure out > > why." > > I think I get your logic. Where would you expect the error to be raised? > > 1) Getting the value? (Postcondition) > 2) Sending the value to the calculator (Precondition) > 3) In the conversion routine (Precondition) > > 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. > > .... > > > > 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. > > > > 3) There are requirements that cannot be coded as assertions. For > > > example a bank may have a requirement that the software should > > > try and prevent the bank becoming bankrupt. Perfectly normal > > > requirement. The software can help perform this task. However, > > > stated as such, you cannot code it. You have a problem testing it. > > > > Actually, it's pretty easy, assuming you have a good definition of the > > bank environment and can run adequate scenarios. It is difficult, on the > > other hand, to have a system be able to internalize all of the factors > > regarding its environment (no system can fully describe itself, much > > less > > itself and its environment!) > > Hmmm, ok so we are now on to my home ground, even though I'm a pilot. > It isn't to code up these requirements, even running scenarios which > some banks > do (like the one I work for! ;-) ) Main reason is that it is very hard > sometimes to > come up with a workable set of assumptions on which to base your > scenarios. > Lots of banks have lossed lots of money making assumptions that are not > valid. > > > > 4) Is having assertions on utility classes and verifying them, writing > > > requirements for them a problem? > > > > > > > In the end, you would have a *very large* number of assertions to keep > > > > track of and update as the system's requirements changed. Making sure > > > > that the changes in your requirements baseline get into the assertions > > > > correctly would be just as difficult as making sure they get into the > > > > method bodies correctly, in my view. > > > > > > Again, having the assertions in place, and having the verification and > > > validation performed automatically as you run makes it more likely that > > > you find the errors early rather than latter. > > > > First, "running" is not early in the development process! > > Running the whole system, OK. 'Running' parts of the system? I want > to run my code as quickly as possible, in order to validate the design. > This > is not contrary to 'accepted' practice. I want to develop quickly, so I > want > to get to test quickly. See the problem above. To see if #3 really is going to fail, you need the real calculation of X from the system input all the way to the conversion. A subset of the thread may pass while the full thread fails. > > > Second, it seems that there is a schism in the DBC community. Some feel > > that > > testing (execution of the code) is the important part, while others > > emphasize > > manual verification. It makes it very difficult to discuss the > > advantages of > > DBC, when the response to "it's difficult to manually verify" is "it > > helps catch > > errors during test" and the response to "it's difficult to use > > assertions to test" > > is "it helps catch errors during manual verification." > > Manual verification is a weak argument IMHO. However in inspecting code > to > see what it does in order to use the code, it is very useful. Execution > is > very important. As aid to clear good design, I have found it to be an > excellent > aid to quality code. While, on the other hand, Mr. Meyer and others say the strongest part of assertions is manual verification. Who's right? > > > > > > > > The chance for an error under these conditions is not lessened by DBC. > > > > > > But the impact of it is, as you are more likely to catch it earlier. > > > Remember, you don't have to write the assertions. ie. Eiffel is giving > > > you an extra tool. > > > > This is the other schism: Arguments about DBC are addressed in Eiffel > > terms, > > and arguments about Eiffel are addressed in DBC terms ("DBC does not > > require Eiffel", for example). > > > > Agreed, it just makes it easier to produce code with DBC, and so you are > more likely to produce code containing the assertions. DBC in C++ is > very awkward, > and from what I have been reading about ADA, the situation is vastly > superior to > C++, but there are some drawbacks for replication the inheritance of > assertions. > (see some previous messages) > > Out of interest, do you think DBC is a bad concept, or are your > arguments mainly > a C++ vs Eiffel or anti the Ariane article? I'm still not convinced there is a unified understanding of DBC. The more I read from proponents, DBC seems to be used as a buzzword like OO, with a lot of different implementation approaches. I can hardly be against something that doesn't have an accepted definition! Am I against good documentation? No. Am I against well-written interfaces? No. Do I think DBC means the same thing as either of these? I'm not sure yet. I do think any methodology that concentrates on code is suspect, however. This is why it bothers me that DBC discussions quickly lead to "here's how you code it in Eiffel" and "you catch that problem during execution." > > > > > > > > (2) If DBC were used as an "executable SRS", the number of assertions in > > > > the > > > > system could very easily grow so large as to cause deadlines to be > > > > missed. > > > > > > Assertions are inherited. It is common for base classes to have lots of > > > assertions, deferred features (virtual in C++ parlance). Inherit classes > > > don't have many as they have inherited the assertions. > > > > > > > I suppose that most Eiffel programmers would write preconditions in > > > > terms > > > > of public attributes (i.e. require (My_Object.Attr_1 = whatever)), but > > > > even simple comparisons like this could really add up if there are > > > > enough > > > > of them. This point is only of concern for developers of large > > > > real-time > > > > systems. > > > > > > Most assertions are of this form. Checks that a reference is not void. > > > > However, most requirements are not in this form. Does this mean that > > most > > requirements won't be written as assertions? > > I disagree. You may not have a requirement explicitly written in your > design document. By definition, you should _never_ have a requirement explicitly written in your design document, at least from the end-user perspective. How many users say, "I want a word processor, and one of the critical requirements is that it check for void references!" > Let us say you have an object from an artificial > horizon, > and that, for arguments sake, it contains three values for pitch, yaw > and bank. That's a requirement, definitely. > A method/routine that has one of these objects as a parameter has a > requirment > that it is passed such an object. This sounds like design. As a pilot, did you ever call up Sporty's Pilot Shop and say, "I'd like to buy an avionics suite where, when the artificial horizon method is passed to an method, it's existence and type conformity is checked"? > (Existance and type conformity). Not > many requirements documents will explicitly state such a requirment, > although > they may state the requirement that the object is optional if that were > the case. > > If your requirements are more complex, then break them down into smaller > requirements, > divide and conquer. It's not a question of complexity... it's a question of motivation. For example, assuming you capture requirements as use cases, would you expect to see much discussion of void pointers in the average application? > > > Furthermore, I can get assertions of this form without DBC/Eiffel (e.g. > > in > > Ada, under any methodology). What's special about DBC if it causes you > > to write code just to get checks you get for free in other languages? > > DBC is not language specific. Eiffel as a language makes it easy to use > DBC. However, proponents of Eiffel say that DBC cannot be _adequately_ implemented in other languages. > > How do you get inheritance of assertions in C++, Ada for free? How can DBC be language independent if it requires specific langauge features? > > > (BTW, this is the third schism. Compare and contrast the arguments by > > other > > DBC/Eiffel advocates that most assertions are "high-level" abstractions, > > making them easier to read. I'm pretty much convinced at this point that > > DBC, like the infamous "object-oriented," can mean just about anything > > to > > anyone!) > > I agree with the point about high-level nature of assertions. Looking > though > code that I have written this is the case. Classes with a large number > of > assertions are abstract base classes of heirachies. This is not > surprising. An assertion at the top of a hierarchy is not necessarily what I had in mind as "high-level." Compare and contrast: 1. Horizontal_Bias <= Maximum_Bias (low level) 2. The system shall operate in the flight envelope shown in Figure 1. (high level, difficult to write as a simple line of code, but the real issue at the system level). For more information on all this, see: http://www.flash.net/~kennieg/ariane.html where these arguments get hashed out as much as I know how. > > ... > > -- > > Nick