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

作者：何锫 康立山hoare逻辑序验证程序断言

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

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社