一、測試與正確性論證的比較

從方法上看，測試是使用大量測試樣例來覆蓋測試代碼，從而能夠檢測代碼的實現是否正確，功能是否完善。而正確性論證是使用代碼的規格和邏輯進行嚴密的推論和證明，從而驗證代碼的實現正確性。從優缺點來看，測試的優點在於能夠直觀地看出測試的結果是否正確，而缺點在於難以構造覆蓋完整的測試集；正確性論證的優點在於能夠保證正確性和覆蓋率，但是不夠直觀，而且論證錯誤不易察覺，也就是不易二次檢查。

因此，在對一個程序進行設計測試檢查的時候，需要二者同時使用，相互補充，使用測試集測試程序功能的完備性，使用正確性論證驗證代碼的邏輯正確性和嚴密的覆蓋所有代碼，這樣才能對程序進行充分的測試驗證。

二、OCL與JSF的比較

OCL，即Object Constraint Language, 中文譯為對象約束語言。OCL是一種用來在指定的模型單元上施加約束的語言。同時OCL也不僅用來寫約束，還能夠對UML圖中的任何元素寫表達式。OCL是約束和查詢語言，有一個形式化的數學語義，並且允許用戶定義自己的OCL符號集。

與JSF的相同之處：OCL和JSF都是形式化的語言，都有同樣的規格即前置、後置條件以及不變式。

與JSF的不同之處：JSF基本上使用的是邏輯表達式，少量使用自然語言。而OCL的表達式具有類型，且數據也有基本類型，這點和JSF有較大區別。

三、UML圖

類圖：

時序圖：

狀態圖：

四、學期總結

1. 知識點總結：

第一階段：從多項式加減到ALS電梯，一個入門的階段，主要的知識是面向對象編程的思想，以及java語言一些基礎的語法，比如正則匹配等等，較為簡單，屬於經驗怪，前期給玩家升級用的。

第二階段：從多線程電梯、IFTTT到第一次出租車作業，一個逐漸熟悉的階段。主要講解了多線程的機制，競爭和同步機制、文件監測和操作等等知識，同時對規格有了一定的要求，代碼質量也更高了。這屬於精英怪，對於在第一階段沒有花時間認真打怪升級的玩家來說，可能就會被這個階段的精英怪秒殺了，然後消耗一次復活（無效作業）的機會來從頭打怪升級，苦肝到深夜。

第三階段：對出租車進行功能上的完善，添加了許多功能。這個階段主要是對程序有了規格化要求的設計，包括JSF規格的書寫，和程序的規格化設計，在總體的代碼量上也有顯著提升。屬於boss級別的怪物，需要苦戰幾日，熬夜連戰，才能最後幹掉boss。

第四階段：這個階段的主要作業是對以往的代碼進行驗證和測試，以及正確性論證。雖然總體作業量小了很多，不用寫大量代碼，也不用構造復雜的結構。但是這個階段的知識是很重要的，放在課程的最後，重要性也不言而喻。

2. 個人總結：

從一開始的多項式加減，到最後的功能強大的出租車，總共9次編程作業，說多不多，說少不少，總而言之，對於我的編程能力還是有較大提升的。最開始的作業，對於面向對象的思想還是不夠理解，寫出來的程序只是有面向對象的外殼，但是實際上還是一個面向過程的程序，一個方法占了100多行，質量也不高，debug還十分困難。到最後幾次作業時，對面向對象已經有了比較深入的見解，對類和方法的區分比較嚴格，方法的代碼量也不多，嵌套深度也少了，把各個模塊和功能安排得比較明白，質量有了明顯的提升，debug也容易多了。盡管如此，但還是有一些不足的地方，需要更深入的學習。

3. 工程化開發：

我認為工程化開發就是，首先需要規範設計好每個功能的規格。然後將各個功能的實現分發給不同的程序員實現，團隊的各個成員負責自己的模塊，同時又可以相互協調合作，提高總體效率，降低成本。在此基礎上，良好的規格化設計和封裝是必要的，大部分程序需要實現大量的功能，這對於工程化開發是必不可少的條件。

4. 對課程的建議：

其實要說平時的吐槽倒挺多的，真要給實際建議的時候，還找不到幾條。首先就是指導書的問題，我相信絕大部分的同學都會提到這個，指導書寫的實在是很粗糙，對於一些細節上的問題，還有幾次作業的扣分點都交代得不清楚。有很多次情況就是，一些摸棱兩可的問題，一開始說readme自行定義，然後發現這些條件又是必要的，在提交作業前突然通知說要改指導書的內容，這讓很多同學心態會崩的。還有就是在issue裏提到要更改的地方，沒有正式的通知，最後詢問得到的結果是自己沒看issues。雖然有各種吐槽，但確實找不到更好的替代方法，包括互測的面向運氣得分機制。希望學弟學妹們能存活吧。。

OO終章--總結博客