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,a48e5b99425d742a X-Google-Attributes: gidfac41,public X-Google-Thread: ffc1e,a48e5b99425d742a X-Google-Attributes: gidffc1e,public X-Google-Thread: f43e6,a48e5b99425d742a X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,a48e5b99425d742a X-Google-Attributes: gid103376,public X-Google-Thread: 1108a1,5da92b52f6784b63 X-Google-Attributes: gid1108a1,public From: Bertrand Meyer Subject: Re: Papers on the Ariane-5 crash and Design by Contract Date: 1997/03/22 Message-ID: <333438B5.ABD322C@eiffel.com> X-Deja-AN: 227582662 References: <332B5495.167EB0E7@eiffel.com> Organization: Interactive Software Engineering Inc. Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.programming.threads,comp.lang.ada Date: 1997-03-22T00:00:00+00:00 List-Id: Is it ever possible to have a technical discussion without resorting to insults? Jon S. Anthony finds it productive to write, about my earlier messages > Do you have any idea how ridiculous this sort of statement makes you > look??? further, that my comments are > extremely disappointing and make [me] look [again!] ridiculous. and that I am > just plain a) wrong or b) - well it doesn't take a genius to fill in > the obvious answer to this option. It is this type of gratuitous attack that empoverishes Usenet and has the potential to destroy it. When people who know what they are talking about, and could contribute usefully to the debate, see this kind of absurdity, they refrain from participating. Everyone loses. I assume Mr. Anthony's hope is that by making sufficiently outrageous statements he'll win by causing others either to lose their temper or to shut up in disgust. For me the latter will probably happen, but not yet. So let's see what he has to contribute. In response to my matter-of-fact statement that !!! The designers of these languages [i.e. Ada (83 or 95) and Java] !!! have explicitly rejected the inclusion of assertions he writes that > Ada _has_ assertions. Their form is not of the same syntactical look > as Eiffel's. So what? They take the form of constraints, in > particular (wrt to the case at hand) subtype constraints OK. Ada has assertions. Great news! I have read a lot about Ada but must have missed them. So let's see what their application would be to a typical example of Design by Contract. Take a class PERSON in a system for genealogical or demographical analysis. Here are some of the logical properties to be documented and enforced: - A person is married if and only if he or she has a spouse. - The spouse of a person's spouse is that person. - You cannot marry someone who is already married. - The gender of a person's spouse is not the same as that person's gender. (Note that this is consistent with the observation that we need at least three values for the gender: Male, Female and Unknown. We may be talking about processing a database with incomplete information.) I think we can accept these rules as part of the specification and stay away from facile jokes and individual opinions about the underlying topics (polygamy, same-sex marriages etc.). Just consider that this is a genealogical database for 19-th century England. Here is a quickly written sketch in Eiffel. I don't guarantee the exactness of the details since this is a 5-minute design, but the ideas should be clear. class PERSON feature -- Access gender: ... status: ... married: BOOLEAN -- Is person married? feature -- Element change marry (other: PERSON) is -- Get married to `other' . require available: not married other_exists: other /= Void other_not_married: not other.married different_gender: gender /= other.gender do ... ensure married: married married_to_other: spouse = other end ... Other features ... invariant married_iff_has_spouse: married = (spouse /= Void) married_to_spouse: married implies (spouse.spouse = Current) married_to_other_sex: married implies (gender /= spouse.gender) end (Some comments come up immediately, e.g. the assertions preclude a married couple with two "unknown" genders, suggesting that perhaps instead of expressions of the form `gender1 /= gender2' we should have a function same_gender (s1, s2). Or perhaps not. But this is precisely where the ideas of Design by Contract as implemented in Eiffel help you: they force you to ask the tough questions at the right time - class design -, not let a down-the-line implementer, writing in a low-level programming language devoid of those concepts, make the tough decisions, rightly or not, consciously or not.) (Also, `not married' is probably too weak; we may need a function `available_for_marriage' which is defined in terms of the status, e.g. if status can be Single, Divorced, Married and Dead, and we have an invariant clause stating that `married = (status = Married)', then `available_for_marriage' will mean Single or Divorced. Same comment as before: it's precisely by writing and refining assertions that we can get things right when it's still time. That's the idea in Eiffel. The above class sketch is only a first iteration.) I have purposely not filled the types for `status' and `gender', and the trivial properties that can be expressed by using enumeration types a la Pascal-Ada and range constraints, for example that `status' and `gender' can only take certain specified values. These are easy to add. Now if Ada has assertions, how would you express the above properties? (For anyone not familiar with Design by Contract: we are not talking about testing for abnormal cases, as in `if other.married then ... report error ...', nor even about Algol W/C/C++ `assert' instructions, as in `assert not other.married'. Instead, we are interested in associating with every software element - class or routine - a precise specification, or "contract", describing its obligations and benefits. The contract will serve as help in the analysis-design-implementation process (as briefly mentioned above), as documentation of the final software, as aid in debugging - by turning on run-time assertion monitoring in Eiffel environments -, as safeguard in using inheritance, as a basis for exception handling etc.) (The precondition of a routine, introduced by `require', states what must be true for the routine to be applicable; for example don't apply `marry' unless the reference `other' denoting the intended spouse is non-void, i.e. is attached to some object. The postcondition of a routine, introduced by `ensure', states the goals to be achieved by the routine; for example one of the results of `marry' is to make the boolean attribute `married' true. The invariant of a class expresses properties that will be satisfied at object creation time, and maintained by all routines of the class, e.g. a person is married if and only if he or she has a spouse - which places constraints on what such routines as `marry', `divorce' etc. can do; these constraints come on top of the routine's own specific constraints expressed by its precondition and postcondition.) -- Bertrand Meyer, President, ISE Inc., Santa Barbara (California) 805-685-1006, fax 805-685-6869, - ftp://ftp.eiffel.com Visit our Web page: http://www.eiffel.com (including instructions to download Eiffel 4 for Windows)