期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

程序形式化验证中的两个基本问题 被引量：1

Two primary problems of verification to program formalization
下载PDF
导出
摘要 本文阐明了形式化验证中“中间断言”和“最弱前置谓词”两种思想和方法 ,在此基础上 ,解决了两个问题 :开始前置断言Q蕴涵非常弱的前置断言Q′与程序正确性的关系 ;对于验证程序正确性 。 The main purpose of this paper is to illuminate two thoughts and methods of formal verification: intermediate assertion and weakest predicate, on this base, two problems are solved:the relation to 'Q contain Q′'and program correction; to verify program correction, if intermediate assertion is weaker, sometimes it is not better.
作者 杨淑群 章仕昌
机构地区 抚州师范专科学校数学与计算机科学系 上饶师范学院物理系
出处 《上饶师范学院学报》 2002年第6期67-69,共3页 Journal of Shangrao Normal University
关键词 中间断言 最弱前置谓词 程序正确性 形式化方法 intermediate assertion weakest predicate program correction formal method
分类号 TP301.2 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献3

  • 1Floyd, R. W. Assigning Meanings to programs[J]. Proc. Symposium on Applied Mathematics, American Mathematical Society. 1967, (19):31 - 37.
  • 2Hoare, C. A. R. An Axiomatic Approach to Computer Programming[J]. Committ of the ACM, 1969, (12): 10.
  • 3Dijkstra. E. W., A Discipline of programming[M]. Prentice - Hall, Inc., Englewood Cliffs, N. J., 1976:93 - 131

同被引文献12

  • 1Joe Verzulli. Getting Started with JML Improve Your Java Programs with JML Annotation [J/OL ]. http z//www, ibm. com/developerworks/java/library/ j-jml/index, html, 2003-3-18.
  • 2Ernst M D. Dynamically Discovering Likely Program Invariants [D]. Washington : University of Washington Department of Computer Science and Engineering, 2000.
  • 3Michael D Ernst, Jeff H Perkins, Philip J Guo. The Daikon System for Dynamic Detection of Likely Invariants [J]. Science of Computer Programming, 2007,69(3) :35-45.
  • 4Jezequel J M,Bertrand Meyer. Design by Contraet z the Lessons of Ariane. Computer [J]. 1997 (8) t 129- 130.
  • 5Ernst M D. Static and Dynamic Analysis: Synergy and Duality[C]//In WODA 2003: ICSE Workshop on Dynamic Analysis, (Portland, OR),2003 : 24-27.
  • 6Hangal S, Lam M S. Tracking Down Software Bugs Using Automatic Detection[C]//In proceedings of the 24th International Conference on Software Engineering, 2002 : 291-301.
  • 7陆汝玲.计算机语言的形式语义[M].北京:科学出版社,1992.
  • 8David Schuler, Valentin Dallmeier, and Andreas Zeller. Efficient Mutation Testing by Checking Invariant Violations [C]//Proceedings of the 2009 International Symposium on Software Testing and Analysis, (Chicago, IL, USA), 2009,21-23.
  • 9Victor Braberman, Federico Ferndndez, et al. Parametric Prediction of Heap Memory Requirements [ C ]//In International Symposium on Memory Management, (Tucson, AZ, USA), 2008, 7-8: 141- 150.
  • 10牟光灿.软件测试是软件质量保证的重要手段[J].计算机应用研究,1997,14(2):3-5. 被引量：7

引证文献1

上饶师范学院学报
2002年 第6期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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