论文部分内容阅读
软件正确性是软件可信性的重要属性。在实际软件开发和设计中，需要不断地对软件进行修改，从而软件越来越正确。为了讨论软件的动态近似正确性，基于概率进程代数的ε-互模拟，建立软件越来越正确的形式化描述。定义ε-极限互模拟，用来反应软件实现与规范之间的关系，给出一些特殊的ε-极限互模拟。提出ε-互模拟极限，用其刻画规范是软件实现的极限形式，同时证明ε-互模拟极限的一些性质。