所有权限制确保面向对象程序的表示独立性
摘要：专为Edsger W.Dijkstra的记忆而设。 表示独立性或关系参数性形式上描述了语言构造提供的数据抽象封装，并且证明了通过模拟进行推理的合理性。表示独立性已经在各种语言和构造中得到证明，但对于对可变状态的共享引用尚未得到证明；事实上，对于这样的语言，一般来说表示独立性是不成立的。本文在一种具有指针、子类化和动态调度、类导向的可见性控制、递归类型和方法以及一种简单形式的模式的命令式面向对象语言中对类进行了表示独立性的形式化。一个类的实例被认为是使用私有字段和所谓的表示对象来实现抽象的。表示对象的封装通过一种叫做约束的限制来表达，该限制限制了别名。对于满足约束条件的程序，证明了表示独立性。给出了约束的静态分析，接受了常见的设计，如观察者和工厂模式。规范化考虑了客户端与提供抽象的类之间的通常接口，但也考虑了类与其子类之间的接口（通常称为``保护''）。
作者：Anindya Banerjee (1), David A. Naumann (2) ((1) Kansas State University, (2) Stevens Institute of Technology)
论文ID：cs/0212003
分类：Programming Languages
分类简称：cs.PL
提交时间：2007-05-23