声明 Statement

以下是 Dafny 中最常见语句:

var LocalVariables := ExprList;
 Lvalues := ExprList;
 assert BoolExpr;
 print ExprList;
 if BoolExpr0 {
  Stmts0
 } else if BoolExpr1 {
  Stmts1
 } else {
  Stmts2
 }

 while BoolExpr

  invariant Inv

  modifies Frame

  decreases Rank

 {
  Stmts
 }

match Expr {
  case Empty => Stmts0
  case Node(l, d, r) => Stmts1
}

 break;
 return;

函数/方法的返回值赋值给变量

(就是将函数/方法返回的值或对象 赋给 一个 局部变量 而已）

var LocalVariables := ExprList;

var 语句引入了局部变量。

Lvalues := ExprList; 赋值语句将 ExprList变量赋给Lvalues。 这些分配是并行执行的（更重要的是，所有必要的读取都发生在写入之前），因此左侧必须表示不同的 L 值。 每个右侧都可以是以下形式之一的表达式或对象创建：

1. new T

2. new T.Init(ExprList)

3. new T(ExprList)

4. new T[SizeExpr]

5. new T[SizeExpr0, SizeExpr1]

第一种形式分配一个类型为 T 的对象。

第二种形式另外在新分配的对象上调用初始化方法或构造函数。

第三种形式是当调用匿名构造函数时的语法。

其他形式分别了T是一维和二维数组对象的匿名构造方法

assert 声明

assert 语句判断后面的表达式结果是否为真（由验证器验证）。

print 打印语句

打印语句将给定打印表达式的值输出到标准输出。字符串中的字符可以转义；例如，对 print 语句感兴趣的是 \n 表示字符串中的换行符。

if 选择语句

if 语句是通常的语句。该示例显示了使用 else if 将备选方案串在一起。像往常一样，else 分支是可选的。

while 循环语句

• while 语句是通常的循环，其中
• invariant 声明给出了一个循环变量
• modifies 语句限制了循环的框架
• reduction 语句从循环中引入了一个变体函数。

默认情况下，循环不变式为真，修改框与封闭上下文中的相同（通常是封闭方法的修改子句），并从循环保护中猜测变体函数。

while BoolExpr //布尔表达式-循环条件 invariant Inv modifies Frame decreases Rank { Statements }

match语句

match 语句计算源Expr（一个类型为归纳数据类型的表达式），然后执行与用于创建源数据类型值的构造函数相对应的 case，将构造函数参数绑定到给定的名称。如果不需要它们来标记 match 语句的结尾，则可以省略包围 case 的花括号。

break语句

break 语句可用于退出循环，而 return 语句可用于退出方法。