论文部分内容阅读
软件正确性是一个逐渐改进的过程．通过不断地修改，软件越来越接近于正确．同时软件的执行依赖于环境．为了刻画软件的动态正确性并考虑环境的因素，以参数化互模拟为基础，利用极限的观点，建立软件动态正确性的形式化描述．首先建立参数化互模拟的无限演化理论，给出参数化极限互模拟的定义，并给出几个特殊的参数化极限互模拟实例．其次，建立参数化互模拟极限，给出参数化互模拟极限的规约刻画．最后，证明参数化互模拟极限的唯一性、与参数化互模拟的相容性等代数性质．