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 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, <bertrand@eiffel.com> -
ftp://ftp.eiffel.com
Visit our Web page: http://www.eiffel.com
	(including instructions to download Eiffel 4 for Windows)