Re: Papers on the Ariane-5 crash and Design by Contract

[Bertrand Meyer <bertrand@eiffel.com>]

Is it ever possible  to have a technical discussion without
resorting to insults? Jon S. Anthony finds it productive to write,
about one of my earlier messages:

> Do you have any idea how ridiculous this sort of statement makes you
> look???

He adds for good measure 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 lower-level programming language devoid of
	those concepts, make the tough decisions, rightly or not,
	consciously or not, and without an automatic feedback
	into the analysis and design.)

        (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, Now_married
        and Dead, and we have an invariant clause stating that
        `married = (status = Now_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 property `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, as expressed by
	its precondition and postcondition.)


 
-- 
Bertrand Meyer, President, ISE Inc., Santa Barbara (California)
805-685-1006, fax 805-685-6869, <bertrand@eiffel.com> -
ftp://ftp.eiffel.com
Visit our Web page: http://www.eiffel.com
	(including instructions to download Eiffel 4 for Windows)