软件动态正确性的形式化描述

• 作者: 张敏 陈仪香 马艳芳
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: 软件正确性 参数化互模拟 形式化 极限 拓扑
• 年，卷（期）: 2013,（3）
• 所属期刊栏目: 软件工程
• 页码范围: 626-635
• 页数: 10页
• 分类号: TP301.2
• 字数: 10749字
• 语种: 中文

摘要

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