特殊关键字

ghost 关键字

通过在声明之前加上关键字 ghost 可以将方法声明为 ghost方法（仅规范而不用于执行）。

this 关键字

默认情况下，类中的方法都具有隐式接收器参数 this。可以通过在方法声明之前使用关键字 static 来删除此参数。

类 C 中的静态方法 M 可以由 C.M(...) 调用。

构造函数/构造体 constructor

在类中，一个方法可以通过将method关键字替换为constructor，申明一个构造方法。

构造函数(构造方法)只能在分配对象时调用（参见示例）

对于包含一个或多个构造函数的类，对象创建必须与对构造函数的调用一起完成。

通常，一个方法当然得有一个名字，但是一个类可以有一个没有名字的构造函数，也就是匿名构造函数 constructor (n:int )

constructor (n: int) //constructor 匿名构造器
modifies this //框架内对象的构造体 this就是this.frame？
{
  Body
}

lemma 关键字

有时，方法method关键字会被引理lemmas取代。

通过使用lemma关键字而不是method来声明方法，会让程序更清楚明白

示例：输入三个整数，返回排序后的三个整数

method Sort(a: int, b: int, c: int) returns (x: int, y: int, z: int)
ensures x <= y <= z && multiset{a, b, c} == multiset{x, y, z} //后置条件

{
  x, y, z := a, b, c;
  if z < y {
    y, z := z, y;
  }
  if y < x {
    x, y := y, x;
  }
  if z < y {
    y, z := z, y;
  }
}