-
题名精化演算支撑工具的分析
- 1
-
-
作者
王云峰
庞军
查鸣
杨朝晖
郑国梁
-
机构
南京大学计算机软件新技术国家重点实验室
南京大学计算机科学与技术系
-
出处
《计算机应用与软件》
CSCD
北大核心
2002年第2期1-5,53,共6页
-
基金
国家自然科学基金(编号:69673006)
国家"九五"攻关(子专题合同编号:98-780-01-06-07)项目的资助
-
文摘
利用精化演算的方法开发软件,其过程由巨大数量的小步骤构成,由手工完成极其烦琐,也极容易出错。因此,利用机器辅助工具的支持是必要的。在分析现有的精化工具的基础上,我们提出了一个用于软件形式化开发的精化工具RT(RefinementTool),对精化工具进行了需求分析和功能分析。在精化工具的设计中,分析了精化工具的设计目标、总体结构、精化与证明的表示方法、用户界面和工具的扩充性等问题,通过对精化和证明的表示方法的分析,提出了一种精化与证明的表示相结合的方法。
-
关键词
形式方法
精化演算支撑工具
软件工具
计算机
-
Keywords
Formal method Refinement calculus Refinement tool
-
分类号
TP311.56
[自动化与计算机技术—计算机软件与理论]
-
-
题名精化演算支撑工具PRT的研究
- 2
-
-
作者
杨朝晖
王云峰
郑国梁
-
机构
南京大学计算机软件新技术国家重点实验室计算机科学与技术系
-
出处
《计算机科学》
CSCD
北大核心
2000年第3期47-50,46,共5页
-
基金
国家自然科学基金
国家"九五"攻关项目基金
-
文摘
1 引言精化演算是一种数学表示法和若干规则的集合,用于从程序规约推导出命令式程序。精化是从抽象程序向具体程序转换的过程,其中包含程序的正确性证明。精化的程序开发方法比对已有程序进行验证以保证程序正确性的方法更有效。通过精化演算中的转换规则可以演算出精化的程序。利用精化演算从规约导出程序的过程由大量步骤构成,非常适合利用机器工具进行辅助。本文对精化工具进行了需求分析和功能分析,研究了一个新的精化工具PRT(Program Refinement Tool)并与现有的一些工具进行了比较。
-
关键词
程序正确性
精化演算支撑工具
PRT
程序结构
-
Keywords
Refinement calculus ,Refinement tool, Theorem proof ,Window reasoning
-
分类号
TP311.1
[自动化与计算机技术—计算机软件与理论]
-