论文部分内容阅读
进程之间的等价关系或精化关系的同余或前同余性（congruence或precongruence）是组合式推理和模块化设计验证的理论基础。针对面向WebService的进程演算，Bemardi和Hennessy提出了Client—Must—Testing（CLT）语义及相关的测试前序 用于描述进程的精化关系，并对包含于 的最大前同余关系＋进行了研究。递归算子是规范理论中重要而且是基础性的算子，Bemardi和Hennessy对包含于 的最大前同余关系的研究中未涉及递归算子，因此不能描述进程的无限行为。文中研