-
题名基于语法树的程序正确性验证模型及算法设计
被引量：2
- 1
-
-
作者
周必水
张延红
赵敬
-
机构
杭州电子科技大学计算机学院
中国电子科技集团二十二所
-
出处
《杭州电子科技大学学报（自然科学版）》
2006年第1期1-4,共4页
-
基金
省教育厅基金项目(KYH063103004)
-
文摘
基于语法树的程序正确性验证方法是目前程序正确性验证全新的研究领域,该方法以程序的语法树作为程序正确性的检验对象,运用适当的树匹配算法,来验证目标程序的正确性。该文在介绍基于语法树的程序正确性验证方法的基础上,借鉴无序标签树匹配的相关研究成果,结合软件构件的查询技术,提出一种新的XML路径查询模型和树匹配算法,并展示了STM在程序正确性验证方面的前景。
-
关键词
程序正确性验证
树匹配
路径查询
匹配度
-
Keywords
proof of program correctness
XML
tree matching path query
xpath matching degree
-
分类号
TP391.76
[自动化与计算机技术—计算机应用技术]
-
-
题名基于Kripke结构的程序正确性证明
被引量：1
- 2
-
-
作者
林杰
余建坤
-
机构
云南财经大学信息学院
-
出处
《计算机应用》
CSCD
北大核心
2011年第5期1425-1427,共3页
-
文摘
为了方便证明程序的正确性,引入了Kripke结构,提出基于Kripke结构的程序正确性证明。重新定义了适合证明的Kripke结构,并描述了将程序流程图转换为Kripke结构状态图的方法。给出了证明程序正确性的相关定理和基于Kripke结构的程序正确性证明方法。证明方法为:首先,把程序流程图转换为状态图;然后,根据状态之间的转移关系列出每个状态下的状态谓词;最后,证明每个状态谓词为真。根据状态谓词进行证明,能够反映出程序执行的状态。用该方法对一个实例进行了完整的证明。
-
关键词
KRIPKE结构
程序正确性证明
状态图
谓词
-
Keywords
Kripke structure
proof of program correctness
state diagram
predicate
-
分类号
TP311.1
[自动化与计算机技术—计算机软件与理论]
-
-
题名关于循环终止性证明的一种最小不动点方法
- 3
-
-
作者
宋炜
-
机构
江西工业大学计算机系
-
出处
《江西工业大学学报》
1991年第1期40-45,共6页
-
文摘
本文分析了循环终止性的特点,给出了实WHILE语句模型,简要地叙述了最小不动点理论,并结合到实循环函数上讨论了终止性的证明。
-
关键词
程序设计
循环终止法
最小不动点
-
Keywords
programming
proof of program correctness
least fixpoint
loop termination
-
分类号
TP311.1
[自动化与计算机技术—计算机软件与理论]
-
-
题名基于语法树和程序正确性验证研究
- 4
-
-
作者
周必水
李骏
沃钧军
-
机构
杭州电子科技大学软件学院
-
出处
《计算机应用与软件》
CSCD
北大核心
2007年第4期111-112,156,共3页
-
文摘
提出了一种新的基于语法树的程序正确性验证方法(STM方法)。在理论和算法上对方法的实现进行了初步探讨,并结合XML技术提出了一套实现这一方法的切实可行的解决方案。
-
关键词
程序正确性验证
语法树
XML
解决方案
-
Keywords
proof of program correctness Syntax tree XML
-
分类号
TP311.1
[自动化与计算机技术—计算机软件与理论]
-
-
题名程序正确性证明的一种方法
被引量：1
- 5
-
-
作者
王凤林
嵇琦
-
机构
哈尔滨投资高等专科学校
-
出处
《大电机技术》
北大核心
1998年第3期18-22,共5页
-
文摘
本文形式地描述了一种证明程序能够正确地进行计算的方法。为了做到这一点，这里给出了一个程序及其执行的抽象模型。然后相对于这一模型给出了程序正确性和程序正确性证明的方法。
-
关键词
程序证明
程序正确性
程序设计方法学
-
Keywords
program proof program correctness programming methodology abstract model
-
分类号
TP311.1
[自动化与计算机技术—计算机软件与理论]
-
