OO_BLOG3_规格化设计(JML学习)

目录

  • JML语言学习笔记
    • 理论基础
    • 应用工具链情况
    • JMLUnit/JMLUnitNG
  • UNIT3 作业分析
    • 作业 3-1 实现两个容器类Path和PathContainer
    • 作业 3-2 实现容器类Path和数据结构类Graph
    • 作业 3-3 实现容器类Path,地铁系统类RailwaySystem
  • 规格撰写的心得与体会
  • 最后,衷心感谢为这门课程辛苦付出的老师和助教。???

JML语言学习笔记

理论基础

1. 注释结构

2. JML表达式

  • 原子表达式,量化表达式,集合表达式,操作符,etc.

3. 方法规格

  • 前置条件(pre-condition)
  • 后置条件(post-condition)
  • 副作用范围限定(side-effects)

4. 类型规格

  • 不变式(invariant)
  • 状态变化约束(constraint)

应用工具链情况

1. OpenJML & SMT Solver

  • 首先由OpenJML将JML规格转换乘SMT-LIB格式的代码,然后调用SMT solver进行检查。用于静态检查

2. JMLUnitNG

  • 根据规格自动生成测试文件。用于自动测试

3. JMLdoc

  • 可以快速生成JML文档的相关文件

4. Junit

  • Junit主要用于单元化测试与一定的自动化测试,配合JML食用效果极佳。

JMLUnit/JMLUnitNG

1. 前期准备

  • 简单代码示例与jar包配置
1615869-20190522120128637-1519398093.png1615869-20190522120152160-30847359.png

2. 命令行操作

java -jar jmlunitng.jar src/Demo.java 
javac -cp jmlunitng.jar src/*.java

3. 测试结果

1615869-20190522120135812-2074808793.png1615869-20190522120144850-322293277.png

4. 结果分析

  • 我们可以看出,自动生成的测试样例对各种极端情况进行了测试,具有较好的覆盖性。
  • 但是,在试验过程中,JML测试的局限性也被暴露出来了。

UNIT3 作业分析

作业 3-1 实现两个容器类Path和PathContainer

1. 架构设计

1)度量分析
1615869-20190522120201178-1202747953.png
2)结构分析
1615869-20190522120739470-1906886274.png
3)算法分析
  • MyPath

    • // path的存储结构,用来顺序存储结点
      private ArrayList<Integer> arrayNodes; 
      // 用来存储一条path中的node的个数(无重复)。key:结点名称;value:该结点出现的次数
      private HashMap<Integer, Integer> hashNodes; 
    • ADD:
      1)读入一个结点数组
      2)将结点顺序存入arrayNodes
      3)遍历结点数组,对于任一结点node,若node不在hashNodes中,即存入(node, 1);若已存在,即存入(node, value + 1)。
  • MyPathContainer

    • private int id = 0; // pathID
      private HashMap<Path, Integer> hashPaths; // Path --> PathID
      private HashMap<Integer, Path> hashIds; // PathID --> Path
      private HashMap<Integer, Integer> nodes; // Node --> frequentNumber
    • ADD:
      原理与path相同REMOVE:
      1)hashIds.remove(pathID),hashPaths.remove(path)
      2)对于path中的每一个node,(设node的出现次数为frequentNumber),若frequentNumber=1,则将node从nodes中移除;若frequentNumber>1,则 nodes.replace(node, frequentNumber-1)。

2. BUG分析

1)bug情况
  • 由于测试数据量的限制,程序在评测与互测环节没有出现错误。
2)修复情况
  • 该程序存在一些不优美的地方,如MyPath中,利用HashMap来存储不同结点是复杂的,可以说是自己造了个轮子,改正方法为使用HashSet进行存储,通过容器的特性来减少手动判断。

作业 3-2 实现容器类Path和数据结构类Graph

1. 架构设计

1)度量分析
1615869-20190522120214819-888796446.png1615869-20190522120220143-2140036106.png
2)结构分析
1615869-20190522120748711-1822232574.png
3)算法分析
  • AlGraph

    • // alGraph: node1 --> (node2 -> node2_frequentNumber)
      private HashMap<Integer, HashMap<Integer, Integer>> alGraph; 
      // edges: node1 --> (node2 -> shortestPathLength_From_Node1_To_Node2)
      private HashMap<Integer, HashMap<Integer, Integer>> edges; 
    • // 由原始图(alGraph)生成距离图(edges)的算法 ———— Floyd算法
      for (k = 0; k< MAX; k++) for (i = 0; i < MAX; i++) for (j = 0; j < MAX; j++) if (Graph[i][j] > Graph[i][k] + Graph[k][j]) Graph[i][j] = Graph[i][k] + Graph[k][j];
      
    • public boolean containsEdge(int node1, int node2) {return alGraph.get(node1).containsKey(node2);
      }
      public boolean isConnected(int node1, int node2) {if (node1 == node2) return true;else                return edges.get(node1).containsKey(node2);
      }
      public int getShortestPathLength(int node1, int node2) {if (node1 == node2) return 0;else                return edges.get(node1).get(node2);
      }
4)迭代中对架构的重构
  • AlGraph继承了上一次作业中的PathContainer,并进行了适当的扩充(具体扩充见如上算法分析)。

2. BUG分析

1)bug情况
  • 测试数据量增大时,程序出现 CPU_TIME_LIMIT_EXCEED 的错误。
  • 原因(据我分析):在Floyd算法中加入的大量的判断,当数据量增大时,造成CPU的负担过大,运算超时。
2)修复情况
  • 重构后UML图
1615869-20190522120754021-238182921.png
  • 算法分析

    • private final int biggest = 999999999; // 极大数(自由定义,小于2^31即可)
      private int id = 0; // PathID(同上一次作业)
      private HashMap<Path, Integer> pathToId; // Path --> PathID(同上一次作业)
      private HashMap<Integer, Path> idToPath; // PathID --> Path(同上一次作业)
      private HashMap<Integer, Integer> nodeToSum; // Node --> Node_Sum(同上一次作业)
      private HashMap<Integer, Integer> nodeToIndex; // Node --> Node_index_in_matrix
      private HashSet<Integer>[] adjVexSets; // 临界表:Node--Set{node1, node2, ...}
      private int[][] disMatrix; // Graph生成的存储各点之间距离的距离矩阵
      private Stack<Integer> indexStack; // 用来维护node<->index的映射的栈
    • '映射关系建立机制,搭建点与数组下标的关系
      if      put_New_Node_Into_Graph then bond_NewNode_to_IndexStack.pop() 
      else if remove_Node_From_Graph  then indexStack.push(oldNode.index)
3)前后对比
  • // 原程序,floyd部分代码
    for (int k : tempEdges.keySet()) for (int i : tempEdges.keySet()) for (int j : tempEdges.keySet()) if (tempEdges.get(i).containsKey(k) && tempEdges.get(k).containsKey(j)) { int via = tempEdges.get(i).get(k) + tempEdges.get(k).get(j);if (tempEdges.get(i).containsKey(j)) {if (tempEdges.get(i).get(j) > via) {tempEdges.get(i).replace(j, via);}} else {tempEdges.get(i).put(j, via);}}
  • // 重构后,floyd部分代码
    for (int k = 0; k < 255; k++) for (int i = 0; i < 255; i++) for (int j = 0; j < 255; j++) if (disMatrix[i][j] > (newDis = disMatrix[i][k] + disMatrix[k][j])) disMatrix[i][j] = newDis;

作业 3-3 实现容器类Path,地铁系统类RailwaySystem

1. 架构设计

1)度量分析
1615869-20190522120225784-579982037.png1615869-20190522120230939-364199165.png
2)结构分析
1615869-20190522120800108-1985593861.png
3)算法分析
  • MyRailwaySystem

    • private int cbCount = 0; // 连通块个数
      private int[][] disMatrix; // 距离矩阵 
      private int[][] transferMatrix; // 最小换乘矩阵
      private int[][] priceMatrix; // 价格矩阵
      private int[][] happyMatrix; // 最低不满意度矩阵
    • // 下面是算法的伪代码,以价格矩阵的更新为例,其它类似
      private void updatePriceMatrix() {priceMatrix = initMatrix(2);for (Each path : paths) {maxSize = path.size();priceArray = ((MyPath)path).getPriceArray();nodeMap = ((MyPath)path).getNodeMap();for (Each node1, node2 : nodeMap)if (priceArray[tempId1][tempId2] + 2 < priceMatrix[index1][index2]) priceMatrix[index1][index2] = priceMatrix[index2][index1] = priceArray[tempId2][tempId1] + 2;}floyd(priceMatrix, 125);
      }
4)迭代中对架构的重构
  • MyPath

    • MyPath添加了两个距离矩阵,用来存储一个Path(地铁线路)内部的(加权)距离信息。
    • 首先,将Path构建成两个加权无向图(权值分别为价格和满意度);然后,通过Floyd算法生成各自的距离矩阵,存储下来。

    • private int[][] priceArray; // 加权(价钱)距离矩阵
      private int[][] happyArray; // 加权(满意度)距离矩阵
      // 以下是算法的伪代码
      private void updateMatrix() {setNodeMap(); // 重新建立映射关系priceArray = initMatrix(nodeCount, 2); // 距离矩阵初始化happyArray = initMatrix(nodeCount, 32); // 距离矩阵初始化for (Each node1, node2 :nodes) { // 建图赋权priceArray[node1.index][node2.index] = priceArray[node2.index][node1.index] = 1;happyArray[node1.index][node2.index] = happyArray[node2.index][node1.index] = = CalculatePleasure();}floyd(priceArray); floyd(happyArray); // 计算各点之间距离
      }

2. BUG分析

1)bug情况
  • 这种算法在测试数据(最多结点数以及最多图变动指令数)有所约束时,展现出非常出色的性能。在强测与互测中均未出现错误。
  • 但是,我的代码结构有着较为严重的问题:几乎完全面向过程的写法严重违反了OOP的原则;多个相似结构重复计算等。
2)修复情况
  • 尚未进行代码重构,仅对课程组给出的标程进行了研究,并进行了简单的算法优化尝试。

规格撰写的心得与体会

  • 规格化设计和契约式编程,让人如沐清风,受益匪浅。 其实这次的代码工程量很大,但是由于课程组给出的JML的引导以及课程组已经将我们需要填写的代码抽象成了接口,这使得我们在写代码时会产生一种错觉——“这是面向对象课程吗?”、“这是数据结构补习课吧!”…… 这正是规格化设计和契约式编程 的巨大作用。
  • JML语言——好用不好写。 JML语言书写的困难度过高(从课程组编写JML出现的各种状况可以看出),给我的感觉是“可远观而不可亵玩”。而且,由于DDL过多加上学习资料不足(网上、课程资料都几乎为零),我缺乏自己动手写JML的动力。
  • 没有指引,路程变成了痛苦的过程。也许,是因为JML这一课还在探索阶段,课程对JML编写、检测、使用的工具的讲解和介绍颇少,基本全靠讨论区和大佬们的指点,自己摸索着完成任务。固然,可以说这是对我们自主学习能力的养成,但是,有必要吗?我相信JML单元会一步步从碎片化走向体系化,更加容易上手。
  • 在路上 ……

最后,衷心感谢为这门课程辛苦付出的老师和助教。???

转载于:https://www.cnblogs.com/FUJI-Mount/p/10905195.html

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:http://www.mzph.cn/news/386757.shtml

如若内容造成侵权/违法违规/事实不符,请联系多彩编程网进行投诉反馈email:809451989@qq.com,一经查实,立即删除!

相关文章

JAVA获取JVM内存空间和物理内存空间

一、获取JVM内存空间 系统环境&#xff1a;WIN JDK版本&#xff1a;1.8re 直接调用Runtime中相应的方法即可&#xff1a; public long maxMemory() Returns the maximum amount of memory that the Java virtual machine will attempt to use. If there is no inherent lim…

CMU Database Systems - Sorting,Aggregation,Join

Sorting 排序如果可在内存里面排&#xff0c;用经典的排序算法就ok&#xff0c;比如快排 问题在于&#xff0c;数据表中的的数据是很多的&#xff0c;没法一下都放到内存里面进行排序 所以就需要用到&#xff0c;外排&#xff0c;多路并归排序 看下最简单的&#xff0c;2路并归…

springboot线程池的使用和扩展

实战环境 windowns10&#xff1b;jdk1.8&#xff1b;springboot 1.5.9.RELEASE&#xff1b;开发工具&#xff1a;IntelliJ IDEA&#xff1b; 实战源码 本次实战的源码可以在我的GitHub下载&#xff0c;地址&#xff1a;gitgithub.com:zq2599/blog_demos.git&#xff0c;项目主…

统计单词个数

我是抄题解狂魔 /* 1.s.substr(x,len) 在s中取出从x位置开始&#xff0c;长度为len的字符串&#xff0c;并返回string类型的字符串。 2.s.find(a) 在s中查找字符串a,并返回起始下标&#xff08;从0开始&#xff09;&#xff0c;若不存在&#xff0c;返回1844674407370955161&am…

通过Rancher安装K8s

说明 我们用kubernetes去管理Docker集群&#xff0c;即可以将Docker看成Kubernetes内部使用的低级别组件。另外&#xff0c;kubernetes不仅仅支持Docker&#xff0c;还支持Rocket&#xff0c;这是另一种容器技术。希望我这篇文章中简单的描述能让你对两者有所理解和认识。 机…

35. 搜索插入位置-LeetCode

心得&#xff1a;这个题也是二分查找&#xff0c;但是有个小技巧&#xff1a;当left>right的时候 left就是要插入的位置。 代码&#xff1a; 1 class Solution {2 public int searchInsert(int[] nums, int target) {3 if(numsnull||nums.length0)4 …

Kubectl指令集

1 Kubectl指令集 1.1 Master查询节点信息 [rootmaster1 kubernetes-1.10]# kubectl get nodes 1.2 查询所有Pod信息 [rootmaster1 ~]# kubectl get pods --namespacekube-system 1.3 查询故障的Pod信息 [rootmaster1 ~]# kubectl get pods -n kube-sys…

SQL基础培训实战教程[全套]

学习简介&#xff1a;林枫山根据网上搜索资料进行参考&#xff0c;编写制作的SQL Server实操学习教程&#xff0c;欢迎下载学习。 下载链接目录如下&#xff1a; 进度0-SQL基础语法 下载学习文档 进度1-建数据表-美化版-2018-6-12 下载学习文档 进度2-关于主键-美化…

K8S仪表板Service unavailable故障的解决办法

K8S仪表板Service unavailable故障的解决办法 &#xff08;使用Rancher部署Kubernetes后访问仪表板提示Service unavailable的问题&#xff09; 一、逐项检查&#xff1a; 1、操作系统Kernel版本&#xff08;3.10以上&#xff09; 2、检查OS版本&#xff08;Ubuntu16.04.x、…

实验五报告

一、实验结论&#xff1a; 1. 二分查找&#xff1a;补足程序ex1_1.cpp// 练习&#xff1a;使用二分查找&#xff0c;在一组有序元素中查找数据项 // 形参是数组&#xff0c;实参是数组名 #include <stdio.h> const int N5; int binarySearch(int x[], int n, int item…

关于浏览器内核

介绍一下对浏览器内核的理解主要分成两个部分&#xff1a;渲染引擎(Render Engine)和JS引擎。常见的浏览器内核有哪些&#xff1f;Trident内核&#xff1a;IE&#xff0c;360&#xff0c;搜过浏览器&#xff1b;Gecko内核&#xff1a;Netscape6及以上版本&#xff0c;Presto内核…

docker 全部杀掉

杀死所有正在运行的容器 docker kill $(docker ps -a -q) 删除所有已经停止的容器 docker rm $(docker ps -a -q) 删除所有未打 dangling 标签的镜像 docker rmi $(docker images -q -f danglingtrue) 删除所有镜像 docker rmi $(docker images -q) 强制删除镜像名称中包含“do…

实验五 网络编程与安全-----实验报告

一、实验五 网络编程与安全-1 1.实验要求&#xff1a; 两人一组结对编程&#xff1a; &#xff08;1&#xff09;参考http://www.cnblogs.com/rocedu/p/6766748.html#SECDSA &#xff1b; &#xff08;2&#xff09;结对实现中缀表达式转后缀表达式的功能 MyBC.java&#xff1b…

K8S的HelloWorld之旅

安装kubectl。使用Google提供商&#xff08;如Google Container Engine或Amazon Web Services&#xff09;创建Kubernetes群集。本教程创建一个 外部负载均衡器&#xff0c;它需要一个云提供商。配置kubectl与Kubernetes API服务器通信。有关说明&#xff0c;请参阅云提供商的文…

思维构造——cf1090D

/* 只要找到两个没有关系的点即可 */ #include<bits/stdc.h> using namespace std; #define maxn 100005 long long n,m; int a[maxn],b[maxn]; vector<int>G[maxn]; int main(){cin>>n>>m;if(n1){puts("NO");return 0;}if(n*(n-1)/2<m)…

误删docker0网桥之后怎么办呢?

误删docker0网桥之后怎么办呢&#xff1f; 今天&#xff0c;在搭建k8s node节点环境的时候&#xff0c;好巧不巧&#xff0c;执行了如下命令&#xff1a; 1 2 [roothxin221 ~]# ifconfig docker0 down &>/dev/null [roothxin221 ~]# brctl delbr docker0 &>/de…

boost.asio学习

https://mmoaay.gitbooks.io/boost-asio-cpp-network-programming-chinese/content/Chapter1.html转载于:https://www.cnblogs.com/hshy/p/10930398.html

Harbor:私有企业级Registry仓库--快速搭建

前言 Harbor可以通过Docker Composer的方式来部署&#xff0c;如果有正常运行的k8s环境&#xff0c;也可以使用k8s来部署Harbor&#xff0c;本文采用 Docker Composer的方式。 准备 假定Linux系统为Centos 7。 docker &#xff0c;默认安装即可 yum -y install docker 1 dock…

java-Mysql学生管理系统

Window1//主方法 package stu_zizhu1; import java.awt.Button; import java.awt.Color; import java.awt.Dimension; import java.awt.FlowLayout; import java.awt.Point; import java.awt.event.ActionEvent; import java.awt.event.ActionListener; import javax.swing.JBu…

Docker版本Jenkins的使用

Docker版本Jenkins的使用 低调的微胖关注赞赏支持 Docker版本Jenkins的使用 12018.05.15 18:21:50字数 1202阅读 22588 一. 什么是Jenkins Jenkins是当前非常流行的一款持续集成工具&#xff0c;可以帮助大家把更新后的代码自动部署到服务器上运行。 二. 为什么用docker版…