第四次博客

測試與正確性論證：

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

 

對象約束語言：

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

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

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

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

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

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

 

學期總結

 

知識點聯繫

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

設計的程序

　　多項式加減

　　傻瓜單電梯

　　可捎帶單電梯

　　可捎帶多線程電梯

　　出租車調度

　　可開關道路的出租車調度

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

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

 

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

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

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

 工程化開發

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

 指望和建議

       望越辦越好。