一种精化演算支撑工具的分析与设计

• 作者: 庞军 李必信 查鸣 王云峰 郑国梁
• 来源期刊: 南京大学学报（自然科学）
• 学科: 工学
• 关键词: 形式方法 精化演算 精化工具 窗口推理
• 年，卷（期）: 2000,（5）
• 页码范围: 560-567
• 页数: 8页
• 分类号: TP311.51
• 字数: 5635字
• 语种: 中文
• DOI: 10.3321/j.issn:0469-5097.2000.05.005

摘要

利用精化演算的方法开发软件,其过程由巨大数量的小步骤构成,由手工完成极其烦琐,也极容易出错,因此利用机器辅助工具的支持是必要的,在分析现有的精化工具的基础上,提出了一个用于软件形式化开发的的精化工具(RT),并对其进行了需求分析和功能分析.在精化工具的设计中,讨论了作为定理证明器和精化引擎基础的窗口推理系统和用于程序精化推理的程序窗口推理系统,同时分析了设计中的设计目标,总体结构,精化与证明的表示方法,用户界面和工具的扩充性等问题,对于工具的理论基础做了较为详细的分析,提出了精化工具的概要设计.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郑国梁	南京大学计算机软件新技术国家重点实验室南京大学计算机科学与技术系	77	1523	21.0	37.0
2	李必信	南京大学计算机软件新技术国家重点实验室南京大学计算机科学与技术系	25	467	11.0	21.0
3	王云峰	南京大学计算机软件新技术国家重点实验室南京大学计算机科学与技术系	14	226	6.0	14.0
4	庞军	南京大学计算机软件新技术国家重点实验室南京大学计算机科学与技术系	4	17	1.0	4.0
5	查鸣	南京大学计算机软件新技术国家重点实验室南京大学计算机科学与技术系	3	2	1.0	1.0