基于环境的软件正确性形式化描述 |
| |
引用本文: | 马艳芳,张敏,陈仪香.基于环境的软件正确性形式化描述[J].山东大学学报(理学版),2011,46(9):22-27. |
| |
作者姓名: | 马艳芳 张敏 陈仪香 |
| |
作者单位: | 1. 淮北师范大学计算机科学与技术学院,安徽淮北,235000 2. 华东师范大学软件学院,上海200062/上海市高可信计算重点实验室,上海200062 |
| |
基金项目: | 国家自然科学基金项目(90718013); 国家高技术研究发展计划(863计划)资助项目(2007AA01Z189); 安徽省高等学校省级自然科学研究重点项目(KJ2011A248); 上海市高可信计算重点实验室开放课题研究项目 |
| |
摘 要: | 软件的运行依赖于环境,在考察软件正确性时需要考虑环境的因素。软件在开发和设计过程中,其正确性是一个逐渐改进的过程,也就是说,通过不断地修改,软件越来越接近于正确。为了刻画软件的这种动态正确性并考虑环境的因素,本文将以三分之二互模拟为基础,利用网极限的观点,建立软件动态正确性的形式化描述。首先建立三分之二互模拟的无限演化理论,给出三分之二极限互模拟的定义。其次建立三分之二互模拟极限,这个极限在一定程度上反映软件规范是其实现的极限形式。最后证明三分之二互模拟极限与三分之二互模拟的相容性等性质。
|
关 键 词: | 极限 三分之二互模拟 正确性 形式化 |
本文献已被 CNKI 万方数据 等数据库收录! |
|