计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2008年
14期
18-20,30
,共4页
Hoare逻辑%序验证%程序断言%XYZ/VERI
Hoare邏輯%序驗證%程序斷言%XYZ/VERI
Hoare라집%서험증%정서단언%XYZ/VERI
如何生成程序断言对于软件验证十分重要.传统方法要求既要对程序结构有深入地把握又要做繁复的Hoare三元式推演工作.为了摆脱这些琐碎事宜,将致力于探讨一种半自动的断言生成方法.为便于理解,讨论主要以XYZ/VERI系统为论述背景.XYZ/VERI系统是一面向时序逻辑程序语言如XYZ/SE的类Hoare逻辑交互式验证系统.该工作一定意义上完善了其验证功能.
如何生成程序斷言對于軟件驗證十分重要.傳統方法要求既要對程序結構有深入地把握又要做繁複的Hoare三元式推縯工作.為瞭襬脫這些瑣碎事宜,將緻力于探討一種半自動的斷言生成方法.為便于理解,討論主要以XYZ/VERI繫統為論述揹景.XYZ/VERI繫統是一麵嚮時序邏輯程序語言如XYZ/SE的類Hoare邏輯交互式驗證繫統.該工作一定意義上完善瞭其驗證功能.
여하생성정서단언대우연건험증십분중요.전통방법요구기요대정서결구유심입지파악우요주번복적Hoare삼원식추연공작.위료파탈저사쇄쇄사의,장치력우탐토일충반자동적단언생성방법.위편우리해,토론주요이XYZ/VERI계통위논술배경.XYZ/VERI계통시일면향시서라집정서어언여XYZ/SE적류Hoare라집교호식험증계통.해공작일정의의상완선료기험증공능.
