标签：python distance exception nothing com 访问 lang 不同 表达
? 本单元在阅读并理解JML规格的基础上，完成一个简单社交网络系统的迭代开发，该系统为实时在线系统，输入给出指令，需要及时给出正确的输出。训练重点为对规格的理解，数据结构和算法的选择，程序复杂度和时间的控制。
? JML是一种类似于javadoc的，通过注释的方式对java代码规格进行规范的一种形式化语言。例如对类中的成员变量的规范描述，对类的功能的特征的规范描述，以及对类中各种方法的使用条件、正确执行结果、副作用等的一系列规范化的描述。与自然语言描述不同的是，JML具有严格的形式化描述，它引入了离散数学中的谓词等的概念以及java语法中的部分运算符等，对代码规格进行数学化的、精确的描述。
? 在我看来，JML最大的好处在于，给代码设计者、实现者和使用者提供了一份严格的逻辑化的规约。设计者需要使用JML语言给出正确的规格设计；实现者按照JML规格，在充分理解的前提下，给出符合JML规格的代码实现；使用者在使用时，给出JML规格所规定的前置条件，则可得到JML描述的正确结果。此外，JML数学化的规范描述保证了它是一种无二义性的语言，即不会产生类似自然语言中的歧义问题。
? JML的核心在于用表达式给出对数据规格、方法规格、类型规格的描述，下面简单梳理JML语法
/* @ annotation @*/ ，行注释为//@annotation \result：表示方法执行后的返回值，类型为方法声明中所定义的返回值类型，通常采用\result == xxx的形式表示返回值\old(exp)：表示表达式exp在方法执行前的值。注意对于对象引用变量，只能判断引用本身是否发生变化，而不能判断所指向的对象实体是否发生变化，因此在使用时一般将整个表达式括起来\not_assigned(x)、\not_modified(x)：判断括号中的变量在方法执行过程中是否没有被赋值、改变，一般用于后置条件约束\nonnullelements(container)：约束container中存储的对象不含nulltype(type)、typeof(exp)：返回类型type、表达式exp对应的类型(Class)\forall：类似于全程量词，表示范围内的每个元素都满足约束。使用形式为(\forall T x; P(x); R(x))，其中：x为元素，P(x)为范围的表示，R(x)为应满足的约束条件\exists：类似于存在量词，表示范围内存在某个元素满足约束，使用形式与\forall相同\sum、\product、\max、\min等：返回给定范围内表达式的和、连乘结果、最大值、最小值。使用形式为\sum T x; P(x); exp(x)，其中x为范围内变量，P(x)表示范围约束，exp(x)为求和、积、最大值、最小值的表达式\num_of：返回指定范围内满足约束的变量取值个数，使用形式同\forall，在语义上(\num_of T x; P(x); R(x))等同于(\sum T x; P(x)&&R(x); 1)<:，例如Integer.TYPE<:Object.TYPE<==>, <=!=>：表示左右两个表达式相等或不等==>, <==：语义与离散数学中的蕴涵关系相同\nothing表示空集，即没有变量；\everything表示全集，即能访问到的所有变量/*@spec_public@*/：用来注释类的私有成员变量，表示在规格中是外部可见的requires：表示前置条件，是对方法输入参数的限制。后接谓词P，方法调用者需要保证P恒真。多个requires子句为并列关系，需要全部满足。若参数不满足前置条件，则方法执行结果不可预测ensures：表示后置条件，是对方法执行结果的约束。后接谓词P，方法实现者需要保证P恒真，否则方法执行错误assignable和modifiable：表示副作用，是对方法执行过程中对对象和类属性修改的限制，前者表示可赋值，后者表示可修改，一般可交换使用，限定范围常用变量名，或\everything和\nothingpure：表示被修饰的方法为轻量级的纯访问性方法，没有副作用。此外，若在方法规格中调用其他方法，只能调用pure修饰的方法public normal_behavior ：表示接下来的部分为方法正常功能行为的规格描述public exceptional_behavior ：表示接下来的部分为方法异常行为的规格描述
signals：在异常行为规格中声明抛出的异常，使用形式为signals (Exception e) exp，即表达式exp满足时，抛出异常esignals_only：signals子句的简化版，后接异常类型，表示在满足异常行为规格的前置条件下直接抛出相应异常also：分割多种行为(正常or异常)规格的关键词。此外，重写方法在补充规格时，需要在补充的规格前使用alsoinvariant：不变式，表示类和对象在所有可见状态下都应该满足的约束条件，即方法执行前后，都要保证不变式的满足constraint：状态变化约束，表示有副作用的方法，在执行前后对类和对象属性改变的约束条件? 此外，JML有着许多应用工具链，其完整链接为：http://www.eecs.ucf.edu/~leavens/JML//download.shtml
? 下面梳理一些可用的工具链：
? 使用的命令：
java -jar .\openjml.jar -exec .\Solvers-windows\z3-4.3.2.exe -esc .\src\Person.java
? 效果如下：
? 会出现很多莫名错误与异常，而且似乎不能识别\result，经多种方法尝试后均无果，遂放弃
? 部署过程如下：
下载包并导入到项目文件，官网地址为：http://insttech.secretninjaformalmethods.org/software/jmlunitng/
在idea自带的终端输入命令：java -jar xxx\jmlunitng.jar -d ./test ./src，注意jmlunitng包地址为绝对路径
命令执行结束后，会自动生成测试代码。需要将test文件夹通过Mark Directory as -> Test Sources Root设置为测试文件夹，否则测试文件无法运行。成功后的test目录如下图
运行上图中的MyGroup_JML_Test中的main函数，结果如下（截取部分）
? 简要分析：可以看到，jmlunitng主要针对极端情况进行了一些数据的生成与测试，如参数为int型则测试0、INT_MAX、INT_MIN，参数为对象则测试null，因此覆盖度与可靠性远不如junit与黑盒测试，但是可以作为极端情况的检测
架构设计：总体上按照规格实现相应的接口。
Relation，存储与Person有关系的其他Person及对应的value，并提供get方法（代码如下）。同时在Person中用HashMap存储，id作为key值public class Relation {
private Person person;
private int value;
public Relation(Person person, int value) {
this.person = person;
this.value = value;
}
public Person getPerson() {
return person;
}
public int getValue() {
return value;
}
}
方法实现：
复杂度分析：isCircle复杂度为遍历图的复杂度O(N+M)，queryNameRank复杂度为O(N)，其余方法复杂度均为O(1)，简单计算后可得满足时间限制条件
架构设计：基本沿用HW9的架构，数据存储上同样采用HashMap<Integer, Object>的形式存储MyPerson和MyGroup对象，id作为key值
方法实现：
isCircle方法改用并查集实现，并用HashMap存储根节点，key与value分别是该节点与其祖先节点的id；在MyNetwork类中，通过路径压缩的getRootId方法与addRelation时的union操作，维护该map。
Group中的一系列查询方法，通过维护缓存变量实现（维护代码如下）。
BigInteger.ZERO（利用0 xor A = A的性质），加人时按照定义更新即可public void addPerson(Person person) {
this.ageSum += person.getAge();
this.ageSquareSum += person.getAge() * person.getAge();
this.conflictSum = this.conflictSum.xor(person.getCharacter());
for (Map.Entry<Integer, Person> entry : people.entrySet()) {
if (entry.getValue().isLinked(person)) {
this.relationSum += 2;
this.valueSum += 2 * entry.getValue().queryValue(person);
}
}
this.relationSum += 1;
this.people.put(person.getId(), person);
}
public void addRelation(int value) {
this.relationSum += 2;
this.valueSum += 2 * value;
}
其余方法沿用HW9的方式，按照规格实现即可
复杂度分析：
qci 1 1便能hack数据生成：
自动化黑盒测试平台：
time.clock()方法统计粗略的运行时间并打印filecmp.cmp()方法进行对拍；并将有差异的结果通过第三方库difflib中的方法，导出到html文件，以较直观的形式呈现出来，便于分析比对。
? 本单元体验极佳，首次全满分无bug
? 对于JML的感受是，一种极其严格的形式化描述语言，严格到可能一个功能简单的方法，需要花费甚至长于代码本身的篇幅是进行规格描述。这种严格的规格设计虽然不方便，但带来的好处也是明显的，即为设计者、实现者、使用者提供了一份类似于合同的规约，能够更好的交接工作，发现错误并及时修改以及迭代开发，从而提高代码质量。此外，严格的语法使得自动化检查等工具链的产生与开发有了可能，使得未来或许能够通过程序检测来确认代码实现是否符合规格设计。
? 在阅读规格实现代码时，理解到：规格只是设计者的思路，而实现者需要充分理解规格的内涵所在，而不能仅仅着眼于其外在形式。即，实现函数时，不能完全按照规格的描述机械化地实现，而应在充分理解规格的基础上，在保证正确性的同时，需要兼顾可扩展性、效率、性能等因素，最终给出灵活的代码实现。这才是规格的意义所在，它只是用来描述功能、架构这一层次的语言，而底层的代码实现不能被规格锁束缚。
? 当然，灵活实现的前提是仔细阅读规格并保证正确性，尤其是细节，否则可能出现HW9中漏判isCircle(id, id)这种极端数据的bug
? 对于规格的书写，目前理解并不深刻。但可以感受到，程序的大致框架也就随之确定。比如本单元三次作业的迭代开发，虽然有各种具体实现，但架构都是基于Person -> Group -> Network的框架的。因此，一个好的规格设计，能够带来好的架构设计，可以保证代码的质量。当然，在实现时也不能被这个框架完全限制，可以在其基础上进行更加灵活的架构设计，比如将算法独立出来设计为单独的类，提供方法供外部调用。如此便可提高代码的可扩展性和复用性。
标签：python distance exception nothing com 访问 lang 不同 表达
原文地址：https://www.cnblogs.com/wangyikun/p/12937876.html
