论文部分内容阅读
关于Hanoi塔问题的非递归算法已有大量的研究.运用薛锦云教授自创的PAR方法和循环不变式开发的新策略,形式化推导出逻辑结构清晰的Hanoi塔非递归算法及其循环不变式,并用Dijkstra最弱前置谓词法验证了该算法的正确性.充分体现了PAR方法的优越性、高效性和可靠性.
Hanoi塔非递归算法的形式化推导和正确性验证
【摘 要】
：
关于Hanoi塔问题的非递归算法已有大量的研究.运用薛锦云教授自创的PAR方法和循环不变式开发的新策略,形式化推导出逻辑结构清晰的Hanoi塔非递归算法及其循环不变式,并用Dijk
【机 构】
：
江西省高性能计算技术重点实验室,江西师范大学计算机信息工程学院,江西师范大学计算机信息工程学院
【出 处】
：
计算机研究与发展
【发表日期】
：
2008年z1期
【基金项目】
：
国家自然科学基金项目(60273092)
其他文献
在借鉴异步电路技术的基础上,对传统三模冗余(TMR)结构进行了改进,提出了基于异步C单元的双模冗余(DMR)结构和基于DCTREG的时空三模冗余(TSTMR-D)结构. DMR结构每位只需两个
网络教学已经是教育信息化的主要途径之一，在网络教学中专业性的课程网站积极的促进教育信息化的发展。在动态的课程网站中页面都是由控件组成的，页面和控件都是对象。学生通过
网站提供了政策法规、办事指南、科普园地等功能，及时为镇安乡人民提供最新的计划生育信息，使百姓能及时了解计划生育政策法规，减少计划生育违纪现象。
针对高职院校发展迅猛，人才培养目标与实践相脱节，推进实践教学改革迫在眉睫，而教学与生产结合是发展的必然趋势，学校与企业合作又是产教结合的必经之路，而校企合作模式及组织管理
在共享存储环境中,传统全局缓存管理的两个缺陷:1)共享缓存空间的多个应用之间相互干扰,每个应用不能公正地共享缓存资源.2)总体的缓存资源利用率较低.设计了一种基于分区的