-
题名基于Hoare逻辑的过程调用的形式化方法
被引量:2
- 1
-
-
作者
雷富兴
张来顺
-
机构
解放军信息工程大学电子技术学院
-
出处
《计算机工程与设计》
CSCD
北大核心
2011年第1期197-201,共5页
-
文摘
采用Hoare逻辑风格的推理,提出了一些从源代码推导过程和这些过程调用的形式化语义规范的技术和算法。为了推导一个过程调用的语义,将过程看作一个抽象单元从程序分离出来,提取过程的形式化语义规范。对于一个具体的过程调用,形式化这个调用的前置条件,根据这些条件形式化求解调用的最强后置条件,也就是调用的语义作用。
-
关键词
HOARE逻辑
过程语义
过程调用语义
前置条件
后置条件
-
Keywords
Hoare logic
procedure semantic
procedure call semantic
precondition
postcondition
-
分类号
TP391
[自动化与计算机技术—计算机应用技术]
-
-
题名循环条件的形式化推导在程序验证中的应用
被引量:1
- 2
-
-
作者
雷富兴
张来顺
石荣刚
杨科
-
机构
解放军信息工程大学电子技术学院
西安通信学院
[
-
出处
《计算机工程与设计》
CSCD
北大核心
2010年第14期3193-3197,共5页
-
文摘
提出了一种求解命令式程序中循环执行和终止条件的方法。该方法基于循环代码本身进行循环执行和终止条件的分析推导,可以定义一个原型工具进行自动化推导。现有的形式化方法依赖于形式化规范,而提出的方法适用于未被形式化的程序。提出的形式化方法可以在一个原型工具中实现,通过该工具来推导循环执行和终止条件,辅助程序验证和程序缺陷修正。
-
关键词
循环执行
循环终止
形式化方法
自动化
程序验证
缺陷修正
-
Keywords
loop progress
loop termination
formal method
automated
program verification
defect correction
-
分类号
TP391
[自动化与计算机技术—计算机应用技术]
-