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

计算机工程与应用 ›› 2008, Vol. 44 ›› Issue (14): 18-20.

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

何锫,康立山

武汉大学软件工程国家重点实验室，武汉 430072

收稿日期:2008-02-21 修回日期:2008-03-21 出版日期:2008-05-11 发布日期:2008-05-11
通讯作者: 何锫

Towards semi-automatic generation of program assertion and proof logic

HE Pei,KANG Li-shan

State Key Laboratory of Software Engineering，Wuhan University，Wuhan 430072，China

Received:2008-02-21 Revised:2008-03-21 Online:2008-05-11 Published:2008-05-11
Contact: HE Pei

摘要/Abstract

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

关键词: Hoare 逻辑, 序验证, 程序断言, XYZ/VERI

Abstract: How to generate program assertions is of great importance to software verifications Classical approach to this problem relies on a good command of program structures and repeatedly applying Hoare’s rule for deducing Hoare triples.In order to get rid of this tedious work，we will dedicate in this paper to establish a semi-automatic approach to assertion generations.To facilitate understanding，the discussion is mainly based on XYZ/VERI system，a Hoare-like interactive verification system for temporal logic programming language like XYZ/SE.To some extent，this work helps with its functionality improvement.

Key words: Hoare’s logic, program verification, program assertion, XYZ/VERI

何锫,康立山. 程序断言的半自动生成及证明逻辑[J]. 计算机工程与应用, 2008, 44(14): 18-20.

HE Pei,KANG Li-shan. Towards semi-automatic generation of program assertion and proof logic[J]. Computer Engineering and Applications, 2008, 44(14): 18-20.

[1]	朱博元1，刘高辉1，李政运2，安述倩2. RISC指令集众核处理器功能验证与实现[J]. 计算机工程与应用, 2014, 50(21): 54-58.
[2]	刘澜，袁道华，童星，王钟磊. 一种针对可信计算平台的分布式可信验证机制[J]. 计算机工程与应用, 2012, 48(2): 99-102.
[3]	肖增良¹,何锫¹,康立山². 并行程序验证的调度策略[J]. 计算机工程与应用, 2009, 45(11): 39-41.