The Object-Oriented (OO) approach to system development has proven enormously useful since it allows designers to build new systems by reusing large parts of existing systems. This incremental style of system building is ideally suited for building systems which must constantly evolve to meet changing requirements. But to build a reliable system, designers must be able to reason about its behavior, and unfortunately, methods for reasoning about OO systems, in particular reasoning incrementally about such systems, are lacking. This dissertation addresses this deficiency by developing reasoning techniques which allow designers, in the process of reasoning about the behavior of a modified system, to reuse reasoning that has been performed about the original system. These techniques are an example of applying the OO philosophy of reuse, not simply to the design and coding tasks, but to the reasoning task as well.;Specifically, this dissertation develops a specification and reasoning method for OO classes, which allows a derived class designer, in the process of verifying that her class meets its specification, to reuse the reasoning performed by the base class designer in the corresponding task for the base class. Self-referential polymorphic methods are specified in such a way that the derived class designer can reason about the richer properties exhibited by such methods in the derived class without re-analyzing the code of the methods. This dissertation introduces a small OO language with a formal operational model, and proves that the formal rules which make up the aforementioned reasoning method are sound and relatively complete. A separate reasoning method is introduced to allow designers to reason about the richer behavior exhibited by client code in the presence of derived class objects. Finally, a specification and reasoning method is introduced for dealing with OO exception mechanisms.
展开▼
