archives

Behavioral Subtyping is Equivalent to Modular Reasoning for Object-oriented Programs


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Leavens, Gary T. and Naumann, David A. (2006) Behavioral Subtyping is Equivalent to Modular Reasoning for Object-oriented Programs. Technical Report 06-36, Computer Science, Iowa State University.

Full text available as:Adobe PDF
Postscript

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 and the standard informal notion has inadequacies. This paper formalizes behavioral subtyping and introduces a new formalization of modular reasoning, called supertype abstraction. A Java-like sequential language is considered, with classes and interfaces, recursive types, first-class exceptions and handlers, and dynamically allocated mutable heap objects; the semantics is designed to serve as foundation for the Java Modeling Language (JML), a widely used specification language. Behavioral subtyping is characterized as sound and semantically complete for reasoning with supertype abstraction.

Keywords:Behavioral subtyping, modular reasoning, object-oriented programming, recursive types, denotational semantics, functional specification, Java Modeling Language (JML).
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): Design Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Software/Program Verification (F.3.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Semantics of Programming Languages (D.3.1)
Theory of Computation: LOGICS AND MEANINGS OF PROGRAMS: Studies of Program Constructs (D.3.2-3)
ID code:00000496
Deposited by:Gary T. Leavens on 22 December 2006
Alternative Locations:ftp://ftp.cs.iastate.edu/pub/techreports/TR06-36/TR.pdf ftp://ftp.cs.iastate.edu/pub/techreports/TR06-36/TR.ps.gz



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