程序断言的半自动生成及证明逻辑

• 作者: 何锫 康立山
• 来源期刊: 计算机工程与应用
• 学科: 工学
• 关键词: Hoare逻辑 序验证 程序断言 XYZ/VERI
• 年，卷（期）: 2008,（14）
• 所属期刊栏目: 博士论坛
• 页码范围: 18-20,30
• 页数: 4页
• 分类号: TP301.6
• 字数: 3954字
• 语种: 中文
• DOI: 10.3778/j.issn.1002-8331.2008.14.004

摘要

如何生成程序断言对于软件验证十分重要.传统方法要求既要对程序结构有深入地把握又要做繁复的Hoare三元式推演工作.为了摆脱这些琐碎事宜,将致力于探讨一种半自动的断言生成方法.为便于理解,讨论主要以XYZ/VERI系统为论述背景.XYZ/VERI系统是一面向时序逻辑程序语言如XYZ/SE的类Hoare逻辑交互式验证系统.该工作一定意义上完善了其验证功能.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	康立山	武汉大学软件工程国家重点实验室	127	2409	27.0	44.0
2	何锫	武汉大学软件工程国家重点实验室	7	19	3.0	3.0