JML概述
理论基础
维基百科对JML的叙述如下
JML is a behavioral interface specification language for Java modules. JML provides semantics to formally describe the behavior of a Java module, preventing ambiguity with regard to the module designers' intentions. JML inherits ideas from Eiffel, Larch and the Refinement Calculus, with the goal of providing rigorous formal semantics while still being accessible to any Java programmer. Various tools are available that make use of JML's behavioral specifications. Because specifications can be written as annotations in Java program files, or stored in separate specification files, Java modules with JML specifications can be compiled unchanged with any Java compiler.
JML是一种描述Java模块行为接口规范的语言，提供特殊的语义符号严格地描述Java模块的行为以避免（自然语言描述所产生的）歧义。JML来源于Eiffel，Larch和Refinement Calculus的思想，其核心思想是提供一种严谨而可读的语义规范。目前有许多工具都能利用JML进行形式化验证。由于这种规格语言可以用Java程序中的注释实现，或单独存储为规范文件，任何Java编译器都能编译带有JML的Java程序。
JML语法（关键字）
JML通常包含以下关键字
requires
ensures
signals
signals_only
assignalbe
pure
invariant
loop_invariant
also
assert
spec_public
esult
old(<expression>)
(forall <decl>; <range-exp>; <body-exp>)
(exists <decl>; <range-exp>; <body-exp>)
a ==>b
a <==b
a <==> b
// demo/Demo.java
package demo;
public class Demo {
/*@ public normal_behaviour
@ ensures
esult == num1 + num2;
*/
public static int Add(int num1, int num2) {
return num1 + num2;
}
public static void main(String[] args) {
int a = Add(100, 200);
}
}
运行结果
理论基础
维基百科对JML的叙述如下
JML is a behavioral interface specification language for Java modules. JML provides semantics to formally describe the behavior of a Java module, preventing ambiguity with regard to the module designers' intentions. JML inherits ideas from Eiffel, Larch and the Refinement Calculus, with the goal of providing rigorous formal semantics while still being accessible to any Java programmer. Various tools are available that make use of JML's behavioral specifications. Because specifications can be written as annotations in Java program files, or stored in separate specification files, Java modules with JML specifications can be compiled unchanged with any Java compiler.
JML是一种描述Java模块行为接口规范的语言，提供特殊的语义符号严格地描述Java模块的行为以避免（自然语言描述所产生的）歧义。JML来源于Eiffel，Larch和Refinement Calculus的思想，其核心思想是提供一种严谨而可读的语义规范。目前有许多工具都能利用JML进行形式化验证。由于这种规格语言可以用Java程序中的注释实现，或单独存储为规范文件，任何Java编译器都能编译带有JML的Java程序。
JML语法（关键字）
JML通常包含以下关键字
requires
ensures
signals
JML概述
理论基础
维基百科对JML的叙述如下
JML is a behavioral interface specification language for Java modules. JML provides semantics to formally describe the behavior of a Java module, preventing ambiguity with regard to the module designers' intentions. JML inherits ideas from Eiffel, Larch and the Refinement Calculus, with the goal of providing rigorous formal semantics while still being accessible to any Java programmer. Various tools are available that make use of JML's behavioral specifications. Because specifications can be written as annotations in Java program files, or stored in separate specification files, Java modules with JML specifications can be compiled unchanged with any Java compiler.
JML是一种描述Java模块行为接口规范的语言，提供特殊的语义符号严格地描述Java模块的行为以避免（自然语言描述所产生的）歧义。JML来源于Eiffel，Larch和Refinement Calculus的思想，其核心思想是提供一种严谨而可读的语义规范。目前有许多工具都能利用JML进行形式化验证。由于这种规格语言可以用Java程序中的注释实现，或单独存储为规范文件，任何Java编译器都能编译带有JML的Java程序。
JML语法（关键字）
JML通常包含以下关键字
requires
ensures
signals
signals_only
assignalbe
pure
invariant
loop_invariant
also
assert
spec_public
esult
old(<expression>)
(forall <decl>; <range-exp>; <body-exp>)
(exists <decl>; <range-exp>; <body-exp>)
a ==>b
a <==b
a <==> b
pure
invariant
loop_invariant
also
assert
spec_public
esult
old(<expression>)
(forall <decl>; <range-exp>; <body-exp>)
(exists <decl>; <range-exp>; <body-exp>)
a ==>b
a <==b
a <==> b
第一次作业
架构设计
JML概述
类图
根据需求确定容器类型
MyPath类
MyPath类中要实现下标索引节点方法及集合包含性判断和集合计数方法。因此我使用ArrayList和HashMap两种容器类型。前者完成数组式管理，后者完成集合式管理。能最快速地完成两类方法。
MyPathContainer类
MyPathContainer类中要实现编号、路径的添加、移除，包含性判断，双向索引以及不同节点数的统计。使用编号到路径、路径到编号两个HashMap实现双向索引及包含性判断，使用节点计数HashMap统计各节点在路径中的出现次数。添加和删除路径时修改节点计数，当节点数量为零时将其从容器中移除。
本次作业未出现bug
第二次作业
架构设计
类图
类增设考量
由于MyGraph中要实现一些图论相关方法且图的构造是根据加入的路径生成，因此增设无向图类及边类。将无向图抽象为节点和边的集合。由于是无向图，边类的equals方法需重写，即构成边的两节点所构成的集合相等则两条边相等。
根据需求确定容器类型
在MyGraph中由于要实现边的包含性判断，使用HashMap来存储边。但实际上，对于节点和边的统计以及相关请求应交由无向图类处理，从而将MyGraph类视为单纯的路径容器。MyGraph中对这两种图元素的存储是冗余的。
在无向图类中，由于我选择了Floyd算法计算最短路径，因此选用邻接矩阵的方式存储图。临界矩阵以二位Integer数组实现，这样可以将不存在的边置为null从而避免极端情况下错误的发生。
优化Trick
由于测试规定了轻修改重查询的特性，我将由Floyd生成的最短距离矩阵视为图的一个属性，随图的更新而更新。也即是说，只有当加入/删除了节点或边时才需要重新计算距离矩阵。通过一些判断可以减少无谓计算。
bug分析
本次作业出现了两个较为严重的bug，一是没有清除无向图中的自环..
thanks for reading, but as you can see, this is an unfinished work...promise that you can see the full version tomorrow....