面向对象第三单元总结

Posted atporter

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了面向对象第三单元总结相关的知识,希望对你有一定的参考价值。


单元内容

本单元的内容是实现一个社交关系模拟系统,通过各类输入指令来进行数据的增删查改等交互,具体内容如下:

  • 实现自己的 Person 和 Network 类,进行简单关系的模拟

  • 实现自己的 Group 类,丰富 Network 类,增加对分组关系的模拟

  • 丰富 Network 类,增加对复杂关系的模拟

JML语法

规格变量

  • 静态规格变量

    形如//@public static model non_null int []elements;

  • 实例规格变量

    形如//@public instance model non_null int []elements;

常用表达式

  • esult表达式:非void类型的方法的返回值

  • old(expr)表达式:表达式expr在方法执行前的取值

  • ot_assigned(x,y,...)表达式:方法执行过程中,括号中变量如果没有被赋值,返回true;否则false

  • forall 表达式

    形如(forall int i,j; 0 <= i && i < j && j < 10; a[i] < a[j])

    如果任意 0<=i<j<10,都有 a[i]<a[j],这个表达式为true;否则false

  • exists 表达式

    形如(exists int i; 0 <= i && i < 10; a[i] < 0)

    如果满足0<=i<10i中,至少有一个满足a[i] < 0,这个表达式为true;否则false

  • sum 表达式

    形如(sum int i; 0 <= i && i < 5; i * i)

    计算所有满足0 <= i && i < 5i * i的和,即0 + 1 + 4 + 9 + 16

方法规格

  • 正常行为规格(normal_behavior)

    • 前置条件(pre-condition)

      使用requires子句 requires P;,意思是“要求调用者确保P为真”

    • 后置条件(post-condition)

      使用ensures子句 ensures P;,意思是“方法实现者确保方法执行返回结果一定满足谓词P的要求,即确保P为真”

    • 副作用范围限定(side-e?ects)

      使用关键词 assignable,表示可赋值,后接一个或多个变量,或 othing 和 everything 两个关键词

  • 异常行为规格(exceptional_behavior)

    • signals子句

      signals (***Exception e) b_expr;,意思是当 b_expr 为 true 时,方法会抛出括号中给出的相应异常 e

    • signals_only子句

      signals_only ***Exception;,满足前置条件时抛出相应的异常

类型规格

  • 不变式invariant —— 在所有可见状态下都必须满足的特性

  • 状态变化约束constraint —— 对前序可见状态和当前可见状态的关系进行约束

public class ServiceCounter{ ? ?
	private /*@spec_public@*/ long counter; ? ?
	//@ invariant counter >= 0; ? ?
	//@ constraint counter == old(counter) + 1; 
}

表示:必须满足counter >= 0,每次修改counter只能加1

JML工具链

概述

  • OpenJML

    -check:对JML注释的规范性检查

    -esc:对程序的静态检查

    -rac:对程序的动态检查

  • SMT Solver:检查代码与规格的等价性

  • JMLUnitNG:生成测试数据

部署OpenJML

参考博客

对Group接口的JML语法检查结果如下:

技术图片

可见,错误只有找不到Person类,其他地方是通过的(检查Person则会直接通过)

部署JMLUnitNG

对于一个简单Demo的测试:

import java.math.BigInteger;

public class Demo {
    /*@ public normal_behavior
      @ requires i1 != null && i2 != null && flag == true;
      @ ensures 
esult == i1.xor(i2);
      @ also
      @ public normal_behavior
      @ requires i1 != null && i2 != null && flag == false;
      @ ensures 
esult == i1.or(i2);
      @ also
      @ public normal_behavior
      @ requires i1 == null || i2 == null;
      @ ensures 
esult == null;
      @*/
    public BigInteger calculate(BigInteger i1, BigInteger i2, boolean flag) {
        if (i1 == null || i2 == null) {
            return null;
        }
        if (flag) {
            return i1.xor(i2);
        } else {
            return i2.or(i1);
        }
    }
}

运行结果:

技术图片

架构分析

技术图片

前两次作业,完全按照JML规格进行架构,储存数据也全用 ArrayList ,此时性能要求还不高

第三次作业,方法复杂度激增,性能卡得也很严格,故进行了大范围的改动:

  • Person 类用 HashMap 储存熟人和对应的value值

  • 新增 Graph 类表示连通分支(所有有关系的人的集合)

    Network 类储存所有的连通分支,并在addPersonaddRelation时进行维护

    Graph 类实现了所有的关系查询方法,这样可以分担Network的任务,提高性能

在debug过程中又增加了Path类,实现了findPath方法,基于dfs对路径进行查询

Path 类只在qsl方法中用到,作为一点小优化

bug 分析

HW10(一个CTLE炸强测)

  • queryNameRank方法,完全是照搬JML规格,多了无谓的循环,多么惨痛的教训

HW11(CTLE、WA遍地开花)

  • borrowFrom方法,欲用 ArrayList 的set方法,手滑打成了add,竟然逃过了强测,互测被抓
  • queryMinPath方法超时,没有堆优化
  • queryStrongLinked方法超时,明明和标程思路一致,还是超时,推测是维护连通分支的代价太大

互测

原本是冲着超时的方向hack的,采取大量数据轰炸的策略,最后也发现了一些正确性上的错误

  • getAgeMeangetAgeVar的除0问题
  • getRelationSumgetValueSum不采用缓存会CTLE(互测环境也会)
  • getRelationSumgetValueSum采用缓存,先分组再加关系没有刷新,WA
  • queryMinPathqueryStrongLinked的CTLE互测中没有出现,但出现了WA

心得与体会

不要照搬JML规格!!不要照搬JML规格!!不要照搬JML规格!!

  1. 在我看来JML是一个隐藏的杀手,它并不像表面那样友好,而是杀人于无形,且一刀致命,可能一个地方没处理好就和互测告别了

    所以根据JML规格写程序的时候一定要谨慎再谨慎,尤其是调用之前实现的方法时,要判断复杂度会不会超标,第二次作业的时候我换掉了所有的contain,就落下了queryNameRank,强测就炸了

  2. 抛开课程而言,我们学习JML规格,不是目的,而是手段。

    对于程序设计来说,JML语言是比自然语言更好的信息储存和传递介质,它具有效率高、无二义等优点,还可以帮助我们更好地理解顶层设计与具体实现的关系

    用我的亲身体验来说明,我在阅读第一单元第二次作业的指导书时,没弄清幂函数的指数什么时候限制为(10^4),什么时候限制为(10^{10}),还以为(10^{10})是评测机要保证的限制,于是产生了bug。而这样的情况在JML单元就绝对不会出现,只要对JML语法认识正确,双方的思维就是一致的

以上是关于面向对象第三单元总结的主要内容,如果未能解决你的问题,请参考以下文章

面向对象第三单元总结

面向对象程序设计第三单元总结

面向对象程序设计第三单元总结

《面向对象程序设计》第三单元 JML 总结

面向对象第三单元总结

面向对象第三单元总结