论文部分内容阅读
现代构件系统通常包含多个并发执行的主动构件，这使得验证构件系统的正确性变得十分困难，通过对构件演算进行扩展，提出了一种主动构件的精化方法，在构件接口层引入契约，契约使用卫式设计描述公共方法和主动活动的功能规约，通过一对发散，失败集合定义契约的动态行为，并利用发散，失败集合之间的包含关系定义契约间的精化关系，证明了应用仿真技术确认契约精化关系的定理，定义构件的语义为其需求接口契约到其服务接口契约的函数，以此为基础，可以通过契约的精化来证明构件的精化，给出了构件的组装规则，在构件系统自底向上的构造过程中，应用