规格

规格

关注
发信
关注(28)粉丝(399)

面向对象设计与构造：JML规格单元作业总结

面向对象设计与构造：JML规格单元作业总结

第一部分：JML语言理论基础

JML语言是什么：对Java程序进行规格化设计的一种表示语言

使用JML语言有什么好处：

  • 用逻辑严格的规格取代自然语言，照顾马龙的语文水平。一切挑战规则的行为必将受到严厉惩罚
  • 代码维护性高，让大牛的代码不再晦涩，让轮子制造机无机可乘

JML(Level 0)语法

  • 单行注释
  • 块注释
  • 原子表达式
  • 量化表达式
  • 操作符
  • 方法规格

  • 类型规格

    • 不变式invariant：是要求在所有可见状态(凡是会修改成员变量，包括静态成员变量和非静态成员变量的方法执行期间)下都必须满足的特性。可以在不变式定义中明确使用 instance invariant 或 static invariant 表示不变式的类别
    • 状态变化约束constraint：对象的状态在变化时往往也许满足一些约束，cons对前序可见状态和当前可见状态的

      关系进行约束

JML手册：

https://oo-public-1258540306.cos.ap-beijing.myqcloud.com/experiments/experiment_5/JML Level 0手册.pdf

第二部分：应用工具链

openJML

Github发行版：

https://github.com/OpenJML/OpenJML/releases

OpenJML(IDEA)硬核玩家：

https://course.buaaoo.top/assignment/66/discussion/193

OpenJML基本使用：

https://course.buaaoo.top/assignment/66/discussion/198

给以上两位奆佬递茶～

功能

写在前面：OpenJML不支持\forall int[] 和 \exists int[]等语法。

  • JML规格静态检查：判断JML规格的正确性(无关代码)

    public class JMLTest {
    
    /*@
    
      @ public normal_behaviour
    
      @ requires lhs<0 &&
    
    */
    
    public static int compare(int lhs, int rhs) {
    
        return lhs - rhs;
    
    }

    public static void main(String[] args) {
    
        compare(114514, 1919810);
    
    }
    
}

面向对象设计与构造：JML规格单元作业总结-LMLPHP

可以看到规格的第三行Invalid

  • 代码静态检查

    windows命令行下似乎不太友好~

面向对象设计与构造：JML规格单元作业总结-LMLPHP

  • 动态检查

public class JMLTest {

    /*@

      @ public normal_behaviour

      @ requires lhs > 0 && rhs > 0;

    */

    public static int compare(int lhs, int rhs) {

        return lhs - rhs;

    }

    public static void main(String[] args) {

        compare(-45, -5);

    }

}

面向对象设计与构造：JML规格单元作业总结-LMLPHP

面向对象设计与构造：JML规格单元作业总结-LMLPHP

可看到对应报错的位置JMLTest.java:11

JMLUnitNG

伸手党入口：

https://course.buaaoo.top/assignment/71/discussion/199

功能

根据JML语言生成TestNG测试

SMT Solver

SMT solver简介：

https://zhuanlan.zhihu.com/p/30520308

SMT solver使用：

https://course.buaaoo.top/assignment/66/discussion/189

功能

openjml使用SMT Solver来对检查程序实现是否满足所设计的规格(specification)

部署SMT Solver

IDEA + Z3-4.7.1

面向对象设计与构造：JML规格单元作业总结-LMLPHP

检查报错内容：

面向对象设计与构造：JML规格单元作业总结-LMLPHP

可看到isValid方法中，代码与JML规格不符

第三部分：JMLUnitNG

测试代码

package JMLTest;

public class JMLTest {

    /*@ public normal_behaviour

      @ ensures \result == lhs - rhs;

    */

    public static int compare(int lhs, int rhs) {

        return lhs - rhs;

    }

    public static void main(String[] args) {

        compare(114514,1919810);

    }

}

生成的测试样例

[TestNG] Running:

  Command line suite

Passed: racEnabled()

Passed: constructor Demo()

Passed: static compare(-2147483648, -2147483648)

Failed: static compare(0, -2147483648)

Failed: static compare(2147483647, -2147483648)

Passed: static compare(-2147483648, 0)

Passed: static compare(0, 0)

Passed: static compare(2147483647, 0)

Failed: static compare(-2147483648, 2147483647)

Passed: static compare(0, 2147483647)

Passed: static compare(2147483647, 2147483647)

Passed: static main(null)

Passed: static main({})

===============================================

Command line suite

Total tests run: 13, Failures: 3, Skips: 0

===============================================

jmlunitng仅仅使用了整数最大值，最小值以及0进行检查，测试覆盖性较差。

第四部分：架构设计

第一次作业

丝路

MyPathContainer

  • plist（pidlist）：路径与路径ID之间的映射关系。利于contains，get相关查询操作
  • nodeMap：记录结点编号与结点出现次数的映射关系。利于全局distinctNodeCount查询操作
  • idCount：全局路径ID增长器
  • inputNodeMap，outputNodeMap：更新状态，被add，remove类方法调用，这样做的原因是抽象出状态更新器为后续功能扩展提供上层接口

MyPath

  • nodeSet ：结点编号集合。利于containsNode和路径内distinctNodeCount查询操作
  • 重写HashCode和equals：为PathContainer容器中的HashMap服务
UML

面向对象设计与构造：JML规格单元作业总结-LMLPHP

第二次作业

丝路

CalGraph：图计算类

  • 静态数组+BFS策略解决最短路
  • nodeList，nodeIdList：图内结点实际ID与分配编号映射关系
  • availNode，usedNode：记录图内编号分配情况
  • graph：邻接表
  • graphChanged：本次查询距上一次查询期间是否有增删图操作
  • edges：二维矩阵，edges[i][j]记录结点i和j之间所连接的边数
  • shortestPath：二维矩阵，最短距离矩阵，可判断两点的连通性

MyGraph，MyPath：基于上次扩展，无重构

UML

面向对象设计与构造：JML规格单元作业总结-LMLPHP

第三次作业

丝路

整体架构

面向对象设计与构造：JML规格单元作业总结-LMLPHP

非拆点构图做法(以最小花费为例)

面向对象设计与构造：JML规格单元作业总结-LMLPHP

步骤1：为每一条Path构建自身最小花费图

  • 0→1→2：直连边的权值为3(基础花费1+换乘花费2)，新添非直连边1→3边权为两结点的最短路+换乘花费2
  • 确保Path内任意两点间均有边相连

步骤2：以Path为单位构建整个最小花费图

步骤3：以最短路形式更新整个最小花费图，如图中的0号结点到3号结点新添权值为3+3的边

  • 确保整个图内任意两点间均有边

步骤4：最终的最小花费为边权 - 2，如0到5的最小花费为7-2 = 5

简单验证行为正确性

面向对象设计与构造：JML规格单元作业总结-LMLPHP

  • 当源节点A和换乘结点B在一条Path中，换乘结点B和目的结点C在一条Path中
  • 按上述方式在Path内构建最小花费图，设A到B边权t1, B到C边权t2
  • A到B的边权为t1 = A到B的最短路+2,在一条路径内无换乘因此A到B开销为t1-2,同理B到C为t2-2
  • A到C经历了一次换乘，开销应为A到B最短路+B到C最短路+2，即(t1-2)+(t2-2)+2,即t1+t2-2(A到C边权-2)
  • 当源结点A和换乘结点B不在同一条Path中，A到B的边权可以看作上述过程更新后的结果

因此

最短路径：普通构图即可

最少换乘：一个Path内任意两点边权为1+MAX(最大换乘次数)，构建整个换乘最短图后，最少换乘为(边权-MAX)/MAX

最少不满意度：Path内任意两点边权为最少不满意度+32(以最短路形式找两点间的最少不满意度)，构建整个换乘最短图后，最少不满意度为边权-32

算法：当然是Floyed啦~
UML

此处只说明一下矩阵类，也是我架构中的精华

面向对象设计与构造：JML规格单元作业总结-LMLPHP

  • 几种矩阵的初始化方式相同(ij=MAX_NUM，ii=0)，均需floyed来对图更新，均需修改图中的数据。上述行为被抽象为父类公有方法，结点ID与所分配编号的映射也是所有子类所公有的数据成员。子类的构图方式createMatrix有所不同，因此被抽象为子类特有方法

  • nodeNum:数据范围(120或者80)

  • usedNodeList：已分配编号的集合(不超过120)，主要是为floyed遍历时剪枝，无需考虑未加入图中的结点

  • nodeIdToNode: 结点ID到所分配编号的映射

  • matrix: 静态二维数组

  • singlePathToMatrix: 满意度矩阵和花费矩阵的特有方法，实际上是为一个Path内构建上述两矩阵提供接口，这一点从createMatrix和singlePathToMatrix的参数类型可以看出。至于为什么要在一个Path类构造上述两种矩阵，其实是为了覆盖更新，例如满意度矩阵的createMatrix方法如下:

    public void createMatrix(Map<MyPath, Integer> pathSet) {
    
        initMatrix();
    
        for (MyPath path : pathSet.keySet()) {
    
            for (int i = 0; i < path.size() - 1; i++) {
    
                for (int j = i + 1; j < path.size(); j++) {
    
                    int sraNode = getNode(path.getNode(i));
    
                    int dstNode = getNode(path.getNode(j));
    
                    if (sraNode != dstNode) {
    
                        int pvalue = path.getShortUnpleasantValue( //从这里可以看出Path内存在
    
                                path.getNode(i), path.getNode(j)) + 32; //一个单独的满意度矩阵
    
                        if (getMatrix()[sraNode][dstNode] > pvalue) {
    
                            modify(sraNode, dstNode, pvalue);
    
                            modify(dstNode, sraNode, pvalue);
    
...
关于重构
  • 在上述Path内新增两种矩阵，意味着MyPath需要新增方法与属性
  • 除此之外，需要在Graph类新增自定义方法和规格接口，再增加PathSet一类的管理数据
  • 新增Matrix类，为CalGraph类的计算提供合理的组织结构

第五部分：BUG

直接上第三次~

被Hack

错位定位

public class Matrix {

    //private static int nodeNum;

    private int nodeNum;

    ...

对你没有看错，注释掉的那一行为提交的版本，下面一行为修复版本。即删掉一个static让我修复了：

为什么呢？

public Matrix(int nodeNum, LinkedList usedNodeList, Map nodeIdToNode) {

        this.nodeNum = nodeNum;

    	...

}

​这是俺Matrix类的构造方法。static意味着，当第一次创建Matrix时传入的nodeNum参数会初始化该类的静态数据nodeNum，初始化后的静态数据生命周期终结于整个APP结束。然后我，我，，忘了我先创建Path时，在Path内构造了两个Matrix，传入的参数为80，即结点序列的最大长度。

​最魔鬼的是，我自己构造的测试单元把数据卡在了40以内。为什么呢？ 因为我认为小数据集验证程序的正确性后，大数据只需保证合理的数据范围即可。当然学习过程中会犯蠢，只希望以后不犯这么蠢的错误就好 ~

Hack别人

C组的生态真是恐怖，某哥们儿的战绩：119/119。我怀疑他在犯罪，但我没有证据

eg.1

局内Saber大哥一个类里写了790行代码

public int addPath(Path path) {

    ...

    if (change == 1) {

       getShortestLenth(); }

	...

}

​采用和我一样的设计思路，存在的问题是每次addPath就更新图，但是这种设计方法不能把Path独立起来看待。在对于图的更新时，要把所有Path一次性加入一张干净的图中。导致他的程序从架构层面就问题不断。

eg.2

​Rider的代码风格我很喜欢，出错的原因是样例中第一次CONNECTED_BLOCK_COUNT正确，但removePath后的第二次CONNECTED_BLOCK_COUNT出错。

private void reset() {

        mapping.reset();

        initMat(initMat);

        initMat(unpleasantMat);

        initMat(priceMat);

        for (Path path : paths) {

            addPath(path);

        }

}

​reset方法是在remove函数中调用的，乍一看没啥毛病。深入addPath后知道没处理好pathId与path对应的问题，以至于remove会出现在某些情况下remove掉错的path。

eg.3

​Caster还是把MyRailwaySystem写得过于臃肿(刚好卡在500行)，方法实现和接口没有隔离。

public int getLeastTransferCount(int fromNodeId, int toNodeId) throws

  	...

    Eyz con = new Eyz(fromNodeId,toNodeId);

    if (!tran.containsKey(con)) {

        minpath(con,tran,djsttran,trangraph,2);

    }

    return tran.get(con);

}

private void minpath(Eyz eyz, HashMap<Eyz,Integer> queue,

      HashMap<Integer,Minpath> mid,HashMap<Qyz,HashMap<Qyz,Qyz>> graph,int type) {

    if (mid.containsKey(eyz.get(0))) {

        mid.get(eyz.get(0)).count(eyz,queue,type);

    } else {

        Minpath mp = new Minpath(graph,eyz.get(0),type,jcnode);

        mid.put(eyz.get(0),mp);

        mid.get(eyz.get(0)).count(eyz,queue,type);

    }

}

​我猜想这里的minpath应该是更新图一类的操作，但说实话我着实看不懂他的命名，也没有代码注释(内心有点小崩溃

出错的原因应该还是没有维护好图。

嗯，还有很多（毕竟，我这次挺

05-22 23:47
Powered by LMLPHP ©2024 规格 0.055961