Leavens, Gary T. (1990) Reasoning About Object-Oriented Programs That Use Subtypes. Technical Report TR90-03, Department of Computer Science, Iowa State University.
Reasoning about Object-Oriented Programs that use Subtypes (Extended Abstract)
Gary T. Leavens and William E. Weihl
Programmers informally reason about object-oriented programs by using
subtype relationships to classify the behavior of objects of different
types and by letting supertypes stand for all their subtypes.
We describe formal specification and verification techniques for such
programs that mimic these informal ideas. Our techniques are modular
and extend standard techniques for reasoning about programs that use
abstract data types. Semantic restrictions on subtype relationships
guarantee the soundness of these techniques.
Contact site administrator at: firstname.lastname@example.org