Xref: utzoo comp.lang.eiffel:521 comp.object:600
Path: utzoo!attcan!utgpu!jarvis.csri.toronto.edu!mailrus!uunet!mcsun!unido!laura!exunido!guendel
From: guendel@exunido.uucp (Andreas Guendel)
Newsgroups: comp.lang.eiffel,comp.object
Subject: Re: Eiffel, assertions, Object-Z and library books.
Keywords: eiffel, assertions, object-z
Message-ID: <1818@laura.UUCP>
Date: 8 Dec 89 14:16:52 GMT
Sender: news@laura.UUCP
Reply-To: guendel@exunido.UUCP (Andreas Guendel)
Organization: University of Dortmund, W-Germany
Lines: 40

In article 526 of comp.object Paul Johnson asks:

> 1) Are Z and Software Contracting incompatable?

> To be a valid instance of a type {member of a Z schema}, an item must
> fulfil all assertions {predicates}.  This means that for "A" and "B"
> above, a member of "B" must fulfil all the assertions of "A",
> otherwise it is not of type "A".  However, in Eiffel, the Rule of
> Assertion Redefinition (OOSC section 11.1.4) says that preconditions
> can be weakened, following the principle of software contracting.
> This is intuitively obvious, but does not seem to fit into the "is-a"
> subset relationship described above.

Paul, you are missing something. The precondition of the Eiffel
software contracting does NOT itself build a predicate describing
an object. It is just a part of the composed predicate
`{precondition} action {postcondition}' known from Hoare-semantics
with the following meaning: Whenever `precondition' is fulfilled
the execution of `action' gives a situation where `postcondition'
holds.

If you think about this you will see that weakening the `precondition'
part really strengthens the composed predicate as needed semantically.

> 2) Are Multiple Inheritance and Software Contracting incompatable?

> Another example, taken from Meyer's seminar.  Suppose we have the
> classes PLANE and ASSET.  From these we derive COMPANY_PLANE.  A
> precondition for FLY in PLANE is to be a qualified pilot.  A
> precondition for USE in ASSET is to be a company employee.  Hence to
> fly a company airplane, you must be a company employed qualified
> pilot.  This strengthens the pre-conditions on both base classes.

We had a discussion about inheritance and the is-a relation in this
newsgroup before. Shortly spoken: If the precondition is strengthend
there is no subclass-relation semantically as the software contracting
rule shows. But this is not unique to multiple-inheritance, it may even
occur in single inheritance hierachies.

Andreas Guendel