标签：获取 算术操作符 导致 习惯 cal 跳过 表达 二次 use
? JML是用于对Java程序进行规格化设计的一种表示语言
JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。其中行注释的表示方式 为//@annotation，块注释的方式为/* @ annotation @*/。按照Javadoc习惯，JML注释一般放在被注释成分的 近邻上部
2.1 原子表达式：
\result表达式：表示一个非void类型的方法执行所获得的结果，即方法执行后的返回值
\old( expr )表达式：用来表示一个表达式expr在相应方法执行前的取值。
\not_assigned(x,y,...)表达式：用来表示括号中的变量是否在方法执行过程中被赋值。
\not_modified(x,y,...)表达式:该表达式限制括号中的变量在方法执行期间的取 值未发生变化。
\nonnullelements( container )表达式：表示container对象中存储的对象不会有null
\type(type)表达式：返回类型type对应的类型(Class)
\typeof(expr)表达式：该表达式返回expr对应的准确类型。
2.2 量化表达式
\forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
\exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
\sum表达式：返回给定范围内的表达式的和。
\product表达式：返回给定范围内的表达式的连乘结果。
\max表达式：返回给定范围内的表达式的最大值
2.3 集合表达式
集合构造表达式：可以在JML规格中构造一个局部的集合（容器），明确集合中可以包含的元素。
2.4 操作符
JML表达式中可以正常使用Java语言所定义的操作符，包括算术操作符、逻辑预算操作符等。此外，JML专门又定义 了如下四类操作符。
(1) 子类型关系操作符：E1<:E2
(2) 等价关系操作符：b_expr1<==>b_expr2或者b_expr1<=!=>b_expr2
(3) 推理操作符：b_expr1==>b_expr2或者b_expr2<==b_expr1。
(4) 变量引用操作符：\nothing指示一个空集；\everything指示一个全集
public class Sub {
2 /*@ public normal_behaviour
3 @ requires a > 0 && b > 0;
4 @ ensures \result == a - b;
5 @*/
6 public static int sub(int a, int b) {
7 return a - b;
8 }
9
10 public static void main(String[] args) {
11 sub(1, 1);
12 }
13 }首先，对JML语言进行检查。
1 java -jar ../openjml/openjml.jar -check Sub.java > re.txt生成和编译
1 java -jar jmlunitng-1_4.jar Sub.java
2 javac -cp jmlunitng-1_4.jar *.java
3 java -jar ../openjml/openjml.jar -rac Sub.java
4 java -cp jmlunitng-1_4.jar Sub_JML_Test运行结果如图：
.png)
第一次作业要求为实现容器类Path和PathContainer，Path为节点序列，PathContainer需要实现pathid和path的检索以及容器内不同节点个数的查询。
具体实现为：Path类通过Arraylist存储路径，Hashset存储点集；PathContainer通过两个Hashmap解决路径检索，维护一个Hashmap记录不同节点的个数。
在第一次作业的基础上要求实现Graph类，需要实现对任意节点间最短距离的查询。
我实现了GraphQuery类来完成对所有图相关查询指令的处理。最短距离的计算，我选择使用floyd法，由于节点的id为int类型，需要首先将其映射到从0开始的连续整数。在GraphQuery中维护一个Hashmap记录该映射关系。每次增加路径时，Graph类调用GraphQuery的add方法，为新增的所有新节点分配映射关系，初始化floyd矩阵并计算。每次删除路径时，重新初始化floyd矩阵并计算。
在第二次作业的基础上要求实现RailwaySystem类，实现对任意节点间最少换乘、最少票价和最少不满意度和图的联通块数目的查询。
图的联通块数目我采用bfs染色进行计算。
对于三种最短路的计算，我采用讨论区著名的wjy算法，将每一条路径先构造成完全图，对于最少换乘，将一条路径上所有点间的权值设为1；对于最少票价，则将权值设为两点间的距离+换乘费用也就是2；对于最少不满意度，将权值设为两点间的不满意度+换乘不满意度即32；如此对任意查询，求其对应图的两点间最短路径即可。
具体架构：由于每条路径都需要重新建图，且该图是稀疏图，因此我采用spfa法计算对不同查询要求计算两点间的新权值。首先封装了SpfaCalculator用于对一张图的最短距离计算，每增加一条路径，实例化一个Updater，记录该路径对应的邻接矩阵并调用SpfaCalculator计算，返回新图。在RailwayQuery中维护三个矩阵分别对应三种需求，对每一条路径，调用updater获取小图并更新大图，之后进行floyd运算。
第一二次作业均没有bug出现，第三次作业对相同节点的contains edge出了问题，通过floyd矩阵中对应位置元素的大小是否为1来判断，但在初始化该矩阵时跳过了对角元的初始化，导致总是返回无穷大。
JML语言更加精准的描述了一个类或者方法的行为，先写JML再实现对应类或方法，可以明确方法的边界行为，并对降低程序的耦合度很有帮助。而本次作业的迭代开发的过程，也让我对继承的具体实现有了更多的认识。
标签：获取 算术操作符 导致 习惯 cal 跳过 表达 二次 use
原文地址：https://www.cnblogs.com/okawaikoto/p/10907677.html
