JML語言的理論基礎和應用工具鏈情況

　　The java modeling language，是用于對java程序進行規格化設計的語言。在語法上，JML表達式包括原子表達式，量化表達式，集合表達式和操作符。方法規格方面，有前置條件requires，后置條件ensures，和副作用assignable or modifiable。

　　openjml是主要的應用工具鏈，包括語法檢查，靜態檢查，運行時檢查三個功能。

　　parsing and type-checking：

　　openjml -check <source files>

　　static checking：

　　openjml -esc <source files>

　　runtime-assertion checking：

　　openjml -rac <source fils>

JMLUnitNG/JMLUnit

　　jmluniting生成測試文件并編譯后可以進行測試，測試能很好地覆蓋一些邊界。

對本單元的體會

　　在本單元閱讀規格、根據規格編寫程序、撰寫規格的訓練下，我更明確地認識到了程序的質量是設計出來的，而不是編程調試出來的，這樣一種規格設計的思想也使我在寫程序時會首先考慮各個單元的返回結果，并設計測試，而不是考慮具體實現方式立刻上手去做。另外，在實際通過JML體會了這種開發模式后，我認為盡管JML描述嚴謹，但快速準確理解仍有難度，尤其在描述的功能比較復雜的時候，或許非大規模團隊開發依然是自然語言描述規格更加方便高效。

轉載于:https://www.cnblogs.com/buaa17373128/p/10908802.html

總結

以上是生活随笔為你收集整理的面向对象博客作业3的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。