Ｆｌｏｙｄ不變式斷言法在程序設(shè)計教學(xué)中的應(yīng)用

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

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

0 引言

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

1 Floyd不變式斷言法

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

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

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

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

2 舉例說明

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

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

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

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