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

• 作者: 任彦芳 杨静 索丙芮
• 来源期刊: 计算机工程与设计
• 学科: 工学
• 关键词: 可靠性 正确性验证 最弱前置谓词 公理化方法 前置条件
• 年，卷（期）: 2009,（17）
• 所属期刊栏目: 软件与算法
• 页码范围: 4020-4022
• 页数: 3页
• 分类号: TP391.2
• 字数: 3386字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	杨静	贵州大学计算机科学与信息工程学院	45	178	7.0	11.0
2	任彦芳	贵州大学计算机科学与信息工程学院	3	11	2.0	3.0
3	索丙芮	贵州大学计算机科学与信息工程学院	3	8	1.0	2.0