通过抽象程序证明复杂具体程序

来源 :软件学报 | 被引量 : 0次 | 上传用户：qwer96669

【摘要】

：

描述了证明抽象程序和具体程序满足一致性关系的方法.抽象程序使用抽象数据结构（ADTs）,如set,list,map及其上的操作.具体程序使用类C语言中的类型.抽象程序和具体程序一致性证

【作者】

：

李彬汤震浩翟娟赵建华

【机构】

：

计算机软件新技术国家重点实验室（南京大学）

【出处】

：

软件学报

【发表日期】

：

2017年4期

【关键词】

：

程序证明一致性抽象程序精化分解 program verification consistency abstract program refinem

【基金项目】

：

国家自然科学基金（61632015,61561146394）, 国家重点基础研究发展计划（973）（2016YFB1000802）

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

描述了证明抽象程序和具体程序满足一致性关系的方法.抽象程序使用抽象数据结构（ADTs）,如set,list,map及其上的操作.具体程序使用类C语言中的类型.抽象程序和具体程序一致性证明需要用户给出抽象变量和具体变量的关系、抽象程序程序点和具体程序程序点的对应关系.基于对应关系,抽象程序和具体程序一致性证明可以分解,从而容易并可能自动证明.

其他文献

江苏省邳州市英华实验小学师生剪纸作品选登

期刊

SnO<sub>2</sub>薄膜超微粒子平均大小的测定

近年来,SnO<sub>2</sub>超微粒子薄膜在气敏材料上的应用引起了人们极大的兴趣。薄膜的粒子大小和形状直接影响到它的性能。作者利用X射线宽化法测定了粒子的平均大小。自编

期刊

超微粒子薄膜气敏材料X射线衍射ultrafine particle film gas sensitive matrials X-ray diffrac

大学物理试题库的研制

本文介绍了大学物理试题库的研制工作,以及生成试卷的理论依据和主要参数,并运用教育统计学和教育测量学理论,对实测结果进行了分析。

期刊

试题库正态分布考试.test basepositive distributiontest.

构建真实语境促进有效输出——译林新版六下Unit 7 Summer holiday plans第一课时教学设计

【设计理念】Unit 7 Summer holiday plans是译林新版《英语》六下的内容,其story time板块主要讲Miss Li和她的学生们在为即将到来的暑假进行规划的事。本课话题与学生的生

期刊

HOLIDAY译林真实语境第一课story《英语》旅游计划语言输出GUESS一般将来时

南京市长江路小学学生美术作品选登

期刊

一种准确而高效的领域知识图谱构建方法

作为语义网的数据支撑,知识图谱在知识问答、语义搜索等领域起着至关重要的作用,一直以来也是研究领域和工程领域的一个热点问题,但是,构建一个质量较高、规模较大的知识图谱往往需要花费巨大的人力和时间成本.如何平衡准确率和效率、快速地构建出一个高质量的领域知识图谱,是知识工程领域的一个重要挑战.对领域知识图谱构建方法进行了系统研究,提出了一种准确、高效的领域知识图谱构建方法——"四步法",将该方法应用到中

期刊

语义网知识图谱本体语义标注实体集扩充关系抽取

基于SMT的时钟约束语言CCSL的形式化分析方法与工具

时钟约束语言CCSL是一种用于描述实时嵌入式系统中事件之间约束的形式化语言,它是UML针对实时嵌入式系统建模的扩展包MARTE（modeling and analysis of real-time and embedded

期刊