摘要：《程序设计》是计算机专业学生的必修课程，教师非常重视对学生程序设计能力的培养。然而现有的程序设计教材未阐明程序和给定问题之间的关系，导致学生无法理解程序设计的本质。文章提出采用Floyd不变式断言法分析程序，并通过两个实例进行说明。教学实践证明，采用这种方法有助于学生理解程序。
　　关键词：不变式断言法；程序正确性证明；最大公约数问题；自然数的平方根问题
　　
　　0　引言
　　
　　《程序设计》是计算机科学技术专业学生的必修课程，它同时也是一门基础课程，在教学过程中，教师都会非常重视对学生程序设计能力的培养。但作者在实际教学中，发现很多程序设计课程的教材均只给出了解决给定问题的程序，而没有给出这个程序为何能解决问题的分析过程。多数学生由于不明白程序和问题之间的关系，因而也就无法理解程序设计的本质，有些程序只能靠死记硬背。作者认为，若采用Floyd不变式断言法理解程序将能加深学生对程序设计本质的认识，很多精妙算法也就不难掌握了。
　　
　　1 Floyd不变式断言法
　　
　　不变式断言法是R.W.Floyd提出的，它是程序正确性证明的基本方法。利用不变式断言法证明一个程序的部分正确性时，通常分为以下3个步骤：
　　(1)建立断言。一个程序除了要建立输入、输出断言外，如果程序中有循环出现，还要建立相应于该循环的不变式断言，即在循环中选取一个断点，在断点处建立一个适当的断言，使循环每次执行到断点时，断言都为真。
　　(2)建立检验条件。在循环中建立断点后，程序执行中所有可能的通路就可以分解为几条有限的通路。对每一条通路建立一个检验条件，即程序运行通过该通路时应满足的条件。
　　(3)证明检验条件。即证明步骤(2)中的所有检验条件，如果每一条通路检验条件为真，该程序是部分正确的。
　　
　　2　举例说明
　　
　　下面引用两个例子来说明Floyd不变式断言法在《程序设计》课程教学中的作用。
　　2.1最大公约数问题
　　以下这个程序完成的功能是求两个非负整数x，y(x，y不能同时为0)的最大公约数。这个算法很多学生都无法真正理解，为何一个如此简短的循环可以求出任意两个非负整数的最大公约数呢?本人在实际教学过程中发现，若采用Floyd不变式断言法对此程序进行分析，学生将能深刻理解此算法，同时也提高了学生理解程序设计本质的能力。
　　
　　注：“本文中所涉及到的图表、注解、公式等内容请以PDF格式阅读原文”