The verification of object-oriented programs and programs with exception handling constructs.

摘要

This is a masters thesis on the verification of object-oriented programs. An object-oriented mini-language and proof system are constructed. Polymorphism, one of whose characteristics is the ability to assign objects of more than one type to a given variable, is a major feature in this mini-language. Class specifications are introduced as a tool for verifying properties of classes within a program. Specifications for classes are especially valuable in the verification of reusable classes. Another problem that is addressed is how a specification for a class B can be derived from a valid specification for another class A given that B inherits from A. A second mini-language and proof system are introduced for the verification of programs with exception handling constructs. Assertion violations and expression exceptions are some of the exceptions considered. Paper copy at Leddy Library: Theses u26 Major Papers - Basement, West Bldg. / Call Number: Thesis1995 .B590. Source: Masters Abstracts International, Volume: 34-02, page: 0783. Adviser: Liwu Li. Thesis (M.Sc.)--University of Windsor (Canada), 1995.