其他分享
首页 > 其他分享> > 面向对象第三单元总结博客

面向对象第三单元总结博客

作者:互联网

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

(1)JML的程序语言理论

  JML(java建模语言)是一种行为接口规格语言(behavioral interface specification language),用于指定java模块的行为。JML结合了按契约设计的方法(design by contract approach, Eiffel)和Larch系列的基于模型的规格方法,Design by Contract with JML(Gary T. Leavens and Yoonsik Cheon, http://www.eecs.ucf.edu/~leavens/JML//jmldbc.pdf)阐述了JML的设计和用法。

(2)JML语法(JML level 0)

  1. JML表达式:

    JML表达式包括原子表达式、量化表达式和集合表达式,常用JML表达式如:

    \result :表示一个非void类型的方法执行所获得的结果,即方法执行后的返回值。

    \old(expr) :表示一个表达式expr在相应方法执行前的取值。

    \not_assigned(x,y,...) :表示括号中的变量是否在方法执行过程中被赋值。如果没有被赋值,返回为true,否则返回false

    \not_modified(x,y,...) :表示该表达式限制括号中的变量在方法执行期间的取值未发生变化。

    \forall :全称量词,表示对于给定范围内的元素,每个元素都满足相应的约束。

    \exists :存在量词,表示对于给定范围内的元素,存在某个元素满足相应的约束。

    \sum :表示给定范围内的表达式的和。

    \product :表示给定范围内的表达式的积。

    \max :表示给定范围内的表达式的最大值。

    \min :表示给定范围内的表达式的最小值。

    \nothing :空集。

    \everything :全集。

  2. 方法规格:

    JML方法规格包括正常行为规格(normal_behavior)和异常行为规格(exceptional_behavior),核心内容是前置条件(requires)、后置条件(ensures)和影响范围(assignable)。

    requires:对方法输入参数的限制,如果不满足前置条件,方法执行结果不可预测,不保证方法执行结果的正确性。

    ensures:对方法执行结果的限制,执行结果应当满足后置条件,否则执行错误。

    assignable:方法在执行过程中对输入对象或this对象所做的修改,如赋值。

  3. 类型规格:

    类型规格是对Java程序中定义的数据类型的限制规则,包括不变式限制(invariant)和约束限制(constraints)。

    invariant :要求在所有可见状态下都必须满足的特性。

    constraint :对状态的变化的约束,即对前序可见状态和当前可见状态的关系的约束。

(3)JML建模

  JML用行为描述、前置条件、后置条件、影响范围对方法的行为建模,用不变式和状态变化约束对类的数据域建模,实现完整的对类的状态和行为的规格化。

(4)JML工具链

  目前已有若干成熟的开源JML应用工具,包括jmlc(断言检查编译器),jmlunit(单元测试工具)及jmldoc(javadoc的增强版)。

二、部署JMLUnitNG并针对Group接口的实现自动生成测试用例

  执行过程如下:

  

  测试结果如下:

  Passed: racEnabled()
  Passed: constructor MyGroup(-2147483648)
  Passed: constructor MyGroup(0)
  Passed: constructor MyGroup(2147483647)
  Passed: <<test.MyGroup@5000001f>>.addPerson(null)
  Passed: <<test.MyGroup@1f>>.addPerson(null)
  Passed: <<test.MyGroup@5000001e>>.addPerson(null)
  Passed: <<test.MyGroup@5000001f>>.addRelation(-2147483648)
  Passed: <<test.MyGroup@1f>>.addRelation(-2147483648)
  Passed: <<test.MyGroup@5000001e>>.addRelation(-2147483648)
  Passed: <<test.MyGroup@5000001f>>.addRelation(0)
  Passed: <<test.MyGroup@1f>>.addRelation(0)
  Passed: <<test.MyGroup@5000001e>>.addRelation(0)
  Passed: <<test.MyGroup@5000001f>>.addRelation(2147483647)
  Passed: <<test.MyGroup@1f>>.addRelation(2147483647)
  Passed: <<test.MyGroup@5000001e>>.addRelation(2147483647)
  Passed: <<test.MyGroup@5000001f>>.delPerson(null)
  Passed: <<test.MyGroup@1f>>.delPerson(null)
  Passed: <<test.MyGroup@5000001e>>.delPerson(null)
  Passed: <<test.MyGroup@5000001f>>.equals(null)
  Passed: <<test.MyGroup@1f>>.equals(null)
  Passed: <<test.MyGroup@5000001e>>.equals(null)
  Passed: <<test.MyGroup@5000001f>>.equals(java.lang.Object@51016012)
  Passed: <<test.MyGroup@1f>>.equals(java.lang.Object@29444d75)
  Passed: <<test.MyGroup@5000001e>>.getAgeMean()
  Passed: <<test.MyGroup@5000001f>>.getAgeMean()
  Passed: <<test.MyGroup@1f>>.getAgeMean()
  Passed: <<test.MyGroup@5000001e>>.getAgeVar()
  Passed: <<test.MyGroup@5000001f>>.getAgeVar()
  Passed: <<test.MyGroup@1f>>.getAgeVar()
  Passed: <<test.MyGroup@5000001e>>.getConflictSum()
  Passed: <<test.MyGroup@5000001f>>.getConflictSum()
  Passed: <<test.MyGroup@1f>>.getConflictSum()
  Passed: <<test.MyGroup@5000001e>>.getId()
  Passed: <<test.MyGroup@5000001f>>.getId()
  Passed: <<test.MyGroup@1f>>.getId()
  Passed: <<test.MyGroup@5000001e>>.getPeopleSum()
  Passed: <<test.MyGroup@5000001f>>.getPeopleSum()
  Passed: <<test.MyGroup@1f>>.getPeopleSum()
  Passed: <<test.MyGroup@5000001e>>.getRelationSum()
  Passed: <<test.MyGroup@5000001f>>.getRelationSum()
  Passed: <<test.MyGroup@1f>>.getRelationSum()
  Passed: <<test.MyGroup@5000001e>>.getValueSum()
  Passed: <<test.MyGroup@5000001f>>.getValueSum()
  Passed: <<test.MyGroup@1f>>.getValueSum()
  Failed: <<test.MyGroup@5000001f>>.hasPerson(null)
  Failed: <<test.MyGroup@1f>>.hasPerson(null)
  Failed: <<test.MyGroup@5000001e>>.hasPerson(null)
  ===============================================
  Command line suite
  Total tests run: 48, Failures: 3, Skips: 0
  ===============================================

三、作业架构设计

  三次作业的架构基本相同,按规格实现官方包的接口。建模策略是首先阅读JML规格,理解整体的需求,再做设计,比如money可以做成person的属性。

  

四、作业bug及修复

  作业bug主要在于第二次作业时为了减少queryGroupRelationSum和queryGroupValueSum的运算次数在addRelation和addPerson中增加了很多判断,有一些考虑不周的漏洞,强测和互测时很多用例的执行结果都出现了错误。bug修复阶段在5行内修复了所有bug。

  

五、心得体会

  理解和撰写规格对于程序设计和测试都有很大的帮助,也利于以测试驱动开发。

标签:JML,规格,博客,面向对象,addRelation,表达式,Passed,null,单元
来源: https://www.cnblogs.com/buaa17373128/p/12944621.html