所有权约束保证面向对象程序的表示独立性
Ownership Confinement Ensures Representation Independence for Object-Oriented Programs
摘要：
献给Edsger W. Dijkstra的记忆。表示独立性或关系参数化形式上表征了数据抽象语言结构提供的封装，并证明了模拟推理的合理性。表示独立性已经在各种语言和构造中得到了证明，但在对可变状态的共享引用中却没有;事实上，它在这些语言中通常是失败的。本文阐述了表示类的独立性，在一个命令式的，面向对象的语言与指针，子类化和动态调度，面向类的可见性控制，递归类型和方法，以及一个简单的模块形式。类的实例被认为是使用私有字段和所谓的表示对象来实现抽象。表示对象的封装通过对别名的限制（称为限制）来表示。证明了满足约束条件的程序的表示独立性。一个静态分析，接受常见的设计，如观察者和工厂模式的限制。形式化不仅考虑了客户端和提供抽象的类之间的通常接口，还考虑了类和它的子类之间的接口（通常称为“受保护的”）。
英文摘要：
Dedicated to the memory of Edsger W.Dijkstra. Representation independence or relational parametricity formally characterizes the encapsulation provided by language constructs for data abstraction and justifies reasoning by simulation. Representation independence has been shown for a variety of languages and constructs but not for shared references to mutable state; indeed it fails in general for such languages. This paper formulates representation independence for classes, in an imperative, object-oriented language with pointers, subclassing and dynamic dispatch, class oriented visibility control, recursive types and methods, and a simple form of module. An instance of a class is considered to implement an abstraction using private fields and so-called representation objects. Encapsulation of representation objects is expressed by a restriction, called confinement, on aliasing. Representation independence is proved for programs satisfying the confinement condition. A static analysis is given for confinement that accepts common designs such as the observer and factory patterns. The formalization takes into account not only the usual interface between a client and a class that provides an abstraction but also the interface (often called ``protected'') between the class and its subclasses.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
