paj@mrcu (Paul Johnson) (12/06/89)
This article poses two questions. They are:
1) Are Z and Software Contracting incompatable?
2) Are Multiple Inheritance and Software Contracting incompatable?
We have been looking at object-oriented extensions to Z (eg.
[CARRINGTON], [SCHUMAN]) as a way of describing object-oriented
systems, with a view to using this for Eiffel design. Unfortunately
we cannot find a way to describe Eiffel classes in terms of Z. In the
following I will use Eiffel terms with the Z terms in curly brackets.
The "is-a" relationship described by inheritance can be described
simply in Z by subsets: if we have a type {Z schema} "A" and then derive
a type "B" from "A" such that an instance {member} of "B" is-a
instance of "A", then we can say that "B" is a subset of "A".
Similarly multiple inheritance can be described by set intersection: if we
have types "P" and "Q", and "R" inherits from "P" and "Q" then "R" is
a subset of ("P" intersection "Q"). Any instance of "R" is also an
instance of "P" and an instance of "Q".
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.
It seems possible that pre-conditions can be considered to be
invarients on all clients (at least at the time when the call is
made). Has anyone else looked at this? Are we missing something, or
are Z and Software Contracting incompatable. If so, which one do we
drop?
Another problem can arise with multiple inheritance. Let us take a
specification with a class {schema} BOOK that has a feature READ.
BOOK has no predicates and READ just outputs a page:PAGE.
The library has a class {schema} BORROWABLE which has features
LOCATION (on_shelf, on_loan, on_table) and USE with a precondition
(NOT on_shelf). We now wish to define a class LIBRARY_BOOK which
inherits from BOOK and BORROWABLE and in which to READ a library book
you must USE it. This implies that READ must have the pre-condition
(NOT on_shelf) or the USE call within LIBRARY_BOOK.READ will fail.
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.
How do we solve this one? Are multiple inheritance and Software
Contracting incompatable?
Bibliography:
[CARRINGTON]: David Carrington, David Duke, Roger Duke, Paul King,
Gordon Rose, Graeme Smith: "Formal Specification in Object-Z:
Introduction and Case Studies", Dept of Computer Science, University
of Queensland. Tech report 105, July 1989.
[SCHUMAN]: S. Schuman, D. Pitt: "Object-Oriented Subsystem
Specification". University of East Anglia. Program Specification and
Transformation, L. Meertens (editor), Elsevier Science Publishers,
1987.
--
Paul Johnson.----------------------------------------------------------------
GEC-Marconi Research are not | Don't worry: Baldrick has a Cunning Plan!
responsible for my opinions. | (Graffiti on East side of Berlin Wall)
-----------------------------------------------------------------------------yh87@mrcu (Paul Johnson) (12/06/89)
The last message did not have my email address in. This one does. Sorry. Paul. -- Paul Johnson | Internet: paj@uk.co.gec-mrc | Phone: +44 245 73331 ext 3216 -------------!------------------.----------!------------------------------- GEC-Marconi Research is not | Don't worry: Baldrick has a Cunning Plan! responsible for my opinions. | (Graffiti on East side of Berlin Wall)
guendel@exunido.uucp (Andreas Guendel) (12/08/89)
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
db@lfcs.ed.ac.uk (Dave Berry) (12/21/89)
In article <1818@laura.UUCP> guendel@exunido.UUCP (Andreas Guendel) writes: >In article 526 of comp.object Paul Johnson asks: >> 2) Are Multiple Inheritance and Software Contracting incompatable? > >> 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. > >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. I can see how Andreas' position applies to single-inheritance hierarchies. I can't see how it answers the multiple-inheritance example given by Paul Johnson. Surely a company plane *is* both an asset and a plane? This applies both conceptually and practically; in practice one might want to add the company_plane to a list of company assets and to a list of planes. If one accepts Andreas' position, how should this example be implemented? Dave Berry, Laboratory for Foundations db%lfcs.ed.ac.uk@nsfnet-relay.ac.uk of Computer Science, Edinburgh Uni. <Atlantic Ocean>!mcvax!ukc!lfcs!db "leIsANewEntertainment:GuerillaWarStruggleIsANewEntertainment:GuerillaWarStrug"
guendel@exunido.uucp (Andreas Guendel) (12/22/89)
In article <288@oasis.mrcu> Paul Johnson asked: > Are Multiple Inheritance and Software Contracting incompatable? > 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. In article <1818@laura.UUCP> I answered: > If the precondition is strengthend there is no subclass-relation semantically > as the software contracting rule shows. In article <1469@castle.ed.ac.uk> Dave Berry responded: > I can see how Andreas' position applies to single-inheritance hierarchies. > I can't see how it answers the multiple-inheritance example given by Paul > Johnson. Surely a company plane *is* both an asset and a plane? This applies > both conceptually and practically; in practice one might want to add the > company_plane to a list of company assets and to a list of planes. > If one accepts Andreas' position, how should this example be implemented? Well, you are right Dave. Taking a rigid theoretical position does by itself not help in a concrete example. Thus, here is an attempt to clarify the example. If you want a companys assets include complex things like a company_plane, you have to take care while defining the class ASSET. Obviously, not any employee may USE each of a companys assets. Why? There might be some in-house legitimation scheme and, at least I hope so, some condition on the employees qualification. In the special case of the subclass company_plane this will be: qualified pilot! If you want to model planes in a section of reality that includes ownership relations, you have to take care while defining the class PLANE. Obviously, not any qualified pilot may FLY each existing plane. Why? He needs the legitimation from the owner of the plane. In the special case of the subclass company_plane this will be: beeing an employee. Summary: In OO-Programming it is not the main problem to build new subclasses of (multiple) superclasses, but to create reusable, extendable classes which model entities in a coherent section of reality. These classes will hopefully allow for semantically correct sub- classing (even with multiple inheritance) later on. Hope this helps, Andreas Guendel