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