方法

Dafny在许多方面类似于典型的命令式编程语言。有方法、变量、类型、循环、if语句、数组、整数等等。任何Dafny程序的基本单元之一就是方法。方法是一段命令式的、可执行的代码。在其他语言中，它们可能被称为过程或函数，但在Dafny中，函数这个术语是为一个不同的概念保留的，我们稍后将讨论这个概念。方法的声明方式如下:

method Abs(x: int) returns (y: int)
{
   ...
}

它声明了一个名为Abs的方法，它接受一个名为x的整数参数，并返回一个名为y的整数。请注意，每个参数和返回值都需要类型，并在每个名称后面跟一个冒号(:)。同样，返回值是命名的，并且可以有多个返回值，如下所示:

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
{
   ...
}

方法主体是包含在大括号中的代码，到目前为止，它被简明地表示为 ... (这不是Dafny的语法). 主体由一系列语句组成,例如熟悉的命令式赋值, if语句, 循环，其他方法调用, return语句等等。例如, MultipleReturns方法可以声明为:

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
{
   more := x + y;
   less := x - y;
   // comments: are not strictly necessary.
   /* unless you want to keep your sanity. */
}
method MultipleReturns(x: int, y: int) returns (more: int, less: int)
{
   more := x + y;
   less := x - y;
   // comments: are not strictly necessary.
}

赋值不使用=, 而是使用:=. (事实上Dafny使用 == 表示相等, Dafny的表达式中没有使用单个的等号。) 简单语句后面必须有分号，空格和注释 (//和 /**/) 将会被忽略. 为了从方法中返回值, 该值在return语句之前的某个时间被分配给一个指定的返回值。实际上，返回值的行为非常类似于局部变量，并且可以被赋值不止一次。但是，输入参数是只读的。return语句用于在到达方法的主体块结束之前返回。return语句可以只是return关键字 (其中使用了out参数的当前值), 也可以获取要返回的值列表。也有复合语句，如if语句。if语句不需要在布尔条件周围加上括号，其作用正如人们所期望的那样:

method Abs(x: int) returns (y: int)
{
   if x < 0 {
      return -x;
   } else {
      return x;
   }
}

需要注意的是，它们总是需要在分支周围使用大括号，即使分支只包含一个语句(复合语句或其他语句)。这里的if语句使用熟悉的比较运算符语法检查x是否小于零，并返回适当的绝对值。(其他比较运算符 <=, >, >=, !=和==, 具有预期的含义。有关操作符的更多信息，请参见参考资料。)