Barbara H. Liskov
Jeannette M. Wing
Abstract
The use of hierarchy is an important component of object-oriented design. Hierarchy allows the use of type families, in which higher level supertypes capture the behavior that all of their subtypes have in common. For this methodology to be effective, it is necessary to have a clear understanding of how subtypes and supertypes are related. This paper takes the position that the relationship should ensure that any property proved about supertype objects also holds for its subtype objects. It presents two ways of defining the subtype relation, each of which meets this criterion, and each of which is easy for programmers to use. The subtype relation is based on the specifications of the sub- and supertypes; the paper presents a way of specifying types that makes it convenient to define the subtype relation. The paper also discusses the ramifications of this notion of subtyping on the design of type families.
- AMERICA, P. 1990. A parallel object-oriented language with inheritance and subtyping. SIC_I- PLAN 2,5, 10 (Oct.), 161-168. Google Scholar
- AMERICA, P. 1991. Designing an object-oriented programming language with behavioural subtyping. In J. W. DE BA~KSa, W. P. DE ROEVEa, AND G. ROZENBEaC (Eds.), Foundations of Objcct-Or~e~ted Languages, REX School~Workshop, Noord~z, Ut~'erho~Lt, The Netherlands, Ma!//June 1990, Volume 489 of ~NCS, pp. 60-90. NY: Springer-Verlag. Google Scholar
- BLACK, A. P., HUTCHINSON, N., JUL, E., LEVY, H. M., AND CARTER, L. 1987". Distribution and abstract types in Emerald. IEEE TSE i3, 1 (Jan.), 65-76. Google Scholar
- BRUCE, K. aND WP, GNER, P. 1990. An algebraic model of subtype and inheritance. In F. BAN- CILHON AND P. BUNEMAN (Eels.), Advances ia Database Program'mtng Lang~age, pp. 75-96. Addison-Wesley, Reading, MA. Google Scholar
- CARDELLI, L. 1988. A semantics of multiple inheritance. Information and Cornp~Ltat~on 76, 138-164. Google Scholar
- CARRINGTON, D., DUKE, D., DUKE, R., KING, P., RosE, G.,, AND SMITH, t). 1989. Object- Z: An object oriented extension to Z. In FOi~TE89, I~z~eTr~a~onal Co~}ere~c~ on Format Descrzpt~on Tech'nTq~Les. Google Scholar
- CUSACt<, E. 1991. Inheritance in object oriented Z. In Proceedings of ECOOP '91. Springer- Verlag. Google Scholar
- CUSACK, E. AND LAI, l~I. 1991. Object-oriented specification in LOTOS and Z, or my cat really is object-oriented! In J. W. DE BAK~<ER, W. P. DE ROEVER, AND G. R~ZP, NBEaG (Eds.), Foundations of Ob2ect Ortented Languages, pp. 179-202. Springer Verlag. LNCS 489. Google Scholar
- DAHL, O.-J., MYRHAUG, B., AND NVGAARD, K. 1970. SIMULA common base language. Technical Report 22, Norwegian Computing Center, Oslo, Norway.Google Scholar
- DHARA, I(. K. 1992. Subtyping among mutable types in object-oriented programming languages, Iowa State University, Ames, Iowa. l~iaster's Thesis.Google Scholar
- DHARA, K. K. AND LEAVENS, (J. T. 1992. Subtyping for mutable types in object-oriented programming languages. Technical Report 92-36 (Nov.), Department of Computer Science, Iowa State University, Ames, Iowa.Google Scholar
- DUb:E, D. AND DUXE, R. 1990. A history model for classes in object-Z. In Proceedings of VDtlI '90: VDilI and Z. Springer-Verlag.Google Scholar
- GARLAND, S. AND GUTTAG, J. 1989. An overview of LP, the Larch Prover. In Proceedzngs of the Thzrd Internat~o',~at Confere',~ce on Rewriting Technzq~es and Apphcaf~ons, Chapel Hill, NC, pp. 137-151. Lecture Notes in Computer Science 355. Google Scholar
- (~OGUEN, J. A. AND MESEGUER, J. 1987. Unifying functional, object-oriented and relational programming with logical semantics. In B. SHNIVER AND P. V~rEGNER (Eds.), Research D~rect~o~zs ~a Ob2ect O'r~e'atcd Prog~'a'mm~n9. MIT Press. Google Scholar
- GUTTAG, J. V., HOaNING, ff J., AN~, W~NG, J. M. 1985. The Larch family of specification lansuases. IEEE ,~oftcc.a,'e ~, 5 (Sept), 2 t-36.Google Scholar
- HALBERT, D. C. AND O'BRIEN, P. m. 1987. Using types and inheritance in object-oriented programming. IEEE Software 4, 5 (Sept.), 71-79.Google Scholar
- HAMMER, M. AND McLEoD, D 1981. A semantic database model. ACM Traus. Database Syst z'rns 6, 3, 351-386. Google Scholar
- HOARE, C. 197"2. Proof of correctness of data representations. Acta Infor~zatzca 1, 1, 271-281.Google Scholar
- KApUR, D. 1980. Towards a theory of abstract data type~. Technical Report 237" (June), MIT LCS. Ph.D. Thesis. Google Scholar
- LEAVENS, G. 1989. Verifying object-oriented prograsm that use subtypes. Technical Report 439 (Feb.), MIT Laboratory for Computer Science. Ph.D. thesis.Google Scholar
- LEAVENS, G. T. 1991. Modular specification and verification of object-oriented programs. IEEE Software 8, 4 (July), 72-80. Google Scholar
- LEAVENS, G. T. AND DHARA, K. K. 1992. A foundation for the model theory of abstract data types with mutation and aliasing (preliminary version). Technical Report 92-35 (Nov.), Department of Computer Science, iowa State University, Ames, Iowa.Google Scholar
- LEAVENS, G. T. AND WEIHL, W. E. 1990. Reasoning about object-oriented programs that use subtypes. In ECOOP/OOPSLA '90 Proceedings. Google Scholar
- LIPECK, U. 1992. Semantics and usage of defaults in specifications. In Foundations of {nformatzon Systems Spec~ficahon and Design. Dagstuhl Seminar 9212 Report 35.Google Scholar
- LisKov, B. }992. Preliminary design of the Thor object-oriented database system. In Proc. of the Software Technology Conference. DARPA. Also Programming Methodology Group Memo 74, MIT Laboratory for Computer Science, Cambridge, MA, March 1992.Google Scholar
- LISKOV, B., ATKINSON, R., BLOOM, T., hiOSS, E., SCHAFFERT, J., SCHEIFLER, R., AND SNYDER, A. 1981. CLU Reference A~r~nual. Springer-Verlag. Google Scholar
- LIsKov, B. AND GUTTAG, J. 1985. Abstraction and Specification in Program Deszgn. MIT Press. Google Scholar
- LISKOV, B. AND WING, J. 1992. Family values: A semantic notion of subtyping. Technical Report 562, MtT Lab. for Computer Science. Also available as CMU-CS-92-220. Google Scholar
- MAIER, D. AND STEIN, J. } 990. Development and implementation of an object-oriented DBMS. In S. ZDONIK AND D. ~{AIEB (Eds.), Read~gs in Object-Oriented Database Systems, pp. 167-185. Morgan Kaufmann. Google Scholar
- MEYEa, B. 1988. Ob3eci-oriented Software Consfruction. Prentice Hall, New York. Google Scholar
- MORGAN, C. 1990. Programming from Specifications. Prentice Hall. Google Scholar
- NELSON, G. 1991. Systems Prograrnmin9 w~th Moduta-3. Prentice Hall. Google Scholar
- SCHA~PEaT. C. COOPER, T., BULLIS, B., KILIAN, M., AND WILPOLT, C. 1986. An introduction to Trellis/Owl. In Proceedings of OOPSLA '86, pp. 9-16. Google Scholar
- SCHEID. J. AND HOLTSBERG, S. 1992. Ina Jo specification language reference manual. Technical Report TM-6021/001/06 (June), Paramax Systems Corporation, A Unisys Company.Google Scholar
- STROUSTRUP, B. 1986. The C-t--t- Programming Language. Addison-Wesley. Google Scholar
- UTTING, M. 1992. An object-oriented refinement calculus with modular reasoning. Ph. D. thesis, University of New South Wales, Australia. Google Scholar
- WING, J. M. 1983. A two-tiered approach to specifying programs. Technical Report 299 (June), MIT I~aboratory for Computer Science. Ph.D. thesis. Google Scholar
Index Terms
- A behavioral notion of subtyping
Recommendations
Unifying typing and subtyping
In recent years dependent types have become a hot topic in programming language research. A key reason why dependent types are interesting is that they allow unifying types and terms, which enables both additional expressiveness and economy of concepts. ...
Subtyping delimited continuations
ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programmingWe present a type system with subtyping for first-class delimited continuations that generalizes Danvy and Filinski's type system for shift and reset by maintaining explicit information about the types of contexts in the metacontext. We exploit this ...
Matching MyType to subtyping
The notion of MyType has been proposed to promote type-safe reuse of binary methods and recently extended to mutually recursive definitions. It is well known, however, that MyType does not match with subtyping well. In current type systems, type safety ...
Reviews
Tsun-Him Tse
Subtyping, also known informally as inheritance, is an important notion in object-oriented programming, but may lead to unexpected problems if not handled properly. In order to ensure that intrinsic properties are preserved during the process of subtyping, Liskov and Wing propose two approaches. First, a constraint approach directly specifies history properties in terms of constraints, which provides the criteria to ensure that every method in the subtype preserves the properties of the supertype. Second, an extension approach specifies that the observable behaviors of every new method in the subtype must agree with the original methods of the supertype. This in turn ensures that history properties are preserved. Liskov and Wing discuss these two approaches in detail with respect not only to constraint and extension rules, but to invariant, signature, and methods rules. I have two observations. First, can the rules discussed in this paper be compatible with overriding__?__ For example, can we identify a set of rules that will help us preserve the desirable properties of the supertype, while avoiding the undesirable properties__?__ Second, I do not think the authors should claim that theirs is “the first work to deal with history properties.” For example, Cusack studied the history properties of inheritance in terms of traces, failures, and divergences in a communicating sequential processes<__?__Pub Caret> (CSP) context [1]. I enjoyed reading this paper. Numerous convincing examples are given to illustrate the arguments. The paper should be read not only by researchers but also by programmers who may not normally concur with the usefulness of formal methods.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments