測試與正确性論證的效果差異及優缺點
測試實際上就是對程式進行的一種黑箱測試，利用各種各樣的測試樣例去檢驗程式是否能夠給出正确的結果。其中的單元測試則是将整體的測試拆分成單元來進行，但其仍然躲不開黑箱測試的形式。而正确性論證雖然也是從各個方法入手，但其并不是盲目的對比輸入輸出是否一樣，而是從邏輯上梳理某個方法運作過程中僅可能出現的輸入（即前置條件）和針對這些輸入僅可能給出的結果（後置條件），進而在確定各個方法實作均正确的情況下将其組合起來成為一個正确的系統。
從效果上來講測試由于并不能窮舉所有的情況，而正确性論證我認為實際上是對各種情況的抽象和歸類，進而将無窮變為有窮，其效果也明顯優于測試。但正确性論證如果要梳理清楚各種邏輯的關系，其複雜程度要高于測試很多， 是以做起來也相對複雜，測試隻需要設計各種測試樣例并且自動運作檢視結果即可，相比而言較為簡單。
OCL調研及與JSF的異同
OCL (Object Constraint Language) 即對象限制語言，是一種訓示使用者模組化系統中的限制方式，它是UML可選的附加内容，可以用來更好的定義對象的行為，并為任何類元指定限制。
OCL是一種精确無二義性的語言，并且是一種規範說明性語言，能夠用來限制UML圖中的對象。
與JSF的異同：
相同：
均使用了數學的方法（謂詞邏輯、集合論）來表達對對象和方法的限制，都采用了自然語言和數學符号折衷的方式
均是一種聲明式的語言，即内容中不包含具體實作
都包含前置條件和後置條件的聲明，也都包含不變式相關邏輯
不同：
OCL中沒有JSF的MODIFIES，但多出了“監護規則”。除此之外OCL非常注重類型的聲明，并且細化了各種容器，相比之下JSF均抽象為數組來表達了。
第十四次作業類圖、順序圖、狀态圖
學期總結
四個單元子產品知識點之間的關系
第一單元我認為主要是初步認識面向對象思想，掌握類屬性方法等元素以及繼承、多态等OO的基本思想，順便學會如何使用Java編寫OO程式。第二單元主要面向OO當中的多線程程式設計，在前一個單元的基礎上利用面向對象的方式編寫多線程程式。第三單元主要是JSF的引入，以及設計方面的更進階要求（如SOLID、規格）。第四單元則是對于測試和正确性論證的學習，即一個程式寫到最後要確定寫的是對的。
這四個單元我認為前兩個單元主要更側重程式設計技術方面，實際上學習多線程程式設計除了掌握并行的思想外，更重要的其實是怎麼在多線程如此混亂的情況下讓程式跑出自己想要的結果（想起了OS中的互斥和同步的關系），因而技巧方面更重一些。而後兩個單元則更側重設計以及程式設計之後驗證的部分，前者讓我們養成良好的設計思想，我認為規格化的開發思想在程式規模增大的時候才能展現其優勢；而後者讓我們確定了自己程式寫的是對的，能夠經過各種各樣的檢驗。
自己的進步
一個學期以來寫了多項式、電梯三部曲、IFTTT、計程車四部曲這麼多程式，可以說進步應該還是有的。
從設計和代碼品質上，一開始代碼耦合高，第一次ALS電梯一個方法有200行，到後來程式逐漸變得層次清晰，最後第13次和14次作業對電梯進行了解耦，将原先200行的方法拆分成很多個，每個的行數都較短。原先因為DRY做的不好，重複代碼較大導緻經常出現改一處忘了改另一處的情況之後也變得很少了。
雖然第一單元的程式幾乎沒什麼bug，但設計思路方面的不清晰導緻多線程部分有所翻車，但在對程式的構思逐漸形成合理的模式後，這種情況在計程車有了很大改善。
對工程化開發的了解
我是從大二才開始聽說“工程化思想”這一詞的，印象最深刻的實際上也是上學期的計組，老師不斷的強調“工程話思想”。實際上工程化思想我認為隻有當程式需要達到一定規模時才能看出其優勢，無論是這學期OO到最後代碼量很大的計程車還是上學期完成的計組實驗都可以說明這一點，而這兩者相比于真正的工程而言更是小巫見大巫。
雖然到現在為止我還沒有接觸過真正的工程化開發，對于作業也僅僅是利用了一點“思想”而已，是以我的了解還隻能停留在空想的階段。我了解的工程化開發，首先是一種子產品化的設計，整個程式是由多個子產品構成的，這些子產品滿足所謂的“高内聚、低耦合”關系，單獨來看雖然不能做什麼但組合到一起才能完成很複雜的工作。其次作為一個“工程”，必定是一個相對長久的概念，是以需要很多個人“前仆後繼”的進行努力。是以在工程化開發中我認為規格很重要。如何讓大家程式設計的點子統一起來，同時讓大家編寫的一個個”子產品“最後能順利的組合在一起是一個需要重視的問題。規格設計以及接口這一概念在其中充當了非常重要的角色。
對課程的期望和建議
1. 在寫作業的時候很多問題我都是從同學的口中得知在”他們班的群裡“助教說了什麼什麼要求，很多時候這些要求沒有被通知到，也出現了最後申訴中兩人互飙微信群截圖的情況。希望可以有一種統一的要求通知機制（比如對于各種問題能及時梳理到issue），能夠統一口徑并且減輕助教答疑和同學們追問的壓力。
2. JSF方面首先我感覺可以借鑒一下OCL語言，例如其中的各種容器。其次課件中經常使用多項式以及數組等等來舉例子，在這些方面的确JSF可以清晰的表達規格，但對于計程車等複雜邏輯而言沒有很好的參考價值。希望課上能多一些較為複雜的例子。
3. 多線程其實在這個課程中的位置稍顯尴尬，的确很重要，但也導緻學習曲線較為陡峭。本學期中期OS課上我們也接觸了很多并發相關的概念，其中PV操作講的那些并發經典例子其實對多線程了解有不少幫助。第一次多線程電梯之前那節多線程的課對于多線程電梯來說有點“不夠”，導緻多線程電梯寫的雲裡霧裡。希望在多線程的起步教學這方面可以增加一些内容幫助了解。