zoukankan html css js c++ java

oo第三次博客

一、梳理JML语言的理论基础、应用工具链情况

理论基础

JML(Java Modeling Language)是用于对Java程序进行规格化设计的一种表示语言。JML是一种行为接口规格语言
（Behavior Interface Specification Language，BISL），基于Larch方法构建。BISL提供了对方法和类型的规格定义
手段。所谓接口即一个方法或类型外部可见的内容。JML主要由Leavens教授在Larch上的工作，并融入了Betrand
Meyer， John Guttag等人关于Design by Contract的研究成果。近年来，JML持续受到关注，为严格的程序设计提供
了一套行之有效的方法。通过JML及其支持工具，不仅可以基于规格自动构造测试用例，并整合了SMT Solver等工具
以静态方式来检查代码实现对规格的满足情况

注释结构

　　JML以javadoc注释的方式来表示规格，每行都以@起头。有两种注释方式，行注释和块注释。其中行注释的表示方式
　　为 //@annotation ，块注释的方式为 /* @ annotation @*/ 。

JML表达式
- 原子表达式
  - esult表达式：表示一个非 void 类型的方法执行所获得的结果，即方法执行后的返回值。
  - old( expr )表达式：用来表示一个表达式 expr 在相应方法执行前的取值。
- 量化表达式
  - forall表达式：全称量词修饰的表达式，表示对于给定范围内的元素，每个元素都满足相应的约束。
  - exists表达式：存在量词修饰的表达式，表示对于给定范围内的元素，存在某个元素满足相应的约束。
- 操作符
  - 子类型关系操作符： E1<:E2 ，如果类型E1是类型E2的子类型(sub type)，则该表达式的结果为真，否则为假。
  - 等价关系操作符： b_expr1<==>b_expr2 或者 b_expr1<=!=>b_expr2 ，其中b_expr1和b_expr2都是布尔表达式，这两个表达式的意思是 b_expr1==b_expr2 或者 b_expr1!=b_expr2 。
  - 推理操作符： b_expr1==>b_expr2 或者 b_expr2<==b_expr1 。
方法规格
- 前置条件(pre-condition)：前置条件通过requires子句来表示： requires P。
- 后置条件(post-condition)：后置条件通过ensures子句来表示： ensures P。
类型规格
- 不变式（invariant）是要求在所有可见状态下都必须满足的特性，语法上定义 invariant P ，其中 invariant 为关键词， P 为谓词。对于类型规格而言，可见状态(visible state)是一个特别重要的概念。
- 状态变化约束（constraint）对象的状态在变化时往往也许满足一些约束，这种约束本质上也是一种不变式。

工具链

jmlrac: test for violations of assertions during execution

ESC/Java2: static verification; compile-time proving that contracts are never violated

jmldoc: javadoc-style documentation

jmlc: assertion-checking compilerj

jml4c: a new JML compiler built upon the Eclipse JDT open-source platform

SMT Solver: 验证程序等价性

OpenJML: 检查JML规范性

二、部署SMT Solver，至少选择3个主要方法来尝试进行验证，报告结果

对MyPath进行测试

TRACE of MyPath.compareTo(com.oocourse.specs3.models.Path)
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(THIS.nodes.content != null) || THIS.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(THIS.nodes.content != null) || THIS.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(THIS.nodeCounter.content != null) || THIS.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(THIS.nodeCounter.content != null) || THIS.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      requires o != null; 
            VALUE: o     === REF!val!64
            VALUE: null     === NULL
            VALUE: o != null     === true
E:eclipse-workspacejmlsrcMyPath.java:78: 注:      /*@ non_null */  Iterator<Integer> iter1 = this.iterator()
            VALUE: this.iterator()     === REF!val!103
            VALUE: iter1     === REF!val!103
E:eclipse-workspacejmlsrcMyPath.java:7: 注:      PossiblyNullDeReference assertion: _JML__tmp242376 != null
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      Precondition assertion: _$CPRE__26880
            VALUE: _$CPRE__26880     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242376.nodes.content != null) || _JML__tmp242376.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242376.nodes.content != null) || _JML__tmp242376.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242376.nodeCounter.content != null) || _JML__tmp242376.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242376.nodeCounter.content != null) || _JML__tmp242376.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:78: 注:      PossiblyNullInitialization assertion: _JML__tmp242377 != null
            VALUE: null     === NULL
E:eclipse-workspacejmlsrcMyPath.java:79: 注:      /*@ non_null */  Iterator<Integer> iter2 = p.iterator()
            VALUE: p     === REF!val!64
            VALUE: p.iterator()     === REF!val!130
            VALUE: iter2     === REF!val!130
E:eclipse-workspacejmlsrcMyPath.java:79: 注:      PossiblyNullDeReference assertion: _JML__tmp242393 != null
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      Precondition assertion: _$CPRE__26881
            VALUE: _$CPRE__26881     === true
E:eclipse-workspacejmlsrcMyPath.java:79: 注:      PossiblyNullInitialization assertion: _JML__tmp242394 != null
            VALUE: null     === NULL
E:eclipse-workspacejmlsrcMyPath.java:80: 注:      Loop test
            VALUE: iter1     === REF!val!103
            VALUE: iter1.hasNext()     === false
            VALUE: iter1.hasNext() && iter2.hasNext()     === false
            VALUE: (iter1.hasNext() && iter2.hasNext())     === false
E:eclipse-workspacejmlsrcMyPath.java:80: 注:      PossiblyNullDeReference assertion: _JML__tmp242403 != null
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      Precondition assertion: _$CPRE__26882
            VALUE: _$CPRE__26882     === true
E:eclipse-workspacejmlsrcMyPath.java:87: 注:      return Integer.compare(this.size(), p.size());
            VALUE: this.size()     === ( - 2147476275 )
            VALUE: p     === REF!val!64
            VALUE: p.size()     === ( - 2147480014 )
            VALUE: Integer.compare(this.size(), p.size())     === 0
E:eclipse-workspacejmlsrcMyPath.java:7: 注:      PossiblyNullDeReference assertion: _JML__tmp242581 != null
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      Precondition assertion: _$CPRE__26888
            VALUE: _$CPRE__26888     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242581.nodes.content != null) || _JML__tmp242581.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242581.nodes.content != null) || _JML__tmp242581.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242581.nodeCounter.content != null) || _JML__tmp242581.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242581.nodeCounter.content != null) || _JML__tmp242581.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:87: 注:      PossiblyNullDeReference assertion: _JML__tmp242595 != null
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      Precondition assertion: _$CPRE__26889
            VALUE: _$CPRE__26889     === true
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      Precondition assertion: _$CPRE__26887
            VALUE: _$CPRE__26887     === true
E:eclipse-workspacejmlsrcMyPath.java:8: 注:      NullField assertion: _JML__tmp242607
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(THIS.nodes.content != null) || THIS.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:8: 注:      Invariant assertion: !(THIS.nodes != null) || _JML__tmp242610
F:eclipsejee-photon2eclipseconfigurationorg.eclipse.osgi998.cpspecsjavautilCollection.jml:70: 注:  Invalid assertion (Invariant)

compareTo

TRACE of MyPath.equals(java.lang.Object)
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(THIS.nodes.content != null) || THIS.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(THIS.nodes.content != null) || THIS.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(THIS.nodeCounter.content != null) || THIS.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(THIS.nodeCounter.content != null) || THIS.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      requires this == obj; 
            VALUE: this     === THIS
            VALUE: obj     === THIS
            VALUE: this == obj     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      requires obj != null && typeof(this) == 	ype(Object); 
            VALUE: obj     === THIS
            VALUE: null     === NULL
            VALUE: obj != null     === true
            VALUE: this     === THIS
            VALUE: typeof(this)     === JMLTypeSort!val!55
            VALUE: 	ype(Object)     === JMLTypeSort!val!6
            VALUE: typeof(this) == 	ype(Object)     === false
            VALUE: obj != null && typeof(this) == 	ype(Object)     === false
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      requires obj == null; 
            VALUE: obj     === THIS
            VALUE: null     === NULL
            VALUE: obj == null     === false
E:eclipse-workspacejmlsrcMyPath.java:40: 注:      if (!(obj instanceof Path)) ...
            VALUE: obj     === THIS
            VALUE: obj instanceof Path     === true
            VALUE: (obj instanceof Path)     === true
            VALUE: !(obj instanceof Path)     === false
            VALUE: (!(obj instanceof Path))     === false
                Condition = false
E:eclipse-workspacejmlsrcMyPath.java:43: 注:      if (nodes.size() != ((Path)obj).size()) ...
            VALUE: nodes     === REF!val!78
            VALUE: nodes.size()     === 2275
            VALUE: obj     === THIS
            VALUE: (Path)obj     === THIS
            VALUE: ((Path)obj)     === THIS
            VALUE: ((Path)obj).size()     === 2275
            VALUE: nodes.size() != ((Path)obj).size()     === false
            VALUE: (nodes.size() != ((Path)obj).size())     === false
                Condition = false
E:eclipse-workspacejmlsrcMyPath.java:43: 注:      PossiblyNullDeReference assertion: _JML__tmp785 != null
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      //@ public invariant content.owner == this; 
            VALUE: content.owner     === REF!val!78
            VALUE: this     === REF!val!78
            VALUE: content.owner == this     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp785.content != null) || _JML__tmp785.content != null
E:eclipse-workspacejmlsrcMyPath.java:43: 注:      InvariantLeaveCaller assertion: _JML__tmp787
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      //@ public invariant content.theSize >= 0; 
            VALUE: content.theSize     === 2275
            VALUE: 0     === 0
            VALUE: content.theSize >= 0     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp785.content != null) || _JML__tmp785.content != null
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      InvariantLeaveCaller assertion: _JML__tmp789
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      //@ public invariant content.owner == this; 
            VALUE: content.owner     === REF!val!78
            VALUE: this     === REF!val!78
            VALUE: content.owner == this     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp785.content != null) || _JML__tmp785.content != null
E:eclipse-workspacejmlsrcMyPath.java:43: 注:      InvariantLeaveCaller assertion: _JML__tmp790
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      //@ public invariant content.theSize >= 0; 
            VALUE: content.theSize     === 2275
            VALUE: 0     === 0
            VALUE: content.theSize >= 0     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp785.content != null) || _JML__tmp785.content != null
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      InvariantLeaveCaller assertion: _JML__tmp792
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      //@ public invariant content.owner == this; 
            VALUE: content.owner     === REF!val!78
            VALUE: this     === REF!val!78
            VALUE: content.owner == this     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp785.content != null) || _JML__tmp785.content != null
E:eclipse-workspacejmlsrcMyPath.java:43: 注:      InvariantEntrance assertion: _JML__tmp793
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      //@ public invariant content.theSize >= 0; 
            VALUE: content.theSize     === 2275
            VALUE: 0     === 0
            VALUE: content.theSize >= 0     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp785.content != null) || _JML__tmp785.content != null
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      InvariantEntrance assertion: _JML__tmp795
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      //@ public invariant content.owner == this; 
            VALUE: content.owner     === REF!val!78
            VALUE: this     === REF!val!78
            VALUE: content.owner == this     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp785.content != null) || _JML__tmp785.content != null
E:eclipse-workspacejmlsrcMyPath.java:43: 注:      InvariantEntrance assertion: _JML__tmp796
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      //@ public invariant content.theSize >= 0; 
            VALUE: content.theSize     === 2275
            VALUE: 0     === 0
            VALUE: content.theSize >= 0     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp785.content != null) || _JML__tmp785.content != null
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      InvariantEntrance assertion: _JML__tmp798
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      Precondition assertion: _$CPRE__35
            VALUE: _$CPRE__35     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      //@ public invariant content.owner == this; 
            VALUE: content.owner     === REF!val!78
            VALUE: this     === REF!val!78
            VALUE: content.owner == this     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp785.content != null) || _JML__tmp785.content != null
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      //@ public invariant content.theSize >= 0; 
            VALUE: content.theSize     === 2275
            VALUE: 0     === 0
            VALUE: content.theSize >= 0     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp785.content != null) || _JML__tmp785.content != null
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      //@ public invariant content.owner == this; 
            VALUE: content.owner     === REF!val!78
            VALUE: this     === REF!val!78
            VALUE: content.owner == this     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp785.content != null) || _JML__tmp785.content != null
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      //@ public invariant content.theSize >= 0; 
            VALUE: content.theSize     === 2275
            VALUE: 0     === 0
            VALUE: content.theSize >= 0     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp785.content != null) || _JML__tmp785.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp799 && _JML__tmp785.content != null) || _JML__tmp785.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp799 && _JML__tmp785.values != null) || _JML__tmp785.values != null
E:eclipse-workspacejmlsrcMyPath.java:43: 注:      PossiblyBadCast assertion: obj == null || obj instanceof com.oocourse.specs3.models.Path
E:eclipse-workspacejmlsrcMyPath.java:43: 注:      PossiblyNullDeReference assertion: _JML__tmp814 != null
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      Precondition assertion: _$CPRE__36
            VALUE: _$CPRE__36     === true
E:eclipse-workspacejmlsrcMyPath.java:46: 注:      /*@ non_null */  Iterator<Integer> iter1 = this.iterator()
            VALUE: this.iterator()     === REF!val!105
            VALUE: iter1     === REF!val!105
E:eclipse-workspacejmlsrcMyPath.java:7: 注:      PossiblyNullDeReference assertion: _JML__tmp822 != null
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      Precondition assertion: _$CPRE__37
            VALUE: _$CPRE__37     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp822.nodes.content != null) || _JML__tmp822.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp822.nodes.content != null) || _JML__tmp822.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp822.nodeCounter.content != null) || _JML__tmp822.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp822.nodeCounter.content != null) || _JML__tmp822.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:46: 注:      PossiblyNullInitialization assertion: _JML__tmp823 != null
            VALUE: null     === NULL
E:eclipse-workspacejmlsrcMyPath.java:47: 注:      /*@ non_null */  Iterator<Integer> iter2 = ((Path)obj).iterator()
            VALUE: obj     === THIS
            VALUE: (Path)obj     === THIS
            VALUE: ((Path)obj)     === THIS
            VALUE: ((Path)obj).iterator()     === REF!val!105
            VALUE: iter2     === REF!val!105
E:eclipse-workspacejmlsrcMyPath.java:47: 注:      PossiblyBadCast assertion: obj == null || obj instanceof com.oocourse.specs3.models.Path
E:eclipse-workspacejmlsrcMyPath.java:47: 注:      PossiblyNullDeReference assertion: _JML__tmp840 != null
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      Precondition assertion: _$CPRE__38
            VALUE: _$CPRE__38     === true
E:eclipse-workspacejmlsrcMyPath.java:47: 注:      PossiblyNullInitialization assertion: _JML__tmp841 != null
            VALUE: null     === NULL
E:eclipse-workspacejmlsrcMyPath.java:48: 注:      Loop test
            VALUE: iter1     === REF!val!105
            VALUE: iter1.hasNext()     === true
            VALUE: iter2     === REF!val!105
            VALUE: iter2.hasNext()     === true
            VALUE: iter1.hasNext() && iter2.hasNext()     === true
            VALUE: (iter1.hasNext() && iter2.hasNext())     === true
E:eclipse-workspacejmlsrcMyPath.java:48: 注:      PossiblyNullDeReference assertion: _JML__tmp850 != null
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      Precondition assertion: _$CPRE__39
            VALUE: _$CPRE__39     === true
E:eclipse-workspacejmlsrcMyPath.java:48: 注:      PossiblyNullDeReference assertion: _JML__tmp858 != null
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      Precondition assertion: _$CPRE__40
            VALUE: _$CPRE__40     === true
E:eclipse-workspacejmlsrcMyPath.java:49: 注:      if (!iter1.next().equals(iter2.next())) ...
            VALUE: iter1     === REF!val!105
            VALUE: iter1.next()     === REF!val!142
            VALUE: iter2     === REF!val!105
            VALUE: iter2.next()     === REF!val!145
            VALUE: iter1.next().equals(iter2.next())     === false
            VALUE: !iter1.next().equals(iter2.next())     === true
            VALUE: (!iter1.next().equals(iter2.next()))     === true
                Condition = true
E:eclipse-workspacejmlsrcMyPath.java:49: 注:      PossiblyNullDeReference assertion: _JML__tmp867 != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      requires moreElements; 
            VALUE: moreElements     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      requires !moreElements; 
            VALUE: moreElements     === true
            VALUE: !moreElements     === false
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      Precondition assertion: _$CPRE__42
            VALUE: _$CPRE__42     === true
E:eclipse-workspacejmlsrcMyPath.java:49: 注:      PossiblyNullDeReference assertion: _JML__tmp943 != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      requires moreElements; 
            VALUE: moreElements     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      requires !moreElements; 
            VALUE: moreElements     === true
            VALUE: !moreElements     === false
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      Precondition assertion: _$CPRE__43
            VALUE: _$CPRE__43     === true
E:eclipse-workspacejmlsrcMyPath.java:49: 注:      Exception thrown by next()
            VALUE: _JML___exceptionCall     === REF!val!156
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      Terminated with exception
            VALUE: _JML___exception     === REF!val!156
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      signals () false; 
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      ExceptionalPostcondition assertion: !Pre_2 || false
E:eclipse-workspacejmlsrcMyPath.java:49: 注:  Invalid assertion (ExceptionalPostcondition)
: F:eclipsejee-photon2eclipseconfigurationorg.eclipse.osgi998.cpspecsjavalangObject.jml:76: 注:  Associated location

equals

TRACE of MyPath.hashCode()
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(THIS.nodes.content != null) || THIS.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(THIS.nodes.content != null) || THIS.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(THIS.nodeCounter.content != null) || THIS.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(THIS.nodeCounter.content != null) || THIS.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:92: 注:      return nodes.hashCode();
            VALUE: nodes     === REF!val!57
            VALUE: nodes.hashCode()     === ( - 2147473923 )
E:eclipse-workspacejmlsrcMyPath.java:92: 注:      PossiblyNullDeReference assertion: _JML__tmp242634 != null
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      //@ public invariant content.owner == this; 
            VALUE: content.owner     === REF!val!57
            VALUE: this     === REF!val!57
            VALUE: content.owner == this     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242634.content != null) || _JML__tmp242634.content != null
E:eclipse-workspacejmlsrcMyPath.java:92: 注:      InvariantLeaveCaller assertion: _JML__tmp242636
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      //@ public invariant content.theSize >= 0; 
            VALUE: content.theSize     === 1142
            VALUE: 0     === 0
            VALUE: content.theSize >= 0     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242634.content != null) || _JML__tmp242634.content != null
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      InvariantLeaveCaller assertion: _JML__tmp242638
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      //@ public invariant content.owner == this; 
            VALUE: content.owner     === REF!val!57
            VALUE: this     === REF!val!57
            VALUE: content.owner == this     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242634.content != null) || _JML__tmp242634.content != null
E:eclipse-workspacejmlsrcMyPath.java:92: 注:      InvariantLeaveCaller assertion: _JML__tmp242639
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      //@ public invariant content.theSize >= 0; 
            VALUE: content.theSize     === 1142
            VALUE: 0     === 0
            VALUE: content.theSize >= 0     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242634.content != null) || _JML__tmp242634.content != null
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      InvariantLeaveCaller assertion: _JML__tmp242641
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      //@ public invariant content.owner == this; 
            VALUE: content.owner     === REF!val!57
            VALUE: this     === REF!val!57
            VALUE: content.owner == this     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242634.content != null) || _JML__tmp242634.content != null
E:eclipse-workspacejmlsrcMyPath.java:92: 注:      InvariantEntrance assertion: _JML__tmp242642
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      //@ public invariant content.theSize >= 0; 
            VALUE: content.theSize     === 1142
            VALUE: 0     === 0
            VALUE: content.theSize >= 0     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242634.content != null) || _JML__tmp242634.content != null
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      InvariantEntrance assertion: _JML__tmp242644
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      //@ public invariant content.owner == this; 
            VALUE: content.owner     === REF!val!57
            VALUE: this     === REF!val!57
            VALUE: content.owner == this     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242634.content != null) || _JML__tmp242634.content != null
E:eclipse-workspacejmlsrcMyPath.java:92: 注:      InvariantEntrance assertion: _JML__tmp242645
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      //@ public invariant content.theSize >= 0; 
            VALUE: content.theSize     === 1142
            VALUE: 0     === 0
            VALUE: content.theSize >= 0     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242634.content != null) || _JML__tmp242634.content != null
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      InvariantEntrance assertion: _JML__tmp242647
E:eclipse-workspacejmlsrcMyPath.java:1: 注:      Precondition assertion: _$CPRE__26890
            VALUE: _$CPRE__26890     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      //@ public invariant content.owner == this; 
            VALUE: content.owner     === REF!val!57
            VALUE: this     === REF!val!57
            VALUE: content.owner == this     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242634.content != null) || _JML__tmp242634.content != null
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      //@ public invariant content.theSize >= 0; 
            VALUE: content.theSize     === 1142
            VALUE: 0     === 0
            VALUE: content.theSize >= 0     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242634.content != null) || _JML__tmp242634.content != null
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      //@ public invariant content.owner == this; 
            VALUE: content.owner     === REF!val!57
            VALUE: this     === REF!val!57
            VALUE: content.owner == this     === true
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242634.content != null) || _JML__tmp242634.content != null
E:eclipse-workspacejmlsrcMyPath.java:93: 注:      //@ public invariant content.theSize >= 0; 
            VALUE: content.theSize     === 1142
            VALUE: 0     === 0
            VALUE: content.theSize >= 0     === true
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(_JML__tmp242634.content != null) || _JML__tmp242634.content != null
E:eclipse-workspacejmlsrcMyPath.java:8: 注:      NullField assertion: _JML__tmp242661
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(THIS.nodes.content != null) || THIS.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:8: 注:      Invariant assertion: !(THIS.nodes != null) || _JML__tmp242664
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(THIS.nodes.content != null) || THIS.nodes.content != null
E:eclipse-workspacejmlsrcMyPath.java:8: 注:      Invariant assertion: !(THIS.nodes != null) || _JML__tmp242666
E:eclipse-workspacejmlsrcMyPath.java:9: 注:      NullField assertion: _JML__tmp242669
E:eclipse-workspacejmlsrcMyPath.java:91: 注:      UndefinedNullDeReference assertion: !(THIS.nodeCounter.content != null) || THIS.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:9: 注:      Invariant assertion: !(THIS.nodeCounter != null) || _JML__tmp242672
E:eclipse-workspacejmlsrcMyPath.java:95: 注:      UndefinedNullDeReference assertion: !(THIS.nodeCounter.content != null) || THIS.nodeCounter.content != null
E:eclipse-workspacejmlsrcMyPath.java:9: 注:      Invariant assertion: !(THIS.nodeCounter != null) || _JML__tmp242674
E:eclipse-workspacejmlsrcMyPath.java:81: 注:      ensures 
esult == theHashCode; 
            VALUE: 
esult     === ( - 2147473923 )
            VALUE: theHashCode     === ( - 2147473923 )
            VALUE: 
esult == theHashCode     === true
E:eclipse-workspacejmlsrcMyPath.java:92: 注:  Invalid assertion (Postcondition)
: F:eclipsejee-photon2eclipseconfigurationorg.eclipse.osgi998.cpspecsjavalangObject.jml:63: 注:  Associated location

hashCode

对MyRailwaySystem进行测试

错误反馈

TRACE of MyRailwaySystem.addPath(com.oocourse.specs3.models.Path)
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(THIS.idPathMap.content != null) || THIS.idPathMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(THIS.pathIdMap.content != null) || THIS.pathIdMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:57: 注:      if (path == null || !path.isValid()) ...
            VALUE: path     === REF!val!81
            VALUE: null     === NULL
            VALUE: path == null     === false
            VALUE: path     === REF!val!81
            VALUE: path.isValid()     === false
            VALUE: !path.isValid()     === true
            VALUE: path == null || !path.isValid()     === true
            VALUE: (path == null || !path.isValid())     === true
                Condition = true
E:eclipse-workspacejmlsrcMyRailwaySystem.java:57: 注:      PossiblyNullDeReference assertion: _JML__tmp594 != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:1: 注:      Precondition assertion: _$CPRE__142
            VALUE: _$CPRE__142     === true
E:eclipse-workspacejmlsrcMyRailwaySystem.java:58: 注:      return 0;
            VALUE: 0     === 0
E:eclipse-workspacejmlsrcMyRailwaySystem.java:13: 注:      NullField assertion: _JML__tmp1322
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(THIS.idPathMap.content != null) || THIS.idPathMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:13: 注:      Invariant assertion: !(THIS.idPathMap != null) || _JML__tmp1325
F:eclipsejee-photon2eclipseconfigurationorg.eclipse.osgi998.cpspecsjavautilMap.jml:76: 注:  Invalid assertion (Invariant)

addPath

TRACE of MyRailwaySystem.containsEdge(int,int)
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(THIS.idPathMap.content != null) || THIS.idPathMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(THIS.pathIdMap.content != null) || THIS.pathIdMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      if (containsNode(fromNodeId) && containsNode(toNodeId)) ...
            VALUE: fromNodeId     === ( - 2147483610 )
            VALUE: containsNode(fromNodeId)     === true
            VALUE: toNodeId     === ( - 2147475929 )
            VALUE: containsNode(toNodeId)     === true
            VALUE: containsNode(fromNodeId) && containsNode(toNodeId)     === true
            VALUE: (containsNode(fromNodeId) && containsNode(toNodeId))     === true
                Condition = true
E:eclipse-workspacejmlsrcMyRailwaySystem.java:1: 注:      Precondition assertion: _$CPRE__448
            VALUE: _$CPRE__448     === true
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(_JML__tmp2101.idPathMap.content != null) || _JML__tmp2101.idPathMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(_JML__tmp2101.pathIdMap.content != null) || _JML__tmp2101.pathIdMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:1: 注:      Precondition assertion: _$CPRE__449
            VALUE: _$CPRE__449     === true
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(_JML__tmp2114.idPathMap.content != null) || _JML__tmp2114.idPathMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(_JML__tmp2114.pathIdMap.content != null) || _JML__tmp2114.pathIdMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:105: 注:      return monitor.containsEdge(fromNodeId, toNodeId);
            VALUE: monitor     === REF!val!146
            VALUE: fromNodeId     === ( - 2147483610 )
            VALUE: toNodeId     === ( - 2147475929 )
            VALUE: monitor.containsEdge(fromNodeId, toNodeId)     === false
E:eclipse-workspacejmlsrcMyRailwaySystem.java:105: 注:      PossiblyNullDeReference assertion: _JML__tmp2129 != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:1: 注:      Precondition assertion: _$CPRE__450
            VALUE: _$CPRE__450     === true
E:eclipse-workspacejmlsrcMyRailwaySystem.java:13: 注:      NullField assertion: _JML__tmp2144
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(THIS.idPathMap.content != null) || THIS.idPathMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:13: 注:      Invariant assertion: !(THIS.idPathMap != null) || _JML__tmp2147
E:eclipse-workspacejmlsrcMyRailwaySystem.java:14: 注:      NullField assertion: _JML__tmp2150
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(THIS.pathIdMap.content != null) || THIS.pathIdMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:14: 注:      Invariant assertion: !(THIS.pathIdMap != null) || _JML__tmp2153
F:eclipsejee-photon2eclipseconfigurationorg.eclipse.osgi998.cpspecsjavautilMap.jml:76: 注:  Invalid assertion (Invariant)

containsEdge

TRACE of MyRailwaySystem.getShortestPathLength(int,int)
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(THIS.idPathMap.content != null) || THIS.idPathMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(THIS.pathIdMap.content != null) || THIS.pathIdMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:129: 注:      if (!isConnected(fromNodeId, toNodeId)) ...
            VALUE: fromNodeId     === ( - 2147475929 )
            VALUE: toNodeId     === ( - 2147475928 )
            VALUE: isConnected(fromNodeId, toNodeId)     === true
            VALUE: !isConnected(fromNodeId, toNodeId)     === false
            VALUE: (!isConnected(fromNodeId, toNodeId))     === false
                Condition = false
E:eclipse-workspacejmlsrcMyRailwaySystem.java:1: 注:      Precondition assertion: _$CPRE__485
            VALUE: _$CPRE__485     === true
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(_JML__tmp2312.idPathMap.content != null) || _JML__tmp2312.idPathMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(_JML__tmp2312.pathIdMap.content != null) || _JML__tmp2312.pathIdMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:131: 注:      if (fromNodeId == toNodeId) ...
            VALUE: fromNodeId     === ( - 2147475929 )
            VALUE: toNodeId     === ( - 2147475928 )
            VALUE: fromNodeId == toNodeId     === false
            VALUE: (fromNodeId == toNodeId)     === false
                Condition = false
E:eclipse-workspacejmlsrcMyRailwaySystem.java:134: 注:      return monitor.query().distance(fromNodeId, toNodeId);
            VALUE: monitor     === REF!val!130
            VALUE: monitor.query()     === REF!val!220
            VALUE: fromNodeId     === ( - 2147475929 )
            VALUE: toNodeId     === ( - 2147475928 )
            VALUE: monitor.query().distance(fromNodeId, toNodeId)     === 0
E:eclipse-workspacejmlsrcMyRailwaySystem.java:134: 注:      PossiblyNullDeReference assertion: _JML__tmp2334 != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:1: 注:      Precondition assertion: _$CPRE__488
            VALUE: _$CPRE__488     === true
E:eclipse-workspacejmlsrcMyRailwaySystem.java:134: 注:      PossiblyNullDeReference assertion: _JML__tmp2351 != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:1: 注:      Precondition assertion: _$CPRE__487
            VALUE: _$CPRE__487     === true
E:eclipse-workspacejmlsrcMyRailwaySystem.java:13: 注:      NullField assertion: _JML__tmp2365
E:eclipse-workspacejmlsrcMyRailwaySystem.java:104: 注:      UndefinedNullDeReference assertion: !(THIS.idPathMap.content != null) || THIS.idPathMap.content != null
E:eclipse-workspacejmlsrcMyRailwaySystem.java:13: 注:      Invariant assertion: !(THIS.idPathMap != null) || _JML__tmp2368
F:eclipsejee-photon2eclipseconfigurationorg.eclipse.osgi998.cpspecsjavautilMap.jml:76: 注:  Invalid assertion (Invariant)

getShortestPathLength

三、部署JMLUnitNG/JMLUnit，实现自动生成测试用例

我使用的JML Level 0 手册中的样例来测试，因为Graph中尝试了修改规格，但是任然无法避免forall和exist的使用，下面是Student的代码

 1 public class Student {
 2     private /*@ spec_public @*/ String name;
 3     //@ public invariant credits >= 0;
 4     private /*@ spec_public @*/ int credits;
 5     /*@ public invariant credits < 180 ==> !master &&
 6       @ credits >= 180 ==> master;
 7       @*/
 8     private /*@ spec_public @*/ boolean master;
 9     /*@ requires sname != null;
10       @ assignable everything;
11       @ ensures name == sname && credits == 0 && master == false;
12       @*/
13     public Student (String sname) {
14         name = sname;
15         credits = 0;
16         master = false;
17     }
18 
19     /*@ requires c >= 0;
20       @ ensures credits == old(credits) + c;
21       @ assignable credits, master;
22       @ ensures (credits > 180) ==> master;
23       @ */
24     public void addCredits(int c) {
25         updateCredits(c);
26         if (credits >= 180) {
27             changeToMaster();
28         }
29     }
30 
31     /*@ requires c >= 0;
32       @ ensures credits == old(credits) + c;
33       @ assignable credits;
34       @*/
35     private void updateCredits(int c) {
36         credits += c;
37     }
38 
39     /*@ requires credits >= 180;
40       @ ensures master;
41       @ assignable master;
42       @*/
43     private void changeToMaster() {
44         master = true;
45     }
46 
47     /*@ ensures this.name == name;
48       @ assignable this.name;
49       @*/
50     public void setName(String name) {
51         this.name = name;
52     }
53 
54     /*@ ensures 
esult == name;
55     @*/
56     public /*@ pure @*/ String getName() {
57         return name;
58     }
59 }

View Code

测试验证，结果都可以通过

测试分析：自动生成的测试样例测试了两个不同对象在addCredits的参数中包括最大整数和最小整数和0，测试了两个不同对象的getName方法，以及setName，其中参数为Null或者为空的时候的情况。

四、按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构　　　　　　　　

第一次作业

为了实现对节点的计数我另外创建了一个结构NodeCounter，对于path中的节点可以直接使用HashSet来实现，但是对于PathContainer中的节点，由于有路径的增加和删除所以需要对不同的节点进行计数，为了避免复杂度出现问题，就以节点为key，节点的出现册数为value建立hashMap，然后将增加路径和删除路径的操作封装起来供PathContainer来进行调用

第二次作业

由于需要计算最短路径，所以在上次的结构基础上额外增加了计算最短路径的Distance类。

NodeMonitor：NodeMonitor是MyPathContainer中的一个对象，这个对象实现了对查询和删除功能的封装，如果需要增删与查询直接调用这个对象的方法即可。当每次在NodeMonitor中进行加减路径的时候，都将NodeMonitor中的newest置为false；每次对NodeMonitor进行查询的时候，如果发现不是最新的(newest为false)，则清空distance，然后根据新的请求重新计算并存储在distance的距离矩阵中，如果一直不发生写操作，那么距离矩阵就可以一直进行缓存。

Distance：在distance中对求解联通性和最短距离进行统一建模，对每次求解过的源点加入primaryKey中。

连通性：先看是否在primaryKey中是否存在起点或者终点，如果存在说明已经以起点或者终点计算过最短路径，然后看是否在距离矩阵中存在起点和重点之间的距离，如果在primaryKey中存在起点或者终点，但是没有起点和终点之间的距离，说明不连通，如果存在则说明联通；如果在primaryKey中不存在起点或者终点，那么以起点为源计算最短路，并将起点加入primaryKey，然后返回起点和终点之间是否存在路径。
最短距离：直接返回对应的距离值即可，因为调用最短距离之前一定判断过联通性，所以联通的点对之间的距离一定存在。

第三次作业

Monitor：由于功能的增加，Monitor相当于继续扩展了原来NodeMonitor的功能，保留了原来除增删路径的方法之外，并新添加了其他相关的查询方法，做到查询和增删功能的单独封装。和之前一样，Monitor只是MyRailwaySystem中的一个查询对象，需要查询什么就直接调用Monitor对象即可。

Nodes：辅助类，存储所有的Station，同样需要实现增删路径的方法。

Station：辅助类，存储一个NodeId和地铁线编号pathId

StaionDistance：辅助类，用于计算Dijkstra中最短路径的距离和Station点对，实现了Comparable接口。

WeightedGraph：对于换乘票价以及不满意度，都统一进行拆点并构造有权图来建模，有权图中存权重矩阵和距离矩阵，以及一个Nodes对象，根据不同的需求对非换成站边权以及换乘站边权进行初始化，然后采用Dijkstra的方法来计算最短路径并缓存

Pleasure：由于不满意度的边权计算与换乘和票价不太相同，所以Pleasure继承了有权图，并重写了构建边权的方法。

UnweightedGraph：这个类与上次的distance类是一样的，为了名字统一叫做UnweightedGraph

Matrix：由于有权图中权重矩阵，距离矩阵，无权图中的距离矩阵都用到了嵌套的HashMap，所以我重新封装了这次作业中嵌套hashMap的add和remove方法，以及containsKey等方法。在有权图中Key的类型可能是Station，也可能是Integer所以需要利用泛型来解决。

import java.util.HashMap;

public class Matrix<T> {
    private HashMap<T, HashMap<T, Integer>> matrix = new HashMap<>();

    public Matrix() {

    }

    public void clear() {
        matrix.clear();
    }

    public void add(T firstKey, T secondKey, int value) {
        if (matrix.containsKey(firstKey)) {
            matrix.get(firstKey).put(secondKey, value);
        } else {
            HashMap<T, Integer> secondHash = new HashMap<>();
            secondHash.put(secondKey, value);
            matrix.put(firstKey, secondHash);
        }
    }

    public void remove(T firstKey, T secondKey) {
        if (matrix.containsKey(firstKey) &&
                matrix.get(firstKey).containsKey(secondKey)) {
            matrix.get(firstKey).remove(secondKey);
            if (matrix.get(firstKey).size() == 0) {
                matrix.remove(firstKey);
            }
        }
    }

    public HashMap<T, Integer> get(T key) {
        return matrix.get(key);
    }

    public Integer get(T firstKey, T secondKey) {
        return matrix.get(firstKey).get(secondKey);
    }

    public boolean containsKey(T firstKey, T secondKey) {
        return matrix.containsKey(firstKey) &&
                matrix.get(firstKey).containsKey(secondKey);
    }
}

View Code

Connectivity：实现了计算连通块的数量和判断联通性的查询功能，根据pathId建立邻接矩阵，描述path之间的邻接关系，同样需要对应实现增加路径和删除路径的方法add和remove方法，由于写指令数很少，所以最多有50个点，所以每次无论查询连通性或者计算联通块数都要通过BFS将path分块，然后将pathId和块号建立映射。Connectivity中有和WeightedGraph共享的Nodes对象，所以根据Nodes对象即可知道NodeId与pathId的映射，所以根据这两个映射，可以根据pathId来找块号，从而判断联通性。块数的查询直接返回存储联通块的容器的大小即可。

五、按照作业分析代码实现的bug和修复情况

第一次作业：时间复杂度没有考虑，所以之后修改为利用Hashmap来查询访问的方式。

第二次作业：计算最短路径时，忘记考虑是否以该源点计算过最短距离的问题，只要存在key但是不存在value就认为不连通，因为比如一开始查询1-5的距离，然后查询5-6，由于1-5的距离对称填到key为5和1的矩阵行，这时5-6之间是没有计算而不是算出来距离不存在，导致联通性判断错误，改为通过使用primaryKey来计算以其为源点计算过的NodeId。

第三次作业：在联通性计算的时候直接使用的path对象，而忘记使用pathId，导致每次插入hashMap的时候每次比较path对象，时间复杂度过高，改为之后使用pathId来区分path。

六、阐述对规格撰写和理解上的心得体会

使用规格使我们的代码便于进行自动化检查和测试，大大提高了正确率，通过学习规格我学到了很多。

查看全文

相关阅读:
现在SimpleMemory的CSS(by BNDong)
I AK IOI
最大半联通子图
 曾经SimpleMemory的CSS
幼儿园战争
 炸掉卡西欧991CNX
LuoguP1131选择客栈
 2019CSP-S2养成任务
 NOIP2013&NOIP2018&USACO 三倍经验铺路题巧妙解法
 NOIP2018D2T1 旅行

原文地址：https://www.cnblogs.com/wangyanpeng/p/10905100.html

oo第三次博客

一、梳理JML语言的理论基础、应用工具链情况

理论基础

注释结构

JML表达式

原子表达式

量化表达式

操作符

方法规格

类型规格

工具链

二、部署SMT Solver，至少选择3个主要方法来尝试进行验证，报告结果

对MyPath进行测试

对MyRailwaySystem进行测试

三、部署JMLUnitNG/JMLUnit，实现自动生成测试用例

四、按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构

第一次作业

第二次作业

第三次作业

五、按照作业分析代码实现的bug和修复情况

六、阐述对规格撰写和理解上的心得体会

四、按照作业梳理自己的架构设计，并特别分析迭代中对架构的重构　　　　　　　　