函数 function

函数具有以下形式：

function F(a: A, b: B, c: C): T
  requires Pre  //前置条件pre
  reads Frame	//框架frame
  ensures Post //后置条件post
  decreases TerminationMetric //变体函数
{
  Body	//函数体
}

• a, b, c : 输入的形参，
• T : 返回结果的类型，
• Pre: 表示函数前提条件的布尔表达式，
• Frame: 函数体body需要的对象列表
• Post: 函数的后置条件布尔表达式
• TerminationMetric: 变体函数
• Body: 定义函数的表达式。

前置条件允许函数是部分的(只用前置就行不用写后置），即前置条件表示函数何时定义，并且 Dafny 会验证函数的每次使用都满足前置条件。

通常不需要后置条件，因为函数在函数体内已经给出了完整的定义。

例如：

（写个后置加个保险也行，一般后置就是声明该函数的基本属性，比如Factorial这个函数所有数字都≥1）

function Factorial(n: int): int
 requires 0 <= n //前置条件pre

 ensures 1 <= Factorial(n) //后置条件post

{
 if n == 0 then 1 else Factorial(n-1) * n //函数体body
}

要在后置条件中引用函数的结果，请使用函数本身的名称，如示例中所示。

默认情况下，函数是ghost，不能从可执行（非ghost）代码中调用。

为了使它从ghost变成非ghost，用关键字function method替换 function.

一个返回布尔值的函数可以用关键字声明，然后省略冒号和返回类型。

如果函数或方法被声明为类class成员，则它具有隐式接收器参数 this。可以通过在声明之前加上关键字 static 来删除此参数。

类 C 中的静态函数 F 可以被 C.F(...) 调用。