一、測試與正確性論證

　　a) 程序測試是指對一個完成了全部或部分功能、模塊的計算機程序在正式使用前的檢測，以確保程序能按預定的方式正確運行。測試用例由測試數據和預期結果構成，高效的測試應用盡量少的測試用例發現軟件儘可能多的錯誤。但程序測試只能發現錯誤，測試用例全部通過仍不能證明程序的正確性，窮舉測試（窮舉所有情況）幾乎是不可能的，同時將耗費大量時間和精力。

　　b) 正確性論證是從邏輯上論證程序的正確性，使用數學推理來嚴格論證程序是否符合其目標。正確性論證可靠性與穩定性更強，但論證過程的完備性和正確性隨代碼規模增大、功能擴展越來越難以保證。

二、OCL語言

　　OCL是英文Object Constraint Language的縮寫，又稱對象約束語言。它作為圖形符號的補充，是一種形式化的無二義的語言，説明了建模元素的有關細節，如約束、前置條件、後置條件等。

　　OCL的原則：

　　　　①聲明性語言，不會改變模型中的內容。

　　　　②形式化語言。

　　　　③無二義規範語言。

　　　　④類型性語言，每一個表達式都有類型。

　　　　⑤易學好用。

　　OCL與JSF：

　　　　①相似之處

　　　　　　二者説明了建模元素的有關細節，如約束、前置條件、後置條件、不變量等；都是表達程序運行對系統狀態的更改而非具體的算法邏輯流程；目的相似。

　　　　②不同之處

　　　　　　OCL的表達式由操作數和運算符按一定規則構成，表達式和特定上下文有關，具有特定的值和類型。JSF的表達式主要是布爾類型，可以視為輕量級的OCL；OCL的語法定義較之JSF更加全面、精準、無二義，可以看作JSF的升級版。

三、UML

1.UML類圖

2.順序圖

 

3.狀態圖

 

 

四、總結

1.四個單元模塊的知識點聯繫

　　 第一單元練習任務是多項式計算和電梯程序，通過寫代碼基本掌握java語法規則，是基礎知識掌握篇。

　　第二單元引入多線程，主要練習用共享對象協調線程間的並行關係，是進階升級篇。

　　第三單元開始學習規格化程序設計，學會用JSF等語言規範約束方法行為，是工程設計篇。

　　第四單元重心在自動測試，練習使用了JUNIT，掌握語句覆蓋、分支覆蓋等基本概念，瞭解測試的方法和方向，並按照一定步驟論證了程序設計的正確性，是測試證明篇。

2.程序分析

 　　程序設計方面，開始有意識避免過長方法體出現，均衡的劃分各個類之間的職責關係，處理好對類的私有屬性的保護，在設計之前明確可能對共享對象操作的各個類和大概操作方法。

　　程序功能方面，儘可能將功能劃分細緻，降低耦合度，不同功能劃分給不同類的不同函數實現，是程序精簡、利於修改和維護。

　　測試方面，學會利用分支樹劃分輸入組合，結合junit視線自動化測試。

3.對工程化開發的理解

 　　工程化開發思想在大型軟件項目開發中十分重要，它利用某些約束規範在不同羣體中達成共識，將工程劃分成不同羣體的協作任務，不僅有利於加快開發速度、提升開發質量，而且由於約束規範的存在，後期對程序的升級加工、後期維護也將方便許多。

4、課程建議

　　希望在課程初次學習到繼承、接口、同步等概念時，配套的練習任務和需要練習的相應概念之間的關係能更加清晰、一目瞭然。比如接口實現，在電梯任務中並非必要用到接口的概念，而且感覺抽象出的接口功能也很模糊，不同人可能有很大差異。部分人只是簡單寫了一個interface，並沒有在程序中使用到，也不是很理解這個接口存在的意義，個人感覺這樣的練習不能很好達到預期目標。