Software Engineering, International Conference on (1996)
Mar. 25, 1996 to Mar. 29, 1996
K.K. Dhara , Dept. of Comput. Sci., Iowa State Univ., Ames, IA, USA
G.T. Leavens , Dept. of Comput. Sci., Iowa State Univ., Ames, IA, USA
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 pearls 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++.
message passing; object-oriented programming; formal specification; inheritance; behavioral subtyping; specification inheritance; object-oriented software; message passing; code reverification; inheritance; C++
G. Leavens and K. Dhara, "Forcing behavioral subtyping through specification inheritance," Software Engineering, International Conference on(ICSE), Berlin, GERMANY, 1996, pp. 258.