unit3_logPre 第三单元的主题是规格化设计，需要我们学会理解与使用JML语言对于java程序进行建模，从而实现对于需求的形式化。 形式化有许多好处： 逻辑明确，没有二义性，具有可靠性。 能够形式化的东西一定能够自动化，所以有利于自