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,c59f452174bd555 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,c59f452174bd555 X-Google-Attributes: gid103376,public From: card@syr.lmco.com Subject: Re: Use of DBC as "executable SRS": scaling problems Date: 1997/07/31 Message-ID: <870354811.9948@dejanews.com> X-Deja-AN: 260996795 To: card@syr.lmco.com X-Http-User-Agent: Mozilla/3.01 (X11; U; SunOS 5.5 sun4m) X-Originating-IP-Addr: 192.91.146.34 (proxy3a.lmco.com) Organization: Deja News Posting Service X-Authenticated-Sender: card@syr.lmco.com X-Article-Creation-Date: Thu Jul 31 13:13:32 1997 GMT Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 1997-07-31T00:00:00+00:00 List-Id: In my initial post, I said that I thought it would be unwise to try to "code" the software requirements specification for a complex software component as a set of assertions (boolean expressions) due to problems of scale. The reason for this is that a requirement stated in the reader's natural language (English, French ...) might require a significant number of boolean expressions in the software implementation. When that requirement is changed, the impact of the change could be significant since "dual maintenance" is required- that is, the assertions must be checked and changed as necessary as well as the method bodies. Note that it is conceivable that only one or the other may need to change. For example, if the requirement change resulted in a change to the valid range of an attribute, perhaps only the precondition or postcondition would need to be modified while the algorithm in the method body could be left alone. In response to my original concerns about scaling, Nick Leaton replied: >Divide and conquer still applies. One would hope that the component >pieces of your system will still small. Using assertions at this level >is an advantage. Divide-and-concquer (composition) does make the process of building complex software more manageable, but it does not necessarily reduce the scaling problem. A complex system is still a complex system, and composition will not reduce the number of assertions you might need to build it (it may even increase the number since decomposing the system will produce more inter-class interfaces). In my discussion of this scaling issue, I wrote the following in my original post: >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. And Nick Leaton replied: >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. As part of our software process here, our software tests must verify all of the testable SRS requirements and cover 100% of the branches in the code (we use a code coverage tool to verify this). In Ada, the only kind of automatically-checked "contract" (if you will) is Ada's type-checking mechanism, which ensures that an array index will not be out of bounds, a null pointer will not be dereferenced, an illegal type cast will not be performed, etc. If any of these "contracts" are violated, Ada's Constraint_Error exception is raised. Our testing procedure ensures that almost all errors of this type will be caught. If we were developing software in Eiffel, we would still require the same testing procedures (indeed, if you don't execute a branch of the code, the assertions along that branch won't verify anything!). As I mentioned earlier, Eiffel's assertions capture more of the "behavioral"/semantic aspects of class methods since they are not necessarily verifying that the object's attributes are legal values (Ada range check), but rather that the object is in the proper *state*. Having an exception rasied at the point where our "state machine" broke down would give better error localization in many cases. One of the common cases is managing an internal data structure like a list or tree. In Ada, a procedure to insert an element might mess up the list pointers without causing a Constraint_Error exception (i.e. a next pointer is accidentally set to null, but the insert procedure doesn't dereference this pointer so no exception is raised). The error would then not be detected until a later point in time when the list was being traversed. In a case like this, a postcondition check would have raised the exception in the offending routine, and I agree that this is better. Either way, though, the branch of code in the hypothetical "insert element" method must be executed for its design error to be caught, so DBC will not allow the error to be found prior to the software test phase (presuming that the error has already gone undetected in code reviews, etc). The other aspect of the scaling problem that I mentioned in my original post was the impact that a very large number of assertions could have on timing (applicable only to real-time systems): >(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 > 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. Nick Leaton replied: >Most assertions are of this form. Checks that a reference is not void. >As a result they are cheap to evaluate. My point was scale: each one may be "cheap", but what if there are a large number of them? The strength of the Eiffel asertion mechanism is that it serves as a way to verify that your software "state machine" is behaving as it should. However, because assertions are actually verifying the state transitions of objects, they cannot be statically "optimized away" like Ada's range checks often can. (Most Ada compilers perform an analysis of array index operations, assignments, and type conver- sions at compile time to determine whether or not a range check is required. For this reason, supressing run-time checking on an Ada program often has less of an impact than many people would expect). Such compile-time optimization is generally not applicable to assertions because the object's state is determined by its initial state and the sequence of methods that were called on it after initialization. To "optimize away" a precondition on an inter-class method call, the Eiffel compiler would have to know the client object's initial state and every method call that has been made to the object! Since this is impossible for all but trivial cases, it is therefore safe to say that if you include assertions in your class definitions, they will cost you at run-time. If there are a lot of them, this could be a problem in a real-time system. (NOTE: I am presuming the use of an Eiffel *compiler* here, not an interpreter). Nick also added: >In other systems you add such checks into the implementation, so >you have to do them anyway. This is a matter of programming style. In my experience, it is generally not done. That is, special "if" statements to check an object's state are *usually* not written at the start of the class's methods (precodnitions) or at the end of the methods (postconditions). I'm not saying this is good, I'm just saying that in my experience people do not write code "Eiffel-style" in Ada/FORTRAN/C etc. Precondition/postcondition/invariant violations are instead caught during testing, as inconsistent/invalid states usually manifest themselves via Constraint_Errors, lost/corrupt data, etc. (Again, I think Eiffel's assertions offer superior error localization during testing). If the testing is rigorous, you can validate your software state machine that way and not "pay the run-time price" for assertions. If your testing is sparse... By the way, is it possible to "turn off" Eiffel's assertions after the code has been fully tested? (I don't mean making a source code change like commenting them out; I'm referring to a compile-time option like Ada's "supress range checks"). Finally, Don Harrison wrote: >I wonder whether there has been some confusion here over the use of >"specification" in different contexts. Eiffel people use the term >in talking about assertions. Ada people tend to associate it with >SRSes. Actually, "Ada people" usually use the term to refer to package specifications or procedure/function/task specifications. Those of us in the defense industry use it for formal SRSes, though, since the US DoD usually requires a customer-approved SRS for any soft- ware purchased with DoD dollars. - Mike --------------- Michael P. Card Lockheed Martin Ocean, Radar and Sensor Systems Division Syracuse, NY 13221 voice: (315)-456-3022 FAX: (315)-456-2414 e-mail:card@syr.lmco.com -------------------==== Posted via Deja News ====----------------------- http://www.dejanews.com/ Search, Read, Post to Usenet