| 基于程序正确性的演算方法 |
| |
| 引用本文： | 任彦芳,杨静,索丙芮. 基于程序正确性的演算方法[J]. 计算机工程与设计, 2009, 30(17) |
| |
| 作者姓名： | 任彦芳 杨静 索丙芮 |
| |
| 作者单位： | 贵州大学,计算机科学与信息工程学院,贵州,贵阳,550025;贵州大学,计算机科学与信息工程学院,贵州,贵阳,550025;贵州大学,计算机科学与信息工程学院,贵州,贵阳,550025 |
| |
| 基金项目： | 国家自然科学基金项目，贵州省科学技术基金项目 |
| |
| 摘 要： | 为了使开发出的程序更具有可靠性,研究了两种正确性验证的演算方法,Dijkstra的最弱前置谓词变换法和Hoare的公理化方法.针对于Hoare公理化方法证明中的前置条件难以寻找的问题,提出了将这两种演算方法结合使用的方法.对最弱前置谓词变换法的过程进行分析,确定了最弱前置谓词算法的准确性.将最弱前置谓词应用到公理化方法中,即把最弱前置谓词变换法求出的前置谓词作为公理化方法的前置条件.通过一个具体实例,详细说明了其验证过程,并证明了该方法的有效性.
|
| 关 键 词： | 可靠性 正确性验证 最弱前置谓词 公理化方法 前置条件 |
Checking method based on program correctness |
| |
| REN Yan-fang,YANG Jing,SUO Bing-rui. Checking method based on program correctness[J]. Computer Engineering and Design, 2009, 30(17) |
| |
| Authors: | REN Yan-fang YANG Jing SUO Bing-rui |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 万方数据 等数据库收录！ |
|
