測試與正確性論證：

測試的目的是將程序的代碼做到全覆蓋，從而確保每個分支都運行一遍，進而分析代碼中是否有錯誤，錯誤出在哪裏。這個方法是實用的，但不是完備的。而正確性論證則通過大量的窮舉，基於repOK和jsf來論證正確性，是邏輯層次的，可以說絕對正確，但相對復雜。私以為，二者的區別在於，測試可以說明沒找到錯，論證說明是對的。

對象約束語言：

OCL(object constraint language)對象約束語言，一種用來進行約束定義的，形式化的無二義的語言。包含四種基本語言要素：

1. 類型(基本類型，高級類型)
2. 操作
3. 表達式(由操作數和運算符構成)
4. 語句

它是UML可選的附加內容，可以用來更好地定義對象的行為，並為任何類元指定約束。在對象約束語言中，對象代表了系統的組件，它定義了完善的項目，約束代表限制。

OCL是一種形式語言，可以應用於任何實現方式的非正規語言。它對UML中圖形或其他組件都沒有控制權，它只是在使用時返回值。OCL並不能修改對象的狀態，而是用來指示對狀態的修改何時發生。OCL表達式以附加在模型元素上的條件和限制來表現對該對象的約束，其中包括附加在模型元素上的不變量或約束的表達式、附加在操作和方法上的前置條件和後置條件等。

相比JSF，OCL中涉及到上下文，不變量等一系列規範，相比我們所使用的JSF更加復雜和精細化，OCL中本身定義了基本數據類型和一些高級數據類型，還有運算符和表達式中的一些書寫規範，幾乎算得上是一種編程語言。（然而並不是）

OCL和JSF中都有對前置條件和後置條件的說明，都是不具有二義性的，可以說JSF是一種簡化以及自由化了的OCL。

學期總結

知識點聯系

　　第一單元主要是一些設計思想，類，接口，繼承等，第二單元是多線程的共享數據管理和沖突解決，第一章是必要的基礎，只有封裝好每個類，才能實現更好多線程的程序。第三單元是規格化設計。第四單元是單元測試和正確性論證，根據規格對每個方法進行測試和覆蓋率檢查，對每個類進行正確性論證。

設計的程序

　　多項式加減

　　傻瓜單電梯

　　可捎帶單電梯

　　可捎帶多線程電梯

　　出租車調度

　　可開關道路的出租車調度

　　可開關道路和帶有紅綠燈的出租車調度

　　可開關道路和帶有可追蹤出租車和紅綠燈的出租車調度

　　寫多項式作業時，初次接觸面向對象，寫得很面向過程。在之後的系列作業中，由於本身功能實現具有難度，雖然對一些類進行了封裝，但是仍然沒有實現功能的劃分，於是每次作業都在對之前的作業進行大改（直到出租車才有所改善）。從電梯到出租車的系列作業，從簡單的兩三個類到十幾個類，在設計上已經能夠嘗試去遵循SOLID設計原則。

　　在測試上沒什麽太大進步。。。大概是是從胡亂測試到了根據測試樹構造數據？

　　而程序的質量是仍然有很大的進步空間的，人懶寫的又少，還是要多練才行（下周一定又開始努力）。

工程化開發

　　了解不深，也無法實現工程化。過短的作業周期，過大的作業壓力，過迷的指導要求，光是活下來都已經舉步維艱，還指望什麽舞姿優雅。

期望和建議

望越辦越好。

第四次博客