Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Behavioral subtyping, specification inheritance, and modular reasoning
Leavens G., Naumann D. ACM Transactions on Programming Languages and Systems37 (4):1-88,2015.Type:Article
Date Reviewed: Dec 15 2015

This is a long paper: 67 pages plus a 21-page appendix. It describes the verification of a dynamically dispatched method call of an object-oriented program by using supertype abstraction. The authors maintain that such abstraction is only valid when each subtype in the program is a behavioral subtype. The goal of this paper is to prove that behavioral subtyping is both necessary and sufficient for the validity of supertype abstraction. In order to do this, the authors semantically formalize supertype abstraction and behavioral subtyping for a Java-like sequential language.

The paper first provides a detailed formal definition of supertype abstraction and behavioral subtyping, followed by a section on related work. The Java-like language is then presented, followed by an overview of formal method specification, modular verification, and modular correctness, which is subsequently used to develop predicate transformer semantics.

Finally, behavioral subtyping and its equivalence to supertype abstraction are presented, along with how behavioral subtyping is ensured through specification inheritance and an adaption of the results to partial correctness. The appendix provides additional proofs and ancillary definitions.

The paper is well organized and presented with more than 80 references. It is intended for those doing serious object-oriented programming language research. The authors have at least 40 years of experience in this area and appear to be primarily addressing their peers (to which I can definitely recommend this work). However, graduate students should probably seek guidance from their advisors before attempting to read an advanced paper of this type.

Reviewer:  Donald Bagert Review #: CR144030 (1603-0207)
Bookmark and Share
  Editor Recommended
 
 
Object-Oriented Design Methods (D.2.2 ... )
 
 
Documentation (D.2.7 ... )
 
 
Formal Methods (D.2.4 ... )
 
 
Inheritance (D.3.3 ... )
 
 
Object-Oriented Languages (D.3.2 ... )
 
 
Object-Oriented Programming (D.2.3 ... )
 
  more  
Would you recommend this review?
yes
no
Other reviews under "Object-Oriented Design Methods": Date
Understanding UML: the developer’s guide
Harmon P., Watson M., Morgan Kaufmann Publishers Inc., San Francisco, CA, 1998. Type: Book (9781558604650)
May 1 1999
Advanced object-oriented analysis and design using UML
Odell J., Cambridge University Press, New York, NY, 1998. Type: Book (9780521648196)
Oct 1 1998
Object modeling and design strategies
Gossain S., Cambridge University Press, New York, NY, 1998. Type: Book (9780521648226)
Oct 1 1998
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy