測試與正確性論證

Dijkstra說過：“程序測試只能證明程序有錯，不能證明程序正確。”所謂程序測試，實際上是測試者特意挑出一批檢查數據，通過運行程序，檢查每個輸入數據所對應的運行結果是否符合預期要求。正確性證明是論證程序達到預期目的的一般性陳述，該論證不與程序輸入的特定值有關，但能夠代表窮舉性測試。

測試相比於正確性論證來說，實際像是將程序看作一個黑盒，並不關註程序內部的實現。測試不僅能快速地發現程序的bug，也能測試程序的效率，復雜度等屬性。但是缺點在於需要大量的數據，想要做到全覆蓋測試並不容易，甚至在很多情況下根本無法實現。

而正確性論證則不一樣，如果說測試是從實踐方面來檢測程序的正確性，那麽正確性論證則是從理論上來證明程序的正確性。正確性論證在理論上來說可以覆蓋整個程序，從而證明整個程序的正確性。比起測試來說，由於是從理論上來證明程序的正確性，因此所需要的資源相對較少。但是其缺點也比較明顯，首先，正確性論證是從實現的角度去論證程序的正確性，只能證明程序實現的正確與否，如果程序一開始的設計就是錯的，那麽正確性論證不能發現這個問題。其次，當一個方法的實現過於復雜時（比如一個方法的代碼超過了50行），正確性論證難以進行。

OCL與JSF

對象約束語言（簡稱OCL）是一種指示用戶建模系統中的限制方式。UML圖通常不夠精細，無法提供與規範有關的所有相關部分。這其中就缺少描述模型中關於對象的附加約束。OCL便是為了解決這類問題應運而生的形式語言。

與JSF相比，雖然兩者都是一種約束語言，但OSL語言是一種無二義性規範語言，並且每一個表達式都有自己的類型。JSF的主要服務對象是方法，而OSL的主要服務對象是每一個類。

第十四次作業

學期總結

不知不覺間已經度過了一個學期的漫長而痛苦的OO旅途。雖說痛苦，但是收獲滿滿。

第一個單元，我們的主要目標是形成面向對象編程的思想。以前所學過的編程語言C語言是典型的面向過程的編程語言，而新接觸的Java語言則是一款面向對象的編程語言，這一單元主要是讓我們熟悉面向對象的編程思想，並且以典型的電梯程序來輔助練習。這一過程中，主要的問題是對Java語言的不熟悉，難以理解面向對象的編程思想。

第二個單元是針對多線程編程的訓練。用一句通俗的話說，這一個單元是最折磨人的。首先在於我們對線程絲毫沒有概念，也不懂得並發等術語的含義，因此在多線程編程中處處碰壁。其次，線程安全也是一個讓我非常頭疼的問題。在這一個單元中，主要出現的問題是如何設計，比如在出租車系列作業中，究竟是一個線程管理一百個出租車還是一百個線程管理一百個出租車方便實現？如何去保證出租車運行過程中線程始終安全？這些問題是當時一直困擾著我的。

第三個單元著重於規格化的設計。這一個單元的主要目的是讓我們意識到規格的重要性。盡管JSF一直在被吐槽，盡管大家對測試時測試者對JSF的扣分十分厭惡，但是，這一個過程確確實實讓我們了解了規格的重要性。規格不僅僅方便了程序的使用，它還能夠讓其他人更容易弄懂你的程序，這對於開發者來說十分重要。

第四個單元的重要任務便是測試和正確性論證了。到了這個單元，大家都已經能夠理解面向對象的編程思想，也能寫出相應的代碼。但是如何保證自己寫的代碼是正確的呢？這一單元針對代碼的測試和正確性論證幫我們解決了這個問題。也讓我們能夠寫出完善健全的代碼。

回看自己寫過的歷次作業，我發現自己的提高還是很明顯的。最初的我寫的代碼，完全是面條式的，如今的代碼，具有了相當程度的可移植性。針對測試，已經學會了將輸入輸出劃分，以形成分類樹來對程序進行測試。

至於工程化開發，我的理解是首先開發者在設計方面要遵循一定的原則，其次要寫出可移植性高，可修改性強的代碼，便於修改和完善。再次對每個類每個方法的實現要規格化，方便測試。最後的測試階段中，要盡量按照測試的分類樹進行測試，盡量實現全覆蓋的測試。

我們經常說的一句話是OO不易，和諧6系。其實我覺得這和課程組有很大的關系。很大的原因是互相測試導致的。有一句網絡語是這麽說的：“我就這樣了，有本事你順著網線來打我啊？”的確，匿名的互相測試確實讓某些同學過於“為所欲為”，周五測試結果出來之後，看到被報的BUG又要與測試者爭論許久，最終還得靠課程組的仲裁。既破壞了同學間的關系又加大了同學和課程組的壓力。

我認為一個很好的解決方法是加大公測力度，減少互測在分數中所占的比例。實話說，互測有很強的主觀性，公測才是真正公平的。但很多次作業公測，弱的驚人，把分數完全交給測試者，難怪同學們都說這是面向運氣編程。

雖然怨言不少，但始終還是希望OO課程能越來越好吧，也希望這門課能成為北航計院的特色課程（雖然已經是特色課程了）。

OO最後一次總結