Ｆｌｏｙｄ不變式斷言法在程序設計教學中的應用

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

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

0 引言

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

1 Floyd不變式斷言法

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

(1)建立斷言。一個程序除了要建立輸入、輸出斷言外，如果程序中有循環出現，還要建立相應于該循環的不變式斷言，即在循環中選取一個斷點，在斷點處建立一個適當的斷言，使循環每次執行到斷點時，斷言都為真。

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

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

2 舉例說明

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

2.1最大公約數問題

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

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