Xref: utzoo comp.lang.eiffel:519 comp.object:583 Path: utzoo!attcan!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!ukc!stc!root44!hrc63!mrcu!paj From: paj@mrcu (Paul Johnson) Newsgroups: comp.lang.eiffel,comp.object Subject: Eiffel, assertions, Object-Z and library books. Keywords: eiffel, assertions, object-z Message-ID: <288@oasis.mrcu> Date: 5 Dec 89 17:03:29 GMT Organization: GEC-Marconi Research Centre, Great Baddow, UK Lines: 75 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) -----------------------------------------------------------------------------