标签：Requires array 出现 exce www demo row work 程序设计
本单元的内容是实现一个社交关系模拟系统，通过各类输入指令来进行数据的增删查改等交互，具体内容如下：
实现自己的 Person 和 Network 类，进行简单关系的模拟
实现自己的 Group 类，丰富 Network 类，增加对分组关系的模拟
丰富 Network 类，增加对复杂关系的模拟
静态规格变量
形如//@public static model non_null int []elements;
实例规格变量
形如//@public instance model non_null int []elements;
\result表达式：非void类型的方法的返回值
\old(expr)表达式：表达式expr在方法执行前的取值
\not_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<10的i中，至少有一个满足a[i] < 0，这个表达式为true；否则false
\sum 表达式
形如(\sum int i; 0 <= i && i < 5; i * i)
计算所有满足0 <= i && i < 5的i * 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，表示可赋值，后接一个或多个变量，或\nothing 和 \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
OpenJML
-check：对JML注释的规范性检查
-esc：对程序的静态检查
-rac：对程序的动态检查
SMT Solver：检查代码与规格的等价性
JMLUnitNG：生成测试数据
对Group接口的JML语法检查结果如下：
可见，错误只有找不到Person类，其他地方是通过的（检查Person则会直接通过）
对于一个简单Demo的测试：
import java.math.BigInteger;
public class Demo {
/*@ public normal_behavior
@ requires i1 != null && i2 != null && flag == true;
@ ensures \result == i1.xor(i2);
@ also
@ public normal_behavior
@ requires i1 != null && i2 != null && flag == false;
@ ensures \result == i1.or(i2);
@ also
@ public normal_behavior
@ requires i1 == null || i2 == null;
@ ensures \result == 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 类储存所有的连通分支，并在addPerson和addRelation时进行维护
Graph 类实现了所有的关系查询方法，这样可以分担Network的任务，提高性能
在debug过程中又增加了Path类，实现了
findPath方法，基于dfs对路径进行查询Path 类只在
qsl方法中用到，作为一点小优化
HW10（一个CTLE炸强测）
queryNameRank方法，完全是照搬JML规格，多了无谓的循环，多么惨痛的教训HW11（CTLE、WA遍地开花）
borrowFrom方法，欲用 ArrayList 的set方法，手滑打成了add，竟然逃过了强测，互测被抓queryMinPath方法超时，没有堆优化queryStrongLinked方法超时，明明和标程思路一致，还是超时，推测是维护连通分支的代价太大原本是冲着超时的方向hack的，采取大量数据轰炸的策略，最后也发现了一些正确性上的错误
getAgeMean和getAgeVar的除0问题getRelationSum和getValueSum不采用缓存会CTLE（互测环境也会）getRelationSum和getValueSum采用缓存，先分组再加关系没有刷新，WAqueryMinPath和queryStrongLinked的CTLE互测中没有出现，但出现了WA不要照搬JML规格！！不要照搬JML规格！！不要照搬JML规格！！
在我看来JML是一个隐藏的杀手，它并不像表面那样友好，而是杀人于无形，且一刀致命，可能一个地方没处理好就和互测告别了
所以根据JML规格写程序的时候一定要谨慎再谨慎，尤其是调用之前实现的方法时，要判断复杂度会不会超标，第二次作业的时候我换掉了所有的contain，就落下了queryNameRank，强测就炸了
抛开课程而言，我们学习JML规格，不是目的，而是手段。
对于程序设计来说，JML语言是比自然语言更好的信息储存和传递介质，它具有效率高、无二义等优点，还可以帮助我们更好地理解顶层设计与具体实现的关系
用我的亲身体验来说明，我在阅读第一单元第二次作业的指导书时，没弄清幂函数的指数什么时候限制为\(10^4\)，什么时候限制为\(10^{10}\)，还以为\(10^{10}\)是评测机要保证的限制，于是产生了bug。而这样的情况在JML单元就绝对不会出现，只要对JML语法认识正确，双方的思维就是一致的
标签：Requires array 出现 exce www demo row work 程序设计
原文地址：https://www.cnblogs.com/atporter/p/12941467.html
