论文部分内容阅读
为了增强带测试克林代数（KAT）的表达能力，提出了一种加概率的带测试克林代数（PKAT）的理论，并将其应用于对加概率正则程序的推演。将概率格局变迁系统作为操作语义的模型，它的每个状态是一个格局，格局是由一个PKAT表达式和一个数据状态组成的序列对。为了确立模型中的关系，定义自然语义和结构操作语义，均从行为和状态两方面进行刻画，证明两者在只考虑程序正常终止的情况下是等价的。