标签：内容 接口 返回值 str rem 架构 总结 equal tno
JML语言理论基础
Java建模语言（Java Modeling Language，JML）是一种进行详细设计的符号语言，他鼓励你用一种全新的方式来看待Java的类和方法。JML是一种行为接口规格语言 （Behavior Interface Speci?cation Language，BISL），基于Larch方法构建。BISL提供了对方法和类型的规格定义手段。所谓接口即一个方法或类型外部可见的内容。通过在Java代码中增加了一些符号，这些符号用来标识一个方法是干什么的，却并不关心它的实现。使用JML，我们就能够描述一个方法的预期的功能而不管他如何实现。通过这种方式，JML把过程性的思考延迟到方法设计中，从而扩展了面向对象设计的这个原则。
JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。JML引入了大量用于描述行为的结构，比如有模型域、量词、断言可视范围、预处理、后处理、条件继承以及正常行为（与异常行为相对）规范等等。对代码进行抽象：
方法规格抽象
数据(类型)规格抽象
通过一系列的JML表达式实现描述：
原子表达式
量化表达式
JML相应的工具链，可以自动识别和分析处理JML 规格。常用的有openjml，其使用SMT Solver来对检查程序实现是否满足所设计的规格(specification)。目前openjml封装了四个主流的solver：z3, cvc4, simplify, yices2。z3由Microsoft开发的，并已在github上开源：https://github.com/Z3Prover/z3 其正式发布版可通过https://www.microsoft.com/en-us/download/details.aspx?id=52270获得。cvc4由Standford开发，可以通过http://cvc4.cs.stanford.edu/downloads/下载。
下载openjml在IDEA中配置外部工具链进行静态验证。
JUnit是一个强大的单元测试工具。配置过程如下：
1、下载JUnit4.13的jar包
2、把这两个jar包加入环境变量的classpath中
3、安装IDEA的Junit generator V2.0插件
4、设置项目jar包依赖
5、生成一个Test类模板
6、运行测试
部分测试如下：
import com.oocourse.specs2.models.Path; import org.junit.After; import org.junit.Assert; import org.junit.Before; import org.junit.Test; /** * MyGraph Tester. * * @author <Authors name> * @version 1.0 * @since <pre>五月 20, 2019</pre> */ public class MyGraphTest { private MyGraph myGraph = new MyGraph(); private Path path1, path2, path3, path4; @Before public void before() throws Exception { path1 = new MyPath(1, 2, 3, 4); path2 = new MyPath(1, 2, 3, 4); path3 = new MyPath(1, 2, 3, 4, 5); path4 = new MyPath(2, 5, 6, 8, 9); myGraph.addPath(path1); myGraph.addPath(path2); myGraph.addPath(path3); } @After public void after() throws Exception { } /** * Method: size() */ @Test public void testSize() throws Exception { //TODO: Test goes here... Assert.assertEquals(myGraph.size(), 2); } /** * Method: containsPath(Path path) */ @Test public void testContainsPath() throws Exception { //TODO: Test goes here... Assert.assertTrue(myGraph.containsPath(path2)); } /** * Method: containsPathId(int pathId) */ @Test public void testContainsPathId() throws Exception { //TODO: Test goes here... Assert.assertTrue(myGraph.containsPathId(2)); } /** * Method: getPathById(int pathId) */ @Test public void testGetPathById() throws Exception { //TODO: Test goes here... Assert.assertEquals(myGraph.getPathById(2), path3); } /** * Method: getPathId(Path path) */ @Test public void testGetPathId() throws Exception { //TODO: Test goes here... Assert.assertEquals(myGraph.getPathId(path2), 1); } /** * Method: addPath(Path path) */ @Test public void testAddPath() throws Exception { //TODO: Test goes here... Assert.assertEquals(myGraph.addPath(path3), 2); } /** * Method: removePath(Path path) */ @Test public void testRemovePath() throws Exception { //TODO: Test goes here... Assert.assertEquals(myGraph.removePath(path2), 1); } /** * Method: removePathById(int pathId) */ @Test public void testRemovePathById() throws Exception { //TODO: Test goes here... myGraph.removePathById(1); Assert.assertTrue(!myGraph.containsPath(path2)); } /** * Method: getDistinctNodeCount() */ @Test public void testGetDistinctNodeCount() throws Exception { //TODO: Test goes here... } }
经验证，功能得到实现且未发现错误。
第二次Graph继承第一次PathContainer实现。采用数据结构如下：
/* node counter; pid -- path Map; distinctNodesSet; graph邻接表; */ private int cnt = 1;//路径id计数器 private Map<Integer, Path> pathMap;//路径id-路径对应表 private Set<Integer> nodeSet;//不重复的节点集合 private Map<Integer, HashSet<Integer>> adj;//图的邻接表 /* used for graph calculate */ private Map<Integer, Integer> marked;//bfs记录访问状态 private Map<Integer, Integer> distTo;//bfs记录距离
无权无向图，简单bfs即可寻找最短路径。第三次规格作业尝试采用Floyd寻找几种自定义最短路。
第一次规格作业，偏序比较接口未考虑int溢出，没有直接使用Integer.compareTo，加上TLE共计8处bug，第二次作业1次TLE的bug。
此单元主要学习规格的理解和使用，初步了解需求分析到代码的中间过程---即规格的标准和工具，逐渐理解JML等规格语言对于代码交接、维护的重要意义。JML像是一种契约，在你完成你的工作后来调用我，我就保证返回给你正确的结果，这种契约保证了软件、工程开发的各司其职、高效执行。
标签：内容 接口 返回值 str rem 架构 总结 equal tno
原文地址：https://www.cnblogs.com/nebulau/p/10896248.html
