archives

Behavioral Subtyping, Specification Inheritance, and Modular Reasoning


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Leavens, Gary T. and Naumann, David A. (2006) Behavioral Subtyping, Specification Inheritance, and Modular Reasoning. Technical Report TR06-20, Computer Science, Iowa State University.

Full text available as:Adobe PDF
Postscript

There is a later version of this eprint available: Click here to view it.

Abstract

Behavioral subtyping is an established idea that enables modular reasoning about behavioral properties of object-oriented programs. It requires that syntactic subtypes are behavioral refinements. It validates reasoning about a dynamically-dispatched method call, say E.m(), using the specification associated with the static type of the receiver expression E. For languages with references and mutable objects the idea of behavioral subtyping has not been rigorously formalized as such, the standard informal notion has inadequacies, and exact definitions are not obvious. This paper formalizes behavioral subtyping and supertype abstraction for a Java-like sequential language with classes, interfaces, exceptions, mutable heap objects, references, and recursive types. Behavioral subtyping is proved sound and semantically complete for reasoning with supertype abstraction. Specification inheritance, as used in the specification language JML, is formalized and proved to entail behavioral subtyping.

Keywords:Behavioral subtyping, supertype abstraction, specification inheritance, modularity, specification, verification, state transformer, dynamic dispatch, invariants, Eiffel language, JML language.
Subjects:Software: PROGRAMMING TECHNIQUES (E): Object-oriented Programming
Software: SOFTWARE ENGINEERING (K.6.3): Requirements/Specifications (D.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Coding Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Software: SOFTWARE ENGINEERING (K.6.3): Distribution, Maintenance, and Enhancement
Software: PROGRAMMING LANGUAGES: Formal Definitions and Theory (D.2.1, F.3.1-2, F.4.2-3)
ID code:00000436
Deposited by:Gary T. Leavens on 21 July 2006
Alternative Locations:ftp://ftp.cs.iastate.edu/pub/techreports/TR06-20/TR.pdf ftp://ftp.cs.iastate.edu/pub/techreports/TR06-20/TR.ps.gz

Available Versions of This Paper



Contact site administrator at: ssg@cs.iastate.edu