方法 methods

方法的声明如下：

method M(a: A, b: B, c: C) r eturns (x: X, y: Y, z: Y)  //输入输出参数
	requires Pre	//前置条件  
	modifies Frame  //框架
	ensures Post	//后置条件
  decreases TerminationMetric //变体函数
{
 	method M(a: A, b: B, c: C) r eturns (x: X, y: Y, z: Y)  //输入输出参数
 	 requires Pre	//前置条件	
 	 modifies Frame  //框架	
 	 ensures Post	//后置条件
 	 decreases TerminationMetric //变体函数

}

其中：

• a, b, c : 输入参数
• x, y, z : 输出参数
• Pre: 表示方法 前提条件 的 布尔表达式
• Frame: 表示类对象的集合，可以被方法更新
• Post: 是方法 后置条件 的 布尔表达式
• TerminationMetric: 是方法的变体函数

框架Frame

框架Frame 是单个或多个对象组成的表达式的集合。(见下面例子)

框架Frame是由类内对象和类外方法内对象两部分组成。(反正就是一堆类对象的集合）

例如，如果 c 和 d 是类C的对象，那么以下每行意思是一样的。

• modifies {c, d}

• modifies {c} + {d}

• modifies c, {d}

• modifies c, d

如果方法内啥都没写，那么前置和后置条件默认为真，框架默认为空集。

变体函数 variant function

变体函数是一个表达式组成的列表，表示由给定表达式组成的字典元组，后跟隐含的top元素。

如果省略没写的话，Dafny 将猜测该方法的变体函数，通常是以该方法的参数列表开头的字典元组。

Dafny IDE 将在工具提示中显示猜测。