一、測試與正確性論證效果的差異及其優缺點

在第十三次作業中，我們使用了JUnit單元測試框架對我們在第三次作業中編寫的捎帶電梯程序中的每一個方法進行了測試。捎帶電梯程序在經過了互測之後，已經是一個比較完善的系統，但是通過大量細致的單元測試，仍能從程序中尋找到一些邏輯漏洞甚至錯誤。通過觀察每個方法的語句和分支覆蓋率，可以比較直觀地看到自己的代碼是否每一行都有其價值。在寫第十三次作業的過程中，我不止一次遇到了這樣的情況：在針對某一個復雜的方法設計大量測試用例，甚至用程序自動生成隨機測試樣例，都無法對某一條語句或者某一個分支做到100%的覆蓋。這個時候，我就會重新檢查這個方法的實現邏輯，判斷這條語句或者這個分支是否真的有存在的必要。很顯然，細致的單元測試有助於我們優化和完善自己的代碼。

而在第十四次作業中，我們采取了正確性論證的方法對同一個捎帶電梯程序進行了正確性分析。通過對JSF的後置條件進行劃分，將一個方法所需要處理的所有情況分為幾種小的分支，然後對這些小分支逐一審視代碼的實現是否滿足了JSF的後置條件。在JSF後置條件明確且可驗證的基礎上，正確性論證可以使我們重新審視自己的代碼，細致地分析其實現邏輯，並確認自己是否覆蓋了每一種可能的情況。由於第十四次作業是在第十三次作業完善後的程序之上完成的，因此正確性論證沒有幫助我找到代碼中的邏輯漏洞；但它驅使我完善自己的JSF後置條件，並且對規模較大的方法進行拆解或重構，以達到可進行正確性論證的目的。從這個角度上來講，正確性論證進一步優化了程序的可驗證性。

單元測試和正確性論證的本質差異其實用一句話就可以概括：單元測試是黑盒測試，而正確性論證是白盒測試。

在構造單元測試的測試樣例時，測試者可以完全不知道程序的具體實現細節，機械化地生成測試數據，並根據方法的規格判斷方法的實現是否正確。它的好處是簡單粗暴快速有效，經過大量測試數據的轟炸，代碼中最細微的漏洞也可以被揪出來並得以修正。此外，單元測試對代碼的重構具有奇效。如果沒有自動化的單元測試，重構代碼的時候就需要不停地去手動驗證之前的測試樣例，一旦發現問題，修改之後又要重頭跑，既浪費時間，又容易出錯。單元測試有助於程序設計者以自動化的方式去驗證程序的正確性，這是正確性論證所不具備的優點。但是，單元測試也有其缺陷：由於它是黑盒測試，從概率的角度上講，無論測試數據再怎麽完善，總會有漏網之魚的Bug出現。換句話說，在程序有一個良好的設計且規格完善的前提下，單元測試可以保證程序的正確率達到99%以上，但無法確保100%正確。

正確性論證與單元測試不同，它是白盒測試，這意味著測試者需要深入代碼的實現，去逐個論證實現與規格上的不同之處。這個過程比較繁瑣，而且對重構極不友好，一旦代碼發生較大的變動，許多方法的正確性論證就要重寫，造成很多額外的麻煩。但是，這些麻煩換來的好處就是，一個被正確設計了的且規格完善的程序只要完成了正確性論證，就可以從邏輯上確保100%的實現正確性，其保證力度要大於單元測試的保證力度。因此，對於一些不再需要進行修改的方法，進行正確性論證是比單元測試更為穩妥的選擇。

在實際的工程中，我認為應以單元測試為主，正確性論證為輔。因為需求總是在不斷變動的，單元測試的簡便和高效適合更現代軟件工程的開發流程。而對於那些比較重要的核心算法代碼（即不會隨需求更改而變動的代碼），應進行正確性論證，以確保邏輯上的100%準確。

值得註意的是，無論是單元測試還是正確性論證，其有效的前提都是程序的設計是合理且正確的，各個類和方法的規格也都已經完善。沒有規格的代碼就像沒有標準答案的考試卷，學生答起來群魔亂舞，老師判起來無從下手。單元測試和正確性論證都是必要的，但這並不代表有了它們就可以萬事大吉。在軟件開發環節的最開始就做出合理的設計，並且撰寫好相應的規格，單元測試和正確性論證才能發揮其最大作用，為提高程序的正確性帶來價值。

二、OCL(Object Constraint Language)語言與JSF

OCL語言是約束(Constriant)語言和查詢(Query)語言。一個約束就是對一個（或部分）面向對象模型或者系統的一個或者一些值的限制，UML類圖中的所有值都可以被約束，而表達這些約束的方法就是OCL語言。在UML2標準中，OCL語言不僅能夠用來寫約束，還能夠用來對UML類圖中的任何元素寫表達式，每個OCL表達式都能指出系統中的一個值或者對象。因為OCL表達式能夠求出一個系統中的任何值或者值的集合，因此它具有了和SQL同樣的能力，因而OCL也是一種查詢語言。

OCL語言的基礎是數學中的集合論和謂詞邏輯，並且它有一個形式化的數學語義，但是它並沒有使用某種數學符號。因為雖然數學符號能夠清晰的、無歧義的表達事物，但是只有極少的專家可以看懂。所以數學符號並不適合用於一個廣泛應用的標準語言。自然語言是最易懂的，但它卻是含混不清晰的。OCL取了自然語言和數學符號的折中方案，使用普通的ASCII字符來表達數學中同樣的概念。

OCL是一個類型語言，任何表達式的值都是屬於一個類型的。這個類型可以是預定義的標準類型例如Boolean或者Integer，也可以是UML圖中的元素例如對象。也可以是這些元素組成的集合，例如對象的集合、包、有序集合等等。

OCL是一種聲明式(Declarative)語言，表達式僅僅描述了應該去做"什麽"，而不是應該"怎樣"去做。因為OCL是聲明式語言，所以UML中的表達式被提升到了純建模的領域，而不必理會實現的細節和實現的語言。

OCL起源於1997年BIM公司為響應OMG的"面向對象分析和設計標準"征求稿所提交的"對象時間限制提議"，OCL是該提議的部分內容。用OCL可以描述四類約束，分別是不變量、前置條件、後置條件和監護條件：

1）不變量是在屬性的生命期內一直保持為真的規則。

2）前置條件是在一個操作被調用時必須為真的約束。它是一個斷言，不是可執行語句。

3）後置條件就是在操作完成時必須為真的約束。它不是可執行語句而是斷言，必須為真。

4）監護規則是在對象能夠從一種狀態轉變為另一種狀態前其值必須為真的約束。

每一個OCL表達式都必須賦予一個明確的上下文來定義參考基準。在模型中的任何一個元素都可以定義為一個上下文，例如類、屬性、操作和關聯。一旦我們定義了上下文，就可以開始定義約束表達式餓。OCL是一種聲明式語言，大部分表達式執行後會返回一個布爾值，也有一些表達式會用來選擇一個單一值或者一個對象/值的集合。

可以看到，OCL語言和我們在面向對象課程中所學到的JSF具有相似之處。不變量、前置條件、後置條件這些我們已經耳熟能詳的概念在OCL和JSF中都有體現，其所代表的含義也都大致相同。OCL中的監護條件則有點類似於JSF中的repOK方法（但並不完全一致），即系統狀態只要滿足相關要求，就可以進行任意滿足規格的調用。通過對這些約束的斷言，我們得以判斷一個方法是否被正確調用或者是否被正確實現，相當於為一張空白的試卷制定了規則和答案。有了這些規則和答案，我們再去具體撰寫代碼實現的時候，就有了相應的依據，可以自行判斷出實現是否正確。此外，它們還可以幫助我們撰寫高質量的單元測試和正確性論證。

不同之處在於，OCL語言是基於UML類圖的，而JSF是基於代碼本身的。從嚴謹性程度上來講，JSF也更高一籌，因為正如上文所說，布爾表達式（以集合論和謂詞邏輯為基礎）是最嚴謹的表達，其帶來的約束的嚴謹性遠勝於自然語言，且適合進行自動化驗證。但是，形式化的數學語言並不適合所有人閱讀，而且一些較為復雜的邏輯可以用簡單的自然語言描述出來，但絕對無法用簡單的數學語言去描述。因此，OCL和JSF各有其適用範圍，兩者的缺點正好是對方的優點。在工程開發中，二者互補為佳。

三、單捎帶電梯系統的UML表示

四、學期訓練總結

1. 四個單元模塊知識點之間的關系

第一單元有三次作業：多項式加減、單傻瓜電梯、單捎帶電梯。第一次作業的難度極小，主要是為了讓同學們初步接觸Java編程，並將思維從C語言的面向過程轉為Java的面向對象。第二次作業的單傻瓜電梯稍有難度，相比於多項式加減，同學們需要設計並實現的類變多了，大部分同學在這次作業中第一次體驗到了多個類協作帶來的面向對象編程體驗。第三次作業的難度陡然增加，指導書變得復雜了許多，算法也比較難以實現。尤其是同學們在寫單電梯的時候還需要考慮之後的多線程電梯，因此寫的時候小心翼翼、舉步維艱，生怕後面還需要重構（然而事實證明，多線程電梯還是需要大規模重構…）。

第二單元可以說是整個課程體系中最難的一個單元。多線程的首次引入、指導書的繁雜、調試的不便、互測的博弈，這些元素使得這三次作業的難度陡然增加。第五次作業的多線程電梯中，同學們需要通過多線程完成三部電梯的協作，並在捎帶算法的基礎上增加最小運動量原則。這些算法和之前的差別不大，難點在於多線程對調度器實現方法的影響。第六次作業是文件監視器，是指導書改動最頻繁的一次，絕對難度並不大，復雜之處在於仔細理解指導書，並完成一個線程安全的設計。第七次作業的出租車調度是一系列作業的開始，這次作業中首次引入了設計原則，通過滿足這些設計原則，同學們可以在之後的增量設計中取得工作量上的減輕。

第三單元主打JSF。第九、十、十一次作業循序漸進，逐步引入方法規格、類規格、帶有繼承的類規格，讓同學們可以通過完善規格，掌握做出一個良好設計的方法。這三次作業的難度不大、算法簡單，但是要想寫好JSF還是需要下一定的功夫。

第四單元是測試與論證。一個程序如果沒有正確性，那就不配稱之為一個程序，第十三次作業的JUnit單元測試和第十四次作業的正確性論證是兩種增加程序正確性的方法，通過這兩次作業對第三次作業單捎帶電梯的檢查，同學們基本掌握了測試和驗證自己程序的方法，這種方法在之後的編程生涯中大有裨益。

這四個單元有一個清晰的主線：熟悉面向對象 à 多線程編程 à 設計與規格 à 測試與驗證。這條主線是從一個對面向對象完全沒有概念的編程新手到能寫出1000行具有優良設計風格的面向對象代碼的人所必經的學習道路。四個單元之間循序漸進，卻又藕斷絲連，對同學們而言有著很大的訓練價值。

2. 我的進步

在面向對象課程中，我的主要進步可以用一句話來概括：從拿到需求（題目）就開始無腦寫代碼，變成了先思考再編碼。我覺得大二整個課程體系（包括但不限於計算機組成、面向對象）都是在訓練我們設計與實現分離的編程風格，事實上經過這一年的訓練，我的設計能力和編碼能力確實有了長足的提高。

此外，還有一些小的方面的進步。例如，以前我從未接觸過多線程編程，也沒有使用過Java的反射，面向對象課程的作業讓我熟悉並掌握了這些很有用的編程工具。

3. 對工程化開發的理解

我並沒有參與過真正的工程化開發，因此接下來這一小節的內容都是基於我的想象。

我理解的工程化開發，重點在於協作。現代大型的軟件工程規模已經大到了絕對不可能僅靠一個人單槍匹馬就能完成開發，因此多人協作就顯得尤為重要。當許多人一起完成一個大型項目的時候，由於每個成員的能力不同、對項目的理解也不同，因此如何進行良好的溝通（包括語言層面的溝通和代碼層面的溝通）成為了一個很大的問題。面向對象這門課程所教授的規格化設計就是解決溝通問題而進行的一個嘗試。類的設計者通過規定前置規格來約定使用者的輸入參數範圍，通過撰寫後置規格來提示使用者類和方法調用後的作用；類的使用者通過遵循前置規格來獲得滿足後置規格的調用結果，通過反復調用repOK方法獲得類是否能夠正常工作的反饋。

"協作"這個詞的內涵是豐富的。為了溝通方便，完善的註釋和優秀的代碼風格是必需的，各種設計原則的滿足是必須的，規範撰寫的過程規格也是必需的。如果沒有這些，一個人無法理解另一個人的想法，無法對代碼作出修改和重構，即使是代碼撰寫者自己，也會在一段時間之後，忘記之前代碼的設計思路。因此，在工程化開發中，為了溝通和協作的需要，更多的時間應該花在規劃、設計和測試上，真正的編碼實現只占整個工程的一小部分。

工程化開發和自己做一個小項目完全不一樣。在自己的項目中，任性沒有關系，甚至有時候任性能夠來帶來更好的創意；然而在工程化開發中，任性只能給整個團隊帶來災難。

4. 對課程的任何期望或建議

希望能夠取消後面三次的出租車作業（即第三單元的三次以JSF為主要訓練目的的作業），改為一個從零開始的、先撰寫規格再完善代碼的循序漸進的項目。在現有的課程體系中，同學們接觸JSF的方式是通過先寫代碼再補充規格的方式，這使得大部分同學難以體會到規格化設計對於一個工程項目的重要性。如果能夠通過一個系列作業，讓同學們完整體會先設計再實現的過程，想必"設計無用論"的想法會少很多。

此外，在互測制度上，建議再完善一下JSFTools，為JSF制定一個統一的規範標準，以避免互測雙方對JSF標準的理解不同而引發的爭論。

最後，希望面向對象課程能變得越來越好，而不是讓越來越多的人去討厭。

面向對象第四單元訓練總結