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

Towards semi-automatic generation of program assertion and proof logic

作　　者：何锫[1] 康立山[1] 

机构地区：[1]武汉大学软件工程国家重点实验室,武汉430072

出　　处：《计算机工程与应用》2008年第14期18-20,30,共4页Computer Engineering and Applications

基　　金：国家自然科学基金(the National Natural Science Foundation of China under Grant No.60473081)

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

关 键 词：HOARE逻辑 序验证 程序断言 XYZ/VERI 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]