【摘 要】
：
为了使开发出的程序更具有可靠性,研究了两种正确性验证的演算方法,Dijkstra的最弱前置谓词变换法和Hoare的公理化方法。针对于Hoare公理化方法证明中的前置条件难以寻找的问
【基金项目】
：
基金项目：国家自然科学基金项目（90718009）,贵州省科学技术基金项目（黔科合J字[2009]2123）.
论文部分内容阅读
为了使开发出的程序更具有可靠性,研究了两种正确性验证的演算方法,Dijkstra的最弱前置谓词变换法和Hoare的公理化方法。针对于Hoare公理化方法证明中的前置条件难以寻找的问题,提出了将这两种演算方法结合使用的方法。对最弱前置谓词变换法的过程进行分析,确定了最弱前置谓词算法的准确性。将最弱前置谓词应用到公理化方法中,即把最弱前置谓词变换法求出的前置谓词作为公理化方法的前置条件。通过一个具体实例,详细说明了其验证过程,并证明了该方法的有效性。
其他文献
为实现考古遗址空间信息的开放式管理和可视化查询功能,提出一种基于XML和MapInfo技术的解决方案,并在.NET平台下设计实现了一个考古遗址空间信息系统ASIS。在阐述了该系统的
网络流量异常指的是网络的流量行为偏离其正常行为的情形，异常流量的特点是发作突然，先兆特征未知，以在短时间内给网络或网络上的计算机带来极大的危害。因此准确、快速地检测网
实时协同编辑系统作为CSCW的一个重要应用，近年来得到广泛研究。对目前协同编辑并发算法的研究现状进行了探讨，比较了国内外现有协同编辑并发算法，包括dOPT、adOPT、SOCK2、SOCK