论文部分内容阅读
通常情况下，我们很难确定一段给定的程序是否符合它的规范，程序提取是一种从构造性证明中提取函数式程序的机制，其构造特性很好地保证了生成程序的正确性。这就为我们提供了一种开发正确性软件的方法。本文基于对Coq中程序提取机制的研究，阐述了它的理论基础、实现机制及应用。
从构造性证明中提取程序
【摘 要】
：
通常情况下，我们很难确定一段给定的程序是否符合它的规范，程序提取是一种从构造性证明中提取函数式程序的机制，其构造特性很好地保证了生成程序的正确性。这就为我们提供了一种
【机 构】
：
信息工程大学信息工程学院计算机科学与技术系
【出 处】
：
计算机科学
【发表日期】
：
2007年5期
【基金项目】
：
本课题得到欧盟项目TYPES（项目编号：types project 29001）资助.感谢英国伦敦大学罗朝晖（Prof.Zhaohui Luo）教授、英国杜伦（Durham）大学保罗.卡拉汉博士（Dr.Paul Callaghan）的帮助和指导,感谢来自欧盟和杜伦大学的资助.
其他文献
家庭教育在高职学生成长成才中有着举足轻重的作用,和学校教育、社会教育有着不同的侧重点。文章通过凝练家庭教育的内容、探索家庭教育的途径、健全家庭教育的机制等,构建符
网格数据库是数据库技术和网格技术相结合后新的研究领域，网格的动态变化特性对数据库查询优化技术提出了适应性的要求。本文提出了基于Petri网描述的子查询计划模型TNSN，通过
乡村振兴与精准扶贫战略在目标上高度契合、在内容上一脉相承、在实践上纵深递进,两者具有顺承、紧密的内在逻辑。但是,审视两大战略衔接发展现状,发现存在参与主体差异、衔