1 測試與正確性論證的比較

　　測試和論證都是驗證程序正確性的方法。

　　測試是在一組測試用例上執行一個程序，並將實際結果與期望結果進行比較以揭示錯誤的存在，但不會精確地揭示錯誤所在之處。如果可能輸入的集合很小，進行徹底的測試時可能的，但如果輸入集合非常大，則徹底的測試時不可能的。測試的優點是易於實施，工程廣為采用，缺點在於其不能完全確保程序的正確性。

　　論證針對格式化的規格和代碼實現，人工方式對代碼邏輯進行分析，確認是否正確。論證可以對代碼進行全面地分析，可以確定錯誤的存在範圍。論證是形式驗證與自然語言層次邏輯推理的結合，缺點是無法確保自然語言層次邏輯推理的嚴謹性。

2 OCL與JSF的比較

　　UML圖表例如類圖可用於描述規格，但還不足以描述規格的全部內容。對象建模中需要描述對對象的約束條件，通常用自然語言來描述。由於自然語言總是有二義性的，人們就使用無二義性的形式化語言，形式化語言對數學要求較高，對普通的從業人員來說有一定難度。OCL就是在這樣的背景下誕生的，OCL也是形式化語言，但它易於閱讀和編寫，並且語義清晰。

• OCL是形式化語言，有規範的類型、操作、表達式、語句的定義，不使用自然語言描述。JSF是半形式化語言，可以使用自然語言。
• OCL表達式的值可以有不同的類型，JSF表達式的類型都是布爾型。
• OCL和JSF都可用於描述規格的前置條件和後置條件。

3 UML圖

類圖

順序圖

狀態圖

4 總結

4.1 知識點總結

　　1 一元多項式加減運算

1) 初步認識面向對象程序的結構特點

2) 區分過程式程序與面向對象程序在結構上的主要差異

3) 初步認識面向對象程序的運行行為和調試

4) 初步認識輸入處理與程序魯棒性的關系

5) 初步掌握結構化輸入的處理技巧

　　2 單部電梯運行控制

1) 如何把程序功能“均衡”分配給多個類

2) 如何讓多個類之間進行協同

3) 初步熟悉基於隊列的調度

　　3 具備捎帶功能的單部電梯

1) 進一步理解調度邏輯及其設計

2) 開始掌握如何使用繼承構造邏輯處理層次

3) 進一步訓練類的均衡設計

4) 開始了解針對狀態的測試設計

　　5 多電梯調度系統

1) 理解和實踐線程交互

2) 線程交互模式識別

　　6 文件監控程序

1) 識別程序並發特征

2) 實踐線程的主從協同模式

3) 基於鎖的線程同步設計

4) 實踐線程安全設計

5) 使用代碼進行測試

　　7 模擬出租車的乘客呼叫與應答系統

1) 實踐面向對象分析

2) 認識和實踐線程交互的動態性

3) 實踐線程工作狀態控制

4) 實踐設計原則

5) 繼續實踐線程安全設計

　　9 前一次作業增加道路打開關閉功能

1) 熟悉過程規格的內涵和書寫

2) 初步實踐基於規格的方法實現

3) 實踐基於異常處理的防禦編程

4) 初步實踐基於過程規格的測試設計

　　10 前一次作業增加紅綠燈功能

1) 熟悉類規格的內涵和書寫

2) 實踐基於規格的類實現

3) 實踐契約式設計方法

4) 初步實踐基於類規格的測試設計

　　11 前一次作業增加新的類型的出租車

1) 實踐類型層次下的規格設計

　　13 針對第三次作業的Junit測試

1) 設計測試數據

2) 設計測試場景

3) 基於規格設計測試

　　14 針對第三次作業的正確性論證

1) 軟件正確性內涵

2) 類實現的正確性論證

3) 方法實現的正確性論證

4) 子類實現的正確性論證

　　每次作業的關鍵要點用藍色粗體字標出。

　　第一單元(1-3)初始面向對象，掌握類、繼承等基本概念，練習均衡設計、類間協同。

　　第二單元(5-7)掌握線程設計、線程安全以及設計原則。

　　第三單元(9-11)學習規格設計的方法。

　　第四單元(13-14)練習程序測試、程序正確性論證。

　　每個單元的知識點相對獨立又相互聯系，例如第四單元的代碼測試，在前三個單元都有所涉及，又如第二單元設計原則，在第一單元的均衡設計部分有所體現。四個單元內容層次分明，循序漸進，從開始的面向對象基礎，到進階的線程設計，再到更高層次的設計原則與規格化設計，最後到程序的測試與論證，構成了一個統一的體系。

4.2 進步

　　在設計上，一開始毫無頭緒(很慶幸做第一次作業時看到了教材上的部分代碼)，後來漸漸地能夠理清要求，尋找出其中的對象，對象間的關系。測試上，最初是想到什麽測什麽，沒有邏輯，後來能夠按照分類樹劃分輸入，分類測試。

4.3 對課程的期望

　　作業上我覺得可以有一次獨立的規格設計作業，從設計，編寫規格，到實現作為一個完整的過程。 第9、10、11次作業是在已有實現的基礎上補充規格或者增加新的方法和規格，如果有一次一開始就用規格化設計的作業，也許能加深對規格化設計的理解。

　　每次作業的答疑如果能統一就好了，如減弱微信群的答疑功能，只在gitlab網站上答疑，並且對作業發布後的變化用單獨的一個版塊來更新。不然，同學們既需要關註微信群，又要閱讀所有的答疑帖才能知道作業要求的改變，耗費時間精力。

　　除了講課和作業的制定上，老師可以參與更多，例如在gitlab上答疑等。“OO不易，和諧6系”這句話可能蘊含著一種較強的對立關系，如果老師的更多參與能夠給同學以引導，更多關註學習本身，而不是如何團結起來應付課程組，或許有更好的效果。

　　如果有同學與老師或助教的面對面答疑時間就更好了，這樣對同學和助教的能力應該都有提升。

5 感謝老師們的認真工作，助教們日日夜夜的陪伴、辛勤的付出，和同學們的熱情參與！

面向對象設計與構造第四次總結作業