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,e01bd86884246855 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,fb1663c3ca80b502 X-Google-Attributes: gid103376,public From: Richard Riehle Subject: Re: Design by Contract (was Re: Interesting thread in comp.lang.eiffel) Date: 2000/07/25 Message-ID: <397D8CC3.BB0C9001@ix.netcom.com> X-Deja-AN: 650524529 Content-Transfer-Encoding: 7bit References: <8ipvnj$inc$1@wanadoo.fr> <8j67p8$afd$1@nnrp1.deja.com> <395886DA.CCE008D2@deepthought.com.au> <3958B07B.18A5BB8C@acm.com> <395A0ECA.940560D1@acm.com> <8jd4bb$na7$1@toralf.uib.no> <8jfabb$1d8$1@nnrp1.deja.com> <8jhq0m$30u5$1@toralf.uib.no> <8jt4j7$19hpk$1@ID-9852.news.cis.dfn.de> <3963CDDE.3E8FB644@earthlink.net> <3963DEBF.79C40BF1@eiffel.com> <396502D2.BD8A42E7@earthlink.net> <39654639.B3760EF2@eiffel.com> <85Fa5.11419$7%3.818927@news.flash.net> <01HW.B591811303737A0605DE478C@news.pacbell.net> <396C7F14.563F1BA4@lmco.com> <8kl0r6$2lp6o$1@ID-9852.news.cis.dfn.de> <01HW.B59443DD000A71F808C44DCC@news.pacbell.net> <8kt1eb$34jh1$1@ID-9852.news.cis.dfn.de> <01HW.B59822A20005ECF4078EC70C@news.pacbell.net> <8l4v6n$3mph1$1@ID-9852.news.cis.dfn.de> X-Accept-Language: en X-Server-Date: 25 Jul 2000 12:57:03 GMT Content-Type: text/plain; charset=us-ascii Organization: MindSpring Enterprises Mime-Version: 1.0 Newsgroups: comp.lang.ada,comp.lang.eiffel Date: 2000-07-25T12:57:03+00:00 List-Id: Having read this thread with interest, I have some views to share that will probably annoy people in both the Ada and the Eiffel community. >From everything I have seen, there is no clear picture that Design By Contract would have had any benefit for the Arianne V rocket. Also, there is very little anyone could have done with standard Ada 83 to prevent the error. In both cases, DBC and Ada exception handling, run-time checks were turned-off. As noted by Ken Garlington earlier, even a constraint error check (Ada) or an assertion check (Eiffel) might have gone undetected in this situation. I think the DBC notion is an excellent one for lots of circumstances. Maybe not for a system such as Arianne V. In a system such as Arianne V, how many pre-conditions, post-conditions, and invariants are warranted? Such a system typically goes through a rapid series of state transitions, each one governed by the previous state. We design each transition on the basis of what we can predict about the current state along with what we can know about the total state of the system. Under DBC we need to predict the possible states that need to be checked for each transition and guarantee some invariant for certain parts of the system. We also need to be sure the assertion checking does not take longer than the processing required to make the next state transition. In Industrial Engineering and Reliability Theory there is the notion of 100% checking for 0.001 % probability of error. Do we want to do this 100% checking by placing pre-, post-, and invariant checks at every transition point or do we try to predict where the system is at risk and apply them only at those points. Unfortunately, we in software have a poor track record for predictability. In fact, some algorithms are beyond our ability to predict through ordinary reasoning mechanisms. For example, consider Langton's Ant (you can read about it in Terry Pratchett' Science of Discworld). An Ant is on a giant grid. The squares on the grid can be either white or black. The algorthim is simple. If the Ant is on a white square, that square turns black and the ant proceeds to the square on its left. If the square is black, the square turns white and the ant proceeds to the square on its right. (This is a good programming exercise for students using a sparse matrix). We can easily declare assertions for the states of each square, but cannot declare assertions for the state of the entire grid. Why? According to Pratchett, it takes about ten thousand iterations of the algorithm before any pattern begins to emerge. And that pattern is not predictable. After ten thousand iterations, a patter does emerge, but there is no guarantee the pattern will not be broken after, say, twenty million more iterations. Large-scale software systems are often like this. We can easily declare simple little assertions that govern the state of some part of the system, but it is impossible to cover all the combinations of circumstances at this level. In both Eiffel and Ada we try to manage this complexity by creating small, well-formulated, easy-to-understand modules. Even with that model of development, it is still difficult to ensure that the total state of the system (such as a rocket during launch) will not enter into some odd combination of circumstances that we could never predict. We are not talking here about the evil global variable. We are talking about a real system in which the complexity requires multiple engineers who must communicate with each other and whose communication must make sense in terms of the total product. Assertions are not enough. More important than the assertion is what to do if the assertion fails. Often, we don't know what to do. Again, Mr. Garlington laid out a list of common responses to failure, but there is no gurarantee we have selected the correct response. No assertion can guarantee that the state to which we transition upon failure will be the correct new state. Someone suggested an assertion based on some timing constraint. That, of course, would be very bad news. The timing for different platforms will vary. Instead, the assertion would be based on the current state of the module currently completing its operation, the postcondition along with the state of the new module (precondition) into which it intended to transition. I raise this point because it is not always clear how to declare an assertion for a component. The Arianne IV component might have had a perfectly reasonable "contract" based on its own timing mechanisms and could have failed to protect Arianne V. Remember, assertions are checked at run-time, not at compile-time. At run-time, in a hard-deadline, real-time system, there is very little time for the OOPS! factor. Both the Ada and Eiffel contributors to this discussion are endowed, I fear, with an excess of hubris. We are so enamoured with our own notions of how to provide software excellence that we oversimplify the real issues related to this kind of software product. Eventually, Design By Contract, along with theorem provers and other advances in computer science will move us all more in the direction of more reliable software, but it is not a finished idea yet. It is a step in the right direction. Many of the ideas in Ada will get better, and eventually Ada (as in the SPARK Examiner model already in place) will benefit from Design by Contract. At present, SPARK is probably the best example of Design By Contract, but it is so conservative in its acceptance of contemporary ideas in object-oriented programming that many practitioners are reluctant to be so constrained. One hundred years from now, those of our successors developing the equivalent of computer software will look back on our arguments with the same admiration we have for the mathematicians in the time of Charlemagne. Arianne V was a big mistake that neither Eiffel nor Ada would have prevented. Let's get on with learning how to make things work instead of beating up on each other about how much better we are than the other guy. Richard Riehle richard@adaworks.com