对象共享是面向对象程序中许多基本设计技术的基础，给软件开发带来很大方便。然而，没有任何约束的共享很难控制，所引起的别名问题给系统的安全带来极大的隐患。对象可以通过它的任何一个别名来修改，因此面向对象程序的行为很难预测、分析、及维护。对象封装是面向对象程序设计中最基本的和必需的要求。它将受保护的对象封装在安全的范围内，从而禁止外部对象对它们的直接访问。 常规的面向对象语言提供的访问控制机制仅仅是一种静态的可见性控制机制，它并不提供对程序运行时的对象的访问控制，从而不能支持对象的封装。近年来，人们提出了许多封装框架来增强现有面向对象语言对于对象封装的支持。其中大多数是静态封装框架，通过设计能够实现封装需求的类型系统来保证动态的对象封装。这种类型系统的实现完全是静态的，可以自动检查的。然而，静态封装框架往往语法限制太强，从而排除了一些本来封装行为良好的常见程序模式：或者语法标注太复杂，一般用户很难写出符合自己封装意愿的程序。而且，不同的静态封装框架的设计复杂多样，相互之间没有本质上的联系，导致用户难以正确地选择和使用。由于面向对象语言语义的复杂性，研究中提出的语义封装框架还很少。仅有的一个语义封装框架仍然借助于许多语法限制，并且只描述了一种特殊的封装需求。而另一个描述一般对象封装的模型仅停留在初步研究阶段，无实用价值。 本论文主要建立了面向对象程序中的对象封装的语义模型和性质，定义了能够描述封装限制的封装分离逻辑。该语义封装模型以一个典型的顺序面向对象语言μJaVa为基础语言，不依赖于任何语法上的封装限制，并且支持多样化的封装需求。基于堆的划分和封装限制条件，定义了良封装状态、良封装命令及良封装程序等概念。 论文中深入研究了语义封装模型的封装性质。一方面，基于μJava研究了面向对象语言中的各种命令的执行对对象封装的影响，即命令在何种情况下会导致封装的泄露。这些一般的性质能帮助程序员理解如何编写良封装的程序，尽可能地避免封装泄露。另一方面，文中给出并证明了能够局部判断程序封装的局部性定理。该定理说明在满足一定的清晰定义的条件的基础上，只需要检查程序中部分代码的行为，就可以确定整个程序是否为良封装的。该局部性定理还允许程序以类为单位进行扩展，只要扩展的类不增加新的封装需求，扩展后的程序仍能保持良封装性。这些性质可以简化对大型程序良封装性的验证。 为了体现语义封装模型的理论价值，文中形式地刻画了几个重要的封装实例，其中包括JavaJDK1.1.1中Class类实现的签名泄露问题，以及两种典型的静态封装框架：私有封装类和拥有者类。从中可以看出本文提出的语义封装模型的一般性。对于它们在语义封装模型中的形式化，文中都分别用直接定义和局部性定理两种方式来验证它们的封装性质。 本论文还提出了能够描述封装限制条件的封装分离逻辑。它以分离逻辑为基础，加入了描述封装限制的新的运算符。文中已建立了封装分离逻辑的关系模型，并且运用point-free技术，利用关系演算的推理系统，推理得到了封装分离逻辑的公理性质。从而为建立封装分离逻辑的公理系统奠定了基础。 本论文最后探讨了进一步的研究工作。其中包括封装分离逻辑的证明系统的完善，封装规范的描述，语义封装模型对其他别名控制技术的应用，及良好静态封装框架的构建等。