基于程序正确性的演算方法

作     者：任彦芳 杨静 索丙芮 REN Yan-fang;YANG Jing;SUO Bing-rui

作者机构：贵州大学计算机科学与信息工程学院 

基　　金：国家自然科学基金项目(90718009) 贵州省科学技术基金项目(黔科合J字2123) 

出 版 物：《计算机工程与设计》 (Computer Engineering and Design)

年 卷 期：2009年第30卷第17期

页      码：4020-4022页

摘      要：为了使开发出的程序更具有可靠性,研究了两种正确性验证的演算方法,Dijkstra的最弱前置谓词变换法和Hoare的公理化方法。针对于Hoare公理化方法证明中的前置条件难以寻找的问题,提出了将这两种演算方法结合使用的方法。对最弱前置谓词变换法的过程进行分析,确定了最弱前置谓词算法的准确性。将最弱前置谓词应用到公理化方法中,即把最弱前置谓词变换法求出的前置谓词作为公理化方法的前置条件。通过一个具体实例,详细说明了其验证过程,并证明了该方法的有效性。

主 题 词：可靠性 正确性验证 最弱前置谓词 公理化方法 前置条件 

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

D　O　I：10.16208/j.issn1000-7024.2009.17.026

馆 藏 号：203764113...