1.JML语言的理论基础
JML是一种行为接口规范语言，可以更准确地描述Java程序的行为。 但是，大多数代码编写和测试仍由人来完成，但是用户体验不是很好，因为在使用过程中工具链的功能非常不完整。数据规范对类中的数据施加了一定数量的约束。 两者都是可见条件下的约束，因此，调用方法的开始和结束状态会突出显示，并且可以在方法执行期间更改一段时间。 不变和约束之间的区别在于不变值限制了数据的状态，而约束则限制了数据更改时的状态。
JML语言相关工具
- Sireum/Kiasan for Java：一个基于契约的自动化验证测试工具
- The AspectJML tool：为Java和AspectJ做运行时检查的工具
- The jml4c tool：基于Eclipse Java编译器开发的JML语言编译器
- JMLEclipse：在Eclipse的JDT编译器基础上开发的JML工具包
作业架构设计
这次的基本架构由JML通过接口提供。 您必须自己编写该课程。 您需要做的就是选择适当的容器并实现该方法。 焦点是图形的算法。 第二和第三项任务也需要考虑性能。
Runnr的首要任务是根据网络上的输入指令和Person的方法来调用NetWork的相关方法。 第一项任务没有性能要求，因此我选择了更常用的ArrayList容器。
- 第一次
- 第二次
- 第三次
心得体会
根据JML的实现，首先确定将导致不同操作的先决条件，使用这些先决条件来分离不同的操作，然后以不同的操作实现它们。
尽管这次算法的复杂度不是很低，但是算法的准确性很高，但是在现有理论非常丰富的情况下，不必盲目地发明轮子。 共享解决方案可重复使用久经考验的车轮。
如果您想研究未来大型项目开发的规范，团队编程将为您提供极大的帮助。