期刊文献+

程序断言的半自动生成及证明逻辑 被引量:3

Towards semi-automatic generation of program assertion and proof logic
下载PDF
导出
摘要 如何生成程序断言对于软件验证十分重要。传统方法要求既要对程序结构有深入地把握又要做繁复的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.
作者 何锫 康立山
出处 《计算机工程与应用》 CSCD 北大核心 2008年第14期18-20,30,共4页 Computer Engineering and Applications
基金 国家自然科学基金(the National Natural Science Foundation of China under Grant No.60473081)
关键词 HOARE逻辑 序验证 程序断言 XYZ/VERI Hoare ' s logic program verification program assertion XYZ/VERI
  • 相关文献

参考文献20

  • 1Hoare T. The verifying compiler: a grand challenge for computing research [ C ]//LNCS 2622,2003:262-272.
  • 2Seacord R C, Plakosh D, Lewis G A. Modernizing legacy system : software technologies, engineering processes, and business practices [ M ]. [ S.l. ] : Pearson Education Limited,2003.
  • 3Ashenhurst R L,Graham S. ACM turing award lectures:the first twenty years ( 1965-1985 ) [ M ]. [ S.l.] :The ACM Press, 1991.
  • 4Juristo N,Moreno A M, Vegas S. Reviewing 25 years of testing technique experiments [ J ]. Empirical Software Engineering,2004,9:1-2.
  • 5Petrenko A K. Yerification, validation, and testing of large software [ J ]. Programming and Computer Software ,2003,29:6.
  • 6Kneuper R. Limits of formal metltods[J]. Formal Aspects of Computing, 1997 (9).
  • 7Piccinini G. Alan tudng and the mathematical objection [ J ]. Minds and Machines, 2003,13:23-48.
  • 8Woods S,Yang Qiang. The program understanding problem: analysis and a heuristic approach[ C ]//IEEE Proceedings of ICSE' 18,1996.
  • 9Hoare C A R. An axiomatic basis for computer programming [ J ].CACM, 1969,12:576-583.
  • 10He Pei, Li Ren-wei,Zhang Wen-hui. Theory and practice for XYZ/ VERI System [ C ]//IFIP Trans on Automated Reasoning. North-Hotland : Elsevier Science Publishers B V, 1993.

共引文献162

同被引文献20

  • 1何锫,唐稚松.N_L:松弛时序逻辑自然推理系统[J].软件学报,1993,4(4):51-55. 被引量:2
  • 2李虎,金茂忠,许福,张敏.程序设计语言的GLR优化分析[J].软件学报,2005,16(2):174-183. 被引量:2
  • 3Hoare T.The verifying compiler:a grand challenge for computing research[C]//LNCS 2622,2003:262-272.
  • 4Seaeord R C,Plakosh D,Lewis G A.Modernizing legacy system:software technologies,engineering processes,and business praetiees[M].[S.l.]: Pearson Education Limited,2003.
  • 5Ashenhurst R L,Graham S.ACM turing award lectures:the first twenty years( 1965-1985)[M].[S.l.] :The ACM Press, 1991.
  • 6Juristo N,Moreno A M,Vegas S.Reviewing 25 years of testing technique experiments[J].Empirical Software Engineering,2004,9:1-2.
  • 7Petrenko A K.Verification,validation,and testing of large software[J]. Programming and Computer Software, 2003,29: 6.
  • 8Kneuper R.Limts of formal methods[J].Formal Aspects of Computing, 1997,9.
  • 9Piccinini G.Alan turing and the mathematical objection[J].Minds and Machines,2003,13:23-48.
  • 10Woods S,Yang Q.The program understanding problem:analysis and a heuristic approach[C]//IEEE Proceedings of ICSE' 15,1996.

引证文献3

二级引证文献2

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部