一、測試與正确性論證的差別
從哲學的角度來說，正确性論證與測試的關系就像理論與實踐的關系一樣。
使用測試的方法檢驗程式正确性确實是一個非常友善可行且廣泛運用的方法。可以通過幾個簡單或複雜的測試樣例，迅速地校驗程式主要邏輯是否正确，運作結果是否符合預期。但是對于較為複雜的問題來說，測試樣例很可能并不能覆寫所有的情況，是以我們曾經引入代碼覆寫率和分支覆寫率的概念。但是在操作過程中我發現，即使某個不完全的測試樣例代碼覆寫率達到100%，分支覆寫率高于95%，它仍然并不一定完全檢驗程式的邏輯是否正确，即使結果符合預期。是以我們很難通過測試樣例說明程式一定正确，即使我們使用了腳本生成等自動化測試方法，仍然不能全面地測試程式的邏輯是否完全正确。是以測試這樣的方法有着其便捷性，也有着其局限性。
正确性論證是一個全新的思路，我們把程式的邏輯構造成分支的形式，通過規格總結出在各個分支下程式的預期表現來從宏觀的邏輯層面上論證程式是否正确，不去關心程式運作過程中如何實作，隻需要滿足規格提到的前置條件和後置條件即可認為程式正确。但是對于複雜問題，建構出程式的邏輯分支便已經十分吃力，程式的複雜邏輯很可能在分析的過程中遺漏一些錯誤，是以這并不是一個萬全的方法。
我們在實踐中，應該結合二者進行測試，雖然耗費時間，但是在對程式認知較為深刻的情況下，自然更容易思考到比較偏僻和少見的邏輯問題。
二、OCL語言
OCL語言是對象限制語言，與JSF相似，同樣擁有着前置條件和後置條件，但是沒有JSF中的Modified屬性，有類似的不變式。還有叫做監護規則的限制，即在對象能夠從一種狀态轉變為另一種狀态前其值必須為真的限制。
OCL語言和JSF一樣，都隻關心方法或對象在運作前後的屬性狀态，不關心具體的實作過程。
三、第十四次作業總結
以上是第十四次作業的UML類圖。
以上是第十四次作業的時序圖。
四、學期總結
本學期我們首先學習了面向對象語言的初級應用，完成了一個看起來很不面向對象的Java程式——多項式計算，這個程式由于功能簡單，導緻其類的功能過于集中，Main類用于錄入資訊，ComputePoly類用來計算多項式加減，确實是難以感受到Java面向對象程式與傳統面向過程程式的差別（除了程式中多了幾個class關鍵字）。當然現在看來，這個程式還可以寫得更面向對象一點，更完美一點。但是對于一個什麼都不懂的初學者來說，用這個作業入門且由于設計需求中對輸入的嚴格要求，大家往往會把注意力集中在java的基本文法學習和正規表達式在Java中的運用之中，反而忽略了面向對象程式的關鍵。愚以為，這個作業可以進行一些改進以更加地偏向面向對象教學，不過考慮到由于需要公測進行測試，且規範輸入格式對之後電梯程式的鋪墊作用，設計出這樣的作業已經是非常合理了，且暫時也難以想到兼顧二者的作業設計，畢竟對于當時的我來說，面向對象還是一個非常抽象籠統的概念，是需要一個學期的學習才能正确認知的。
随後我們完成了兩次單線程電梯，第一個是傻瓜式電梯，之後我們運用了學到的類的繼承，将其更新為有一點點智能的可捎帶電梯。到這裡，我們已經可以管中窺豹地初步認識到Java面向對象中一大特性之繼承的作用以及好處，同時對單線程程式設計也是較為熟練。
之後我們便愉快地進入了Java多線程的世界，我們首先再次更新了之前的稍微智能一點的小垃圾電梯，将其改造為非常小可愛的三部電梯同時工作，并且直接進入了多線程階段，可以真實地模拟時間，簡直是太酷了！
這三次作業讓我們發現，在功能更新的時候，總是有一些其他無關類（如Floor類）的代碼由于一些不可言狀的原因必須進行修改，這是怎麼回事！明明很厲害的面向對象怎麼會有這種情況出現！難道是我做錯了什麼！原來随着需求的修改，程式的邏輯有了很大的變化，之前在樓層類中使用了一些屬性來記錄相應的請求，而在多線程電梯裡又用不到了，導緻這部分邏輯在方法中備援，才需要大量的修改甚至是重構。此時我們發現了，類的抽象化做的非常的不好！樓層就是樓層嘛，樓層有樓層的功能，為什麼還要用來記錄請求資訊呢（其實是因為要列印輸出），記錄請求資訊意味着類之間的耦合性變高了，這也就是我們必須要修改除去scheduler類之外的其他代碼的原因。
當這一作業告一段落，我們完成了一個用作過渡的，用來幫助我們學習多線程的線程安全和同步控制的作業——檔案系統。在這次作業中，我們學習了諸多線程安全的手段（有且不僅有sleep(200L), sleep(500L)和sleep(1000L)），極大地提升了自己線上程同步控制上的造詣。
在之後的Taxi作業，我們早早就聽說了本次作業将有多次更新，是以我在實作時很認真地思考自己的程式，如何讓自己的程式變成高内聚低耦合的神奇存在。又線上程控制上有了很深的認知，使這次作業的線程同步的沖突從設計層面上被盡量避免。同時又完成了需求提到的并不豐富的功能，其中最困難的部分可能是重新寫一個好用的最短路徑搜尋以替代原本GUI中提供的特别占記憶體且特别慢的方法吧。
之後不論是為道路添加流量還是添加紅綠燈還是設定VIP計程車，都極大地展現了一個良好的程式構思是多麼的有意義，添加流量時由于要修改map類的邏輯，包括最短路搜尋，導緻需要寫不少代碼，之後的紅綠燈幾乎隻修改了兩三個方法，修改了十幾到幾十行代碼就解決了這個問題。而可追蹤計程車更是完美的展現了面向對象程式中繼承的優點，程式的其他部分對可追蹤和普通計程車的處理完全沒有差別，卻可以很好地完成功能需求。再加上某個選修課學到的c++面向對象的相關知識，到這，我覺得面向對象程式中繼承的運用以及好處已經被我掌握個大概了。
從Taxi第二次作業開始，我們引入了全新的程式設計理念——規格，這個東西可以很好地統一程式員之間的交流語言，也可以為自己的程式設計提升便利。這一部分與我們之後的幾次作業有着極大的關聯。
之後的幾次代碼量非常小的作業中，我們先後接觸了JUnit單元測試、程式正确性論證等概念，這兩個概念令我對之前蠢笨的測試方法感到十分羞愧，想起當時百度的時候也曾經看到JUnit的使用方法但由于懶惰并沒有深入學習，導緻剛開始在對程式測試時，幾乎都在使用複制粘貼按回車大法。但是代碼量小并不代表作業更輕松，雖然當時的我在身體及意識上對它們都有些不重視，但是在實踐過程中，發現當初寫的程式簡直是太難以接受了，将這樣的程式整理出合适的規格實在是過于繁瑣。是以，迫不得已地修改了一小部分代碼使程式變得好看一點。又由于在第二次電梯作業中對其非常的上心，記得當時很多的邏輯結構，是以很容易就構造出了符合條件的測試集。雖然由于邏輯的複雜，在正确性論證的過程中碰了釘子，但總體來說還算比較順利。
從我個人的角度來看，這一路走來，我的工程化能力有着比較大的提升和進步，對面向對象的學習也是非常認真。是以非常感謝OO課程組為我們精心設計的關卡，非常感謝助教在這一過程中對我們的幫助。就我個人來說，相信如果沒有OO的闖關機制來輔助我的學習，單純通過上OO理論課，然後随便布置一些作業的話，我很難對OO這門課的認識有如今的程度。