Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Modular Reasoning in Object-Oriented Systems
Object-oriented languages are growing in popularity due to the benefits
they provide in modeling, encapsulation, reuse, and evolvability.
However, reasoning about the properties of object-oriented systems can
be challenging for many of the same reasons that give objects their
power. Inheritance enables extensive reuse, but also couples a
class to its superclass, making it hard to evolve the two
independently. Objects and state are natural mechanisms for modeling
many problem domains, but reasoning about multi-object, stateful
systems in a modular way is difficult because of aliasing.
The goal of this project is to build a foundational theory as well as
practical tools for reasoning about object-oriented software systems in
a modular way. Modular reasoning is important because programmers
can think about the correctness of different modules in isolation, as
well as make changes to the implementation of a module without
affecting clients. We propose to address the challenge of modular
reasoning in part with the following techniques:
We will use a richer notion of protected interface in order to
decouple a class from its subclasses. The goal of the interface
is to expose only the semantics of a class to its subclasses, so that
any semantics-preserving change to the implementation of the class's
protected interface can be made without affecting subclasses.
We will use new techniques in ownership type systems and
separation logic to reason about a subsystem of objects in isolation
from the outside world. The main challenge will be providing the
strong encapsulation necessary for separate reasoning about properties
without compromising the rich interactions between objects that give
object-oriented programming its power.
As a first step towards these goals, we have developed ownership
domains, an extension of ownership type systems that supports powerful
reasoning about encapsulation while retaining the flexibility necessary
to support many object-oriented styles and idioms. This work is
described by the paper below. Our
long-term goal is to develop a comprehensive proof theory for
object-oriented systems, along with tools and type systems that aid in
both lightweight reasoning and full verification of programs.