Modular specification and verification of object-oriented programs
- 1 July 1991
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Software
- Vol. 8 (4) , 72-80
- https://doi.org/10.1109/52.300040
Abstract
A method for modular specification and verification using the ideas of subtype and normal type is presented. The method corresponds to informal techniques used by object-oriented programmers. The key idea is that objects of a subtype must behave like objects of that type's supertypes. An example program is used to show the reasoning problems that supertype abstraction may cause and how the method resolves them. Subtype polymorphism is addressed, and specification and verification update is discussed. A set of syntactic and semantic constraints on subtype relationships, which formalize the intuition that each object of a subtype must behave like some object of each of its supertypes, is examined. These constraints are the key to the soundness of the method. To state them precisely, a formal model of abstract type specifications is used.Keywords
This publication has 7 references indexed in Scilit:
- Reasoning about object-oriented programs that use subtypesACM SIGPLAN Notices, 1990
- How to make ad-hoc polymorphism less ad hocPublished by Association for Computing Machinery (ACM) ,1989
- Encapsulation and inheritance in object-oriented programming languagesACM SIGPLAN Notices, 1986
- A Larch Shared Language handbookScience of Computer Programming, 1986
- The Larch Family of Specification LanguagesIEEE Software, 1985
- Using category theory to design implicit conversions and generic operatorsPublished by Springer Nature ,1980
- Proof of correctness of data representationsActa Informatica, 1972