Dhara, Krishan K. and Leavens, Gary T. (1995) Forcing Behavioral Subtyping Through Specification Inheritance. Technical Report TR95-20a, Department of Computer Science, Iowa State University.
Forcing Behavioral Subtyping Through
K. Kishore Dhara and Gary Leavens
A common change to object-oriented software is to add a
new type of data that is a subtype of some existing type in
the program. However, due to message passing unchanged parts
of the program may now call operations of the new type.
To avoid reverification of unchanged code, such operations should
have specifications that are related to the specifications of the
appropriate operations in their supertypes. This paper presents
a specification technique that uses inheritance of specifications
to force the appropriate behavior on the subtype objects. This
technique is simple, requires little effort by the specifier, and
avoids reverification of unchanged code. We present two notions of
such behavioral subtyping, one of which is new. We show how to use
these techniques to specify examples in C++.
Contact site administrator at: email@example.com