教育论文网

Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用
硕士博士毕业论文站内搜索    
分类：教育论文网→工业技术论文→自动化技术、计算机技术论文→计算技术、计算机技术论文→计算机软件论文→程序设计、软件工程论文→程序设计论文
Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用
论文目录
 
摘要第1-4 页
Abstract第4-8 页
第一章 绪论第8-15 页
　　· 研究背景和意义第8-10 页
　　· 相关研究情况第10-14 页
　　· 主要研究工作第14-15 页
第二章 形式化方法和PAR 方法第15-25 页
　　· 形式化方法第15-19 页
　　　　· 形式化方法的研究内容第16-17 页
　　　　· 形式化方法的分类第17-18 页
　　　　· 形式化方法的能力和局限第18 页
　　　　· 形式化方法在高可信软件开发中的重要性第18-19 页
　　· PAR 方法第19-25 页
　　　　· PAR 方法/PAR 平台简介第20 页
　　　　· 算法设计语言Radl第20-22 页
　　　　· 抽象程序设计语言Apla第22-25 页
第三章 Isabelle 定理证明器的剖析第25-37 页
　　· 定理证明器的分类第25-26 页
　　· Isabelle 定理证明器的剖析第26-32 页
　　　　· Isabelle 定理证明器的特点第26-28 页
　　　　· Isabelle 定理证明器的系统结构第28-30 页
　　　　· Isabelle 定理证明器的理论第30-31 页
　　　　· Isabelle 定理证明器的证明方法第31-32 页
　　· Isabelle 定理证明器的规则/策略第32-37 页
　　　　· 规则第32-35 页
　　　　· 策略第35-37 页
第四章 Isabelle 在PAR 方法/PAR 平台中的应用第37-70 页
　　· PAR 方法开发算法程序第37-39 页
　　· 算法程序正确性的证明方法第39-44 页
　　　　· Floyd 的归纳断言法第40 页
　　　　· Hoare 公理方法第40-42 页
　　　　· Dijkstra 最弱前置谓词方法第42-44 页
　　· Isabelle 验证使用PAR 方法/PAR 平台开发的算法程序第44-67 页
　　　　· Isabelle 验证算法程序的工作流程第44-46 页
　　　　· 数组和算法程序的验证第46-48 页
　　　　· 数组段最小和算法程序的验证第48-52 页
　　　　· Hanoi 塔非递归算法程序的验证第52-58 页
　　　　· 二叉树遍历非递规算法程序的验证第58-67 页
　　· Isabelle 验证 PAR 平台中部分的转换代码第67-70 页
　　　　· 选择语句转换规则的验证第67-68 页
　　　　· 循环语句转换规则的验证第68-70 页
第五章 总结与展望第70-71 页
　　· 工作总结第70 页
　　· 下一步工作目标第70-71 页
参考文献第71-76 页
致谢第76-77 页
攻读学位期间参与的科研项目第77 页
攻读学位期间发表(完成)的学术论文目录第77 页

本篇论文共77页，点击这进入下载页面。
 
更多论文
Isabelle定理证明器的剖析及其在PA
我军装备采办成本控制研究
新贸易壁垒及其作用机制分析--在国
基于语义的构件检索技术研究与实现
影响军事技术创新的文化因素分析
SanderSⅢ型跟骨骨折两种监测手术治
基于本体的个性化元搜索技术的研究
局部战争中我国战略产业安全研究
不确定性对我国城镇居民消费和投资
基于熵理论的军事教育组织系统分析
Radl→Apla程序生成系统及其可靠性
关联理论视角下汉语临时词义缩小与
基于关联理论的汉语语篇桥接指称阐
基于独立成分分析的图像检索的研究
语际语用能力发展的探索性研究
信息检索中迁移Markov网络模型的研
从解释学视角探讨译者在翻译中的理
人工神经网络在认知诊断中的应用研
对认知原则和交际原则的实证研究
计算机化自适应测验选题策略研究--
集中建构的意识提升策略抵制语法错
PDA设备安全管理系统生成器的分析、
中介策略区间—解读大学英语口试中
一种基于中间件技术的角色访问控制
奈达功能对等理论指导下的旅游资料
从BPEL到Petri网映射的研究
“聚焦于形式”的语言教学对正确使
APLA语言并发机制的研究
接受理论指导下的古典汉诗英译中的
英汉名动转用的认知研究
英语宣战演说的人际意义研究
基于骨架的并行编程环境中结构骨架
市场经济体制下乡镇农技推广体系的
从接受理论的角度论儿童文学的英汉
基于潜在中间语义的多语言信息检索
经济发达地区土地利用变化及其驱动
关联理论框架下的隐含义研究
基于扩展PCA图像分类模型研究
论昆德拉小说的希腊精神
大城市与小城镇吸纳外来人口能力与
从关联理论角度探讨战争影片字幕翻
反内核模式驱动级病毒技术研究及策
经济发达地区城市用地扩展与供地政
从关联翻译理论角度看幽默对话的汉
基于本体论的可复用构件表示研究及
农产品市场时空格局与江苏农业结构
传播学理论观照下的揭示语翻译研究
基于树形结构构件库组装研究与实现
H2S在大鼠心肺复苏后脑
中国英语学习者拒绝言语行为中的语
 
形式化方法论文 高可信软件论文 形式化验证论文 定理证明论文 高阶逻辑论文 交互式定理证明器论文 算法程序论文 PAR方法论文 PAR平台论文
版权申明：目录由用户wwwf**提供，www.51papers.com仅收录目录，作者需要删除这篇论文目录请点击这里。
| 设为首页||加入收藏||站内搜索引擎||站点地图||在线购卡|
版权所有 教育论文网 Copyright(C) All Rights Reserved