论文部分内容阅读
本文采用演算的方式对余代数理论进行了研究，并将所得到的理论成果应用于构件化软件开发方法中。在本文中，提出了基于状态的类属化软件组件的余代数模型，并分别给出了两种相关的组件演算，这两种演算分别对应于对组件行为的不同抽象层次，具有各自的特点，同时两者又互相统一；本文在类属化软件组件的余代数模型框架下，对组件精化的理论进行了研究，并证明了模拟对于精化的一致性；本文研究了余代数理论在构件化软件开发方法中的应用，包括采用形式规范语言RSL进行组件的规范、精化和验证；本文还给出了统一建模语言UML部分视图模型的余代数语义，希望为基于组件的系统开发给出一种形式化的理论框架。本文工作的主要贡献详述如下：
本文首先通过对组件行为模式用强monad进行描述，采用强monad作为参数进行参数化，对基于状态的软件组件进行类属化并给出了类属化组件的余代数模型。在这一模型基础上，第3、4章分别给出了两种演算机制：同类和异类组件演算。在这两种演算中，分别给出了一族算子，用于对组件进行组合，同时给出了这些算子所满足的规则。
本文第5章在类属化组件的余代数模型基础上，提出了组件的行为精化的定义，将L模拟和L-1模拟统一为模拟，并证明了模拟对于行为精化的一致性。这一定义将精化通过组件接口函子上的精化前序表示出来，明确给出了组件行为精化的语义特征。这一工作从理论上对当前的各种精化方法进行了统一，通过选择适当的精化前序，这一精化概念可以适用于不同的具体精化中。
随后，第6章通过一个应用系统的实例，采用RSL作为规范语言，说明了如何将余代数方法应用于对软件组件的规范、精化和验证中，并在该实例中通过构造组件抽象规范的终结余代数，给出了一种状态空间最小的实现。
最后，在第7、8章中，本文对统一建模语言UML部分视图模型的余代数语义进行了研究，主要包括类图、用例图和状态机图的余代数语义，这一工作对UML中不同视图，初步给出了一种统一的语义模型，并且基于组件精化的理论，我们给出了状态机视图模型的一组精化演算规则。