摘要：《程序設計》是計算機專業(yè)學生的必修課程，教師非常重視對學生程序設計能力的培養(yǎng)。然而現(xiàn)有的程序設計教材未闡明程序和給定問題之間的關系，導致學生無法理解程序設計的本質(zhì)。文章提出采用Floyd不變式斷言法分析程序，并通過兩個實例進行說明。教學實踐證明，采用這種方法有助于學生理解程序。

關鍵詞：不變式斷言法；程序正確性證明；最大公約數(shù)問題；自然數(shù)的平方根問題

0 引言

《程序設計》是計算機科學技術專業(yè)學生的必修課程，它同時也是一門基礎課程，在教學過程中，教師都會非常重視對學生程序設計能力的培養(yǎng)。但作者在實際教學中，發(fā)現(xiàn)很多程序設計課程的教材均只給出了解決給定問題的程序，而沒有給出這個程序為何能解決問題的分析過程。多數(shù)學生由于不明白程序和問題之間的關系，因而也就無法理解程序設計的本質(zhì)，有些程序只能靠死記硬背。作者認為，若采用Floyd不變式斷言法理解程序?qū)⒛芗由顚W生對程序設計本質(zhì)的認識，很多精妙算法也就不難掌握了。

1 Floyd不變式斷言法

不變式斷言法是R.W.Floyd提出的，它是程序正確性證明的基本方法。利用不變式斷言法證明一個程序的部分正確性時，通常分為以下3個步驟：

(1)建立斷言。一個程序除了要建立輸入、輸出斷言外，如果程序中有循環(huán)出現(xiàn)，還要建立相應于該循環(huán)的不變式斷言，即在循環(huán)中選取一個斷點，在斷點處建立一個適當?shù)臄嘌裕寡h(huán)每次執(zhí)行到斷點時，斷言都為真。

(2)建立檢驗條件。在循環(huán)中建立斷點后，程序執(zhí)行中所有可能的通路就可以分解為幾條有限的通路。對每一條通路建立一個檢驗條件，即程序運行通過該通路時應滿足的條件。

(3)證明檢驗條件。即證明步驟(2)中的所有檢驗條件，如果每一條通路檢驗條件為真，該程序是部分正確的。

2 舉例說明

下面引用兩個例子來說明Floyd不變式斷言法在《程序設計》課程教學中的作用。

2.1最大公約數(shù)問題

以下這個程序完成的功能是求兩個非負整數(shù)x，y(x，y不能同時為0)的最大公約數(shù)。這個算法很多學生都無法真正理解，為何一個如此簡短的循環(huán)可以求出任意兩個非負整數(shù)的最大公約數(shù)呢?本人在實際教學過程中發(fā)現(xiàn)，若采用Floyd不變式斷言法對此程序進行分析，學生將能深刻理解此算法，同時也提高了學生理解程序設計本質(zhì)的能力。

注：“本文中所涉及到的圖表、注解、公式等內(nèi)容請以PDF格式閱讀原文”