| 程序形式化验证中的两个基本问题 |
| |
| 引用本文： | 杨淑群,章仕昌. 程序形式化验证中的两个基本问题[J]. 上饶师范学院学报, 2002, 22(6): 67-69 |
| |
| 作者姓名： | 杨淑群 章仕昌 |
| |
| 作者单位： | 1. 抚州师范专科学校数学与计算机科学系,江西,抚州,344000
2. 上饶师范学院物理系,江西,上饶,334001 |
| |
| 摘 要： | 本文阐明了形式化验证中“中间断言”和“最终前置谓词”两种思想和方法，在此基础上，解决了两个问题：开始前置断言Q蕴函非常弱的前置断言Q′与程序正确性的关系；对于验证程序正确性，中间断言并不是越弱越好。
|
| 关 键 词： | 中间断言 最弱前置谓词 程序正确性 形式化方法 |
| 文章编号： | 1004-2237(2002)06-0067-03 |
| 修稿时间： | 2002-09-18 |
Two primary problems of verification to program formalization |
| |
| YANG Shu-qun ,ZHANG shi-chang. Two primary problems of verification to program formalization[J]. Journal of Shangrao Normal College, 2002, 22(6): 67-69 |
| |
| Authors: | YANG Shu-qun ZHANG shi-chang |
| |
| Affiliation: | YANG Shu-qun 1,ZHANG shi-chang 2 |
| |
| Abstract: | |
| |
| Keywords: | intermediate assertion weakest predicate program correction formal method |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
