标签：exists 有一个 组成 hash 计算 ons == 这一 接口
JML给我上了一课
最开始接触接口的时候，我的直观感受就是“这好像没啥用啊”，它只定义了一些行为的参数和返回值，但是对于实现这些行为帮助不大。转念一想，哦，可以把一些关键的内容写在注释里。这样的注释当然可以用自然语言来写，但是JML提供了另一种思路——用形式化的语言来写注释。虽然这样的方法对于写的人和读的人可能不如自然语言友好，但是它可以避免歧义。避免歧义也很符合计算机的口味，为计算机进行自动化验证甚至自动化生成代码创造了条件。
关于JML的具体内容，请看一个例子：
JML的例子
这个例子中的方法是把一个编号为id1的person加入到编号为id2的group中。从这个例子可以看出，一个方法的JML由0或更多个normal_behavior和0或更多个exceptional_behavior组成，之间用also连接。每个normal_behavior由requires(满足什么条件才执行这个behavior), assignable(这个behavior可能会修改什么对象), ensures(这个behavior执行后能保证什么结果)构成；而每个exceptional_behavior由requires, assignable, signals(满足特定条件需要抛出特定异常)构成。
requires, ensures, signals都会跟随一个布尔表达式，其中涉及到一些JML的规则。
布尔表达式中的变量，在接口的最开始定义，例如上例中的people和groups：
JML变量定义
布尔表达式中，可以使用一类特殊的方法——pure方法。pure方法是指纯粹访问性的方法，它不需要前置条件，也不会对对象进行改变，执行一定会正常结束，例如上例中的getPerson：
JML pure方法
布尔表达式中还有一些特殊的表达式，例如\result, \exists, \forall等等，不难理解，在此不赘述了。有一个相对特殊的是\old，表示方法调用前的情况。
除了上例中针对方法的方法规格，还有针对类的类规格，主要包括invariant和constraints两种。
invariant是一个数据在可见状态下应该满足的要求。可见状态在此不详述了，大致就是说，在会修改状态的方法执行期间是不可见的，允许暂时违背invariant。
constraints描述一个数据如果要变化，怎么变。
invariant和constraints例如：
private /*@spec_public@*/ long counter;
//@ invariant counter >= 0;
//@ constraint counter == \old(counter)+1;
这一单元由于JML给的比较详细，加上有运行时间的限制，所以可以自由发挥的地方不是很多。
标签：exists 有一个 组成 hash 计算 ons == 这一 接口
原文地址：https://www.cnblogs.com/xhy18373542/p/12941381.html
