Floyd不变式断言法在程序设计教学中的应用

《程序设计》是计算机专业学生的必修课程,教师非常重视对学生程序设计能力的培养。然而现有的程序设计教材未阐明程序和给定问题之间的关系,导致学生无法理解程序设计的本质。文章提出采用Floyd不变式断言法分析程序,并通过两个实例进行说明。教学实践证明,采用这种方法有助于学生理解程序。

随机Petri网模型到马尔可夫链的转换算法的证明

随机Petri网具有很强的模型描述能力,马尔可夫链是一种常用的性能分析模型.为了有效利用随机Petri网进行性能的定量分析,给出了一个详细完整的随机Petri网模型转换为同构马尔可夫链的算法.运用Floyd不变式断言法证明了算法的部分正确性,运用良序集法证明了算法的终止性.算法是部分正确的且是可终止的,这个证明结论说明算法是完全正确的.为了佐证证明结论,基于Java和SQL Server设计开发了一个软件平台,在此平台上实现了转换算法,测试实例的测试结果验证了算法的正确性.对算法时间复杂性的分析表明算法是有效的.

关于程序正确性证明的进一步探讨

本文介绍了什么是程序的完全正确性、部分正确性、终止性,并通过实例,介绍了利用不变式断言法和计数器方法分别证明程序的部分正确性和终止性的具体方法步骤。