标签：OO 总结 Java 语言 实现 作业 规格 JML 单元
前言
经过了三个星期的第三单元的学习，现在又到了进行总结的时间了。接下来我将从ML语言的理论基础，SMT Solver，JMLUnit，以及自己作业的架构等方面来叙述这个单元的学习。
JML语言的理论基础和应用工具链
理论基础：
JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言（Behavior Interface Specification Language，BISL），基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。
一般而言，JML有两种主要的用法：
（1）开展规格化设计。这样交给代码实现人员的将不是可能带有内在模糊性的自然语言描述，而是逻辑严格的规格。
（2）针对已有的代码实现，书写其对应的规格，从而提高代码的可维护性。这在遗留代码的维护方面具有特别重要的意义。
维基百科的翻译如下：JML是Java模块的行为接口规范语言。 JML提供语义来正式描述Java模块的行为，防止模块设计者的意图模糊。 JML继承了Eiffel，Larch和Refinement Calculus的思想，其目标是提供严格的形式语义，同时仍然可供任何Java程序员访问。 有各种工具可以使用JML的行为规范。 由于规范可以作为Java程序文件中的注释编写，或者存储在单独的规范文件中，因此可以使用任何Java编译器编译具有JML规范的Java模块。
应用工具链情况：
可以使用开源的JML编译器来编译含有JML标记的代码，所生成的类文件会在运行时自动检查JML规范，若程序未实现规范中规定的事情，JML运行期断言检查编译器会抛出一个unchecked exception来说明程序违背了哪一条规范。JMLUnit可以生成一个Java类文件测试的框架。SMT Solver工具可以以静态方式来检查代码实现对规格的满足情况。
SMT Solver
不用写啦。
JMLUnitNG/JMLUnit
说实话，自己对于这个东西，确实不太会，当时即使看着讨论区里面大佬的帖子，然后照着做，仍然碰到了很多奇怪的问题。花了很久的时间，最后也只是勉强搞定了大佬给的自己创的测试用例。
一顿操作之后，终于成功搞出了结果。还真是只感受了一下，更深的也确实不会弄了。
个人作业总结
很遗憾，最后一次作业没有能够提交成功，所以就主要写一下前两次的作业的一些东西吧。
架构
这个单元的作业一步一步从抽象的层面向具体的层面一步步靠近。通过extend关键字，还有implement关键字，实现了关系的继承还有接口的实现。
通过上面的类图很容易看到作业的继承迭代情况。在第一次作业中，MyPath实现了Path接口，MyPathContainer实现了Container接口。在第二次作业中，我没有对MyPath和MyPathContainer类进行什么修改，基本保持了原来的状态，然后新建了一个MyGraph类实现了Graph接口，同时继承了MyPathContainer类，使得它可以使用寻找路径，ID等的操作。同时，因为要在myGraph类中构建一个图，所以在MyGraph中重写了添加和删除路径的操作，在添加删除的时候，对自己构建的图也进行相应的修改。
总体架构上面Path的改变不大，主要的迭代都是发生在Container上面，将一个抽象的容器变成一个具体的地铁站。
同时在设计中我是用的容器都是Java自带的容器，包括ArrayList和HashMap。
代码bug
因为最后只完成了前两次作业没所以并没有遇到逻辑上面的bug。但是强测试中因为时间和复杂度的问题被扣了不少的分。究其原因，还是在实现MypathContainer类的时候，使用了大量的for循环语句进行遍历查找，导致数据量大的时候会严重的超时。当时在完成作业的时候，说实话自己并没有考虑很多关于时间的问题。看到JML语言的描述之后，就直接顺着它的思路和描述，用for循环写了下来，然后也不需要怎么调试就可以轻松通过初测。
在对bug的修复中就是减少对for循环语句的使用，更多地使用新学的HashMap来完成对数据的存储和查找工作。HashMap速度确实比正常的查找快得多，理论最快可以达到O(1)，即使是最坏的情况也可以达到O(logn)。
心得体会
JML规格是为了在一些大型的项目，尤其是那些要求非常严格，希望绝对没有bug的重要项目。
在总体上，有一个总的规划，先确保总的逻辑正确性，再分别实现小的部分。每个对象（或者方法），都假设别人完成了别人的工作，然后自己也确保自己完成自己应有的工作，那么整个系统就能协调地运行了。JML中有require，来限定方法的传入的部分是什么样的，也有ensure来约束最后通过这个方法，想要取得怎样的效果。在JML语言中，我们并不关心中间是如何实现的，具体的实现部分取决于程序员自己，他只关心传入的和传出的部分都是什么，好像把一个个方法用标准化的语言给掩藏起来了，我觉得这也是面向对象思想的一部分吧。
在规格中，可能会用到一些数据结构，但是实际的实现过程中可能用不上这些。比如说JML中写着要for遍历寻找，但我们实际上可以用HashMap的getKey方法来实现，只要最后得出的结果是正确的，就是符合规格的。这也让它看上去更加灵活多变。
总结
第三单元的学习就随着这篇博客结束了。第三单元结束后，可能也没有多少代码作业了。总体上说，这三周的学习还是让我收获了不少的。自己接触到了一种全新的用来描述规格的语言——JML语言。并且用它来完成了几次作业。在课上的试验中，自己也亲自完成了几个根据代码或者描述，写出对应的JML语言规格的练习。说实在的，自己完成的情况其实并不太好，希望自己能在最后一个单元的学习中再接再厉吧。
标签：OO,总结,Java,语言,实现,作业,规格,JML,单元 来源： https://www.cnblogs.com/17373366-masterpan/p/10889790.html
本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享； 2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关； 3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关； 4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除； 5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。