基于环境的软件正确性形式化描述

作     者：马艳芳 张敏 陈仪香 

作者机构：淮北师范大学计算机科学与技术学院安徽淮北235000 华东师范大学软件学院上海200062 上海市高可信计算重点实验室上海200062 

基　　金：国家自然科学基金项目(90718013) 国家高技术研究发展计划(863计划)资助项目(2007AA01Z189) 安徽省高等学校省级自然科学研究重点项目(KJ2011A248) 上海市高可信计算重点实验室开放课题研究项目 

出 版 物：《山东大学学报（理学版）》 (Journal of Shandong University(Natural Science))

年 卷 期：2011年第46卷第9期

页      码：22-27页

摘      要：软件的运行依赖于环境,在考察软件正确性时需要考虑环境的因素。软件在开发和设计过程中,其正确性是一个逐渐改进的过程,也就是说,通过不断地修改,软件越来越接近于正确。为了刻画软件的这种动态正确性并考虑环境的因素,本文将以三分之二互模拟为基础,利用网极限的观点,建立软件动态正确性的形式化描述。首先建立三分之二互模拟的无限演化理论,给出三分之二极限互模拟的定义。其次建立三分之二互模拟极限,这个极限在一定程度上反映软件规范是其实现的极限形式。最后证明三分之二互模拟极限与三分之二互模拟的相容性等性质。

主 题 词：极限 三分之二互模拟 正确性 形式化 

学科分类：08[工学] 081202[081202] 0812[工学-测绘类] 

核心收录：

馆 藏 号：203141613...