模块

介绍

将程序分解成多个部分来构造它是创建大型程序的重要部分。在Dafny中，这是通过模块实现的。模块提供了一种将相关类型、类、方法、函数和其他模块组合在一起的方法，以及控制声明的作用域。模块可以相互导入以实现代码重用，并且可以对模块进行抽象以将实现与接口分离。

声明新模块

Declaring New Modules声明新模块 一个新模块是用module关键字声明的，后面跟着新模块的名字，还有一对括住模块主体的花括号({}):

module Mod {
  ...
}

模块主体可以包含任何可以放在顶层的内容。这包括类、数据类型、类型、方法、函数等。

module Mod {
  class C {
    var f: int;
    method m()
  }
  datatype Option = A(int) | B(int)
  type T
  method m()
  function f(): int
}

你也可以将一个模块嵌套到另一个模块中:

module Mod {
  module Helpers {
    class C {
      method doIt()
      var f: int;
    }
  }
}

然后，你可以在Mod模块中引用Helpers模块的成员，方法是在它们前面加上" Helpers "。例如:

module Mod {
  module Helpers {
    class C {
      method doIt()
      var f: int;
    }
  }
  method m() {
    var x := new Helpers.C;
    x.doIt();
    x.f := 4;
  }
}

module Mod {
  module Helpers { ... }
  method m() {
    var x := new Helpers.C;
    x.doIt();
    x.f := 4;
  }
}

在模块级别定义的方法和函数可以像类一样使用，只是模块名作为前缀。它们也可以在同一个模块中的类的方法和函数中使用。

module Mod {
  module Helpers {
    function method addOne(n: nat): nat {
      n + 1
    }
  }
  method m() {
    var x := 5;
    x := Helpers.addOne(x); // x is now 6
  }
}

默认情况下，函数(和谓词)的定义在定义它们的模块外部公开。这可以通过导出集进行更精确的控制，我们将在下一节中看到。所以增加

module Mod {
  module Helpers {
    function method addOne(n: nat): nat {
      n + 1
    }
  }
  method m() {
    var x := 5;
    x := Helpers.addOne(x);
    assert x == 6; // this will succeed
  }
}

  assert x == 6;

以m()结尾将进行验证。

导入和导出模块

声明新的子模块是有用的，但有时您希望引用来自现有模块的内容，比如库。在这种情况下，您可以将一个模块导入另一个模块。这是通过import关键字完成的，有几种不同的形式，每一种都有不同的含义。最简单的形式是具体的导入,导入形式A = B这个模块声明创建一个引用B(必须已经存在),并结合新名称注意这个新名称,例如 A,,只有绑定模块包含导入声明;它不会创建全局别名。例如，如果helper是在Mod之外定义的，那么我们可以导入它:

module Helpers {
  function method addOne(n: nat): nat
  {
    n + 1
  }
}
module Mod {
  import A = Helpers
  method m() {
    assert A.addOne(5) == 6;
  }
}

module Helpers {
  ...
}
module Mod {
  import A = Helpers
  method m() {
    assert A.addOne(5) == 6;
  }
}

注意，在m()中，我们必须使用A而不是helper，因为我们将它绑定到一个不同的名称。名称Helpers在m()中不可用，因为只有在Mod中绑定的名称才可用。为了使用来自另一个模块的成员，它要么必须用module声明，要么用import导入。

不过，如果我们不想给Helpers起个新名字，也不必。如果需要，可以编写import Helpers = Helpers, Dafny甚至为这种行为提供了简便的import Helpers。您不能同时绑定两个具有相同名称的模块，因此有时必须使用= 版本号以确保名称不会冲突。

导出集合

默认情况下，导入import将允许访问被导入模块的所有声明(及其定义)。为了更精确地控制这一点，我们可以使用导出export集。每个导出export集可能有当前模块的声明列表，以provides或reveals的形式给出。没有名称的导出export被认为是该模块的默认导出，并且在没有显式命名集合时使用。

module Helpers {
  export Spec provides addOne, addOne_result
  export Body reveals addOne
  export extends Spec
  function method addOne(n: nat): nat
  {
    n + 1
  }
  lemma addOne_result(n : nat)
     ensures addOne(n) == n + 1
  { }
}

在这个例子中，我们声明了3个导出集，Spec 集授予了对addOne函数的访问权，但是由于它是用provides声明的，所以它没有授予对其定义的访问权。Body导出集将addOne声明为reveals，现在可以访问addOne的bdoy部分。最后，默认导出作为Spec的扩展extends给出，这表明它只是给出Spec所声明的所有导出。

我们现在可以在导入helper时选择这些导出集中的任何一个，并获得它的不同视图。

module Helpers {
  export Spec provides addOne, addOne_result
  export Body reveals addOne
  export extends Spec
  function method addOne(n: nat): nat
  {
    n + 1
  }
  lemma addOne_result(n: nat)
     ensures addOne(n) == n + 1
  { }
}

module Mod1 {
  import A = Helpers`Body
  method m() {
    assert A.addOne(5) == 6; // succeeds, we have access to addOne's body
  }
  method m2() {
    //A.addOne_result(5); // error, addOne_result is not exported from Body
    assert A.addOne(5) == 6;
  }
}
module Mod2 {
  import A = Helpers`Spec
  method m() {
    assert A.addOne(5) == 6; // fails, we don't have addOne's body
  }
  method m2() {
    A.addOne_result(5);
    assert A.addOne(5) == 6; // succeeds due to result from addOne_result
  }
}
module Mod3 {
  import A = Helpers
  method m() {
    assert A.addOne(5) == 6; // fails, we don't have addOne's body
  }
}

我们还可以使用导出集export sets 来控制可用的类型定义。所有类型声明(如newtype、type、datatype等)都可以导出为提供provides或显示。在前一种情况下，导入该类型的模块将其视为不透明类型。

module Helpers {
  export provides f, T
  export Body reveals f, T
  type T = int
  function f(): T { 0 }
}
module Mod {
  import A = Helpers
  function g(): A.T { 0 } // error, T is not known to be int, or even numeric
  function h(): A.T { A.f() } // okay
}

一旦导入export了显示reveals以前不透明类型的导出，则已知对它的所有现有使用都是内部类型。

module Helpers {
  export provides f, T
  export Body reveals f, T
  type T = int
  function f(): T { 0 }
}
module Mod {
  import A = Helpers
  function h(): A.T { A.f() }
}

module Mod2 {
  import M = Mod
  import A = Helpers`Body
  function j(): int
    ensures j() == 0 //succeeds
  { M.h() }
}

作为一种方便的简写方式，特殊标识符“*”可以在提供provides或揭示reveals之后给出，以表示所有声明都应该提供或揭示。

module A {
   export All reveals * // reveals T, f, g
   export Spec provides * // provides T, f, g
   export Some provides * reveals g // provides T, f reveals g
   type T = int
   function f(): T { 0 }
   function g(): int { 2 }
}

我们还可以一次提供多个导出来创建一个聚合导入(aggregate import).

module A {
  export Justf reveals f
  export JustT reveals T
  type T = int
  function f(): int { 0 }
}
module B {
  import A`{Justf,JustT}
  function g(): A.T { A.f() }
}

导出一致性

导出集(export set)必须始终呈现模块的一致视图:任何出现在导出声明中的内容都必须被导出。回顾前面的示例，我们不能创建一个既显示f(reveals f)又显示T的导出集export set。原因很简单，我们将创建一个类型约束0:T，如果T是不透明的，则无法解决这个约束。类似地，如果不提供T，则不能创建提供provides或揭示f reveals f的导出集。

module Helpers {
  export provides f, T // good
  export Body reveals f, T // good
  export BadSpec reveals f, provides T // bad
  export BadSpec2 provides f // bad
  type T = int
  function f(): T { 0 }
}

由于我们可以定义同时包含导入import和导出export声明的模块，因此我们可能需要从外部模块导出声明，以创建一致的导出集export set。外部模块的声明不能直接包含在导出export中，但是提供它们的导入import可以。

module Helpers {
  export provides f, T
  type T = int
  function f(): T { 0 }
}
module Mod {
  export Try1 reveals h // error
  export Try2 reveals h, provides A.f, A.T // error, can't provide these directly
  export reveals h, provides A // good
  import A = Helpers
  function h(): A.T { A.f() }
}

当导入Mod时，我们现在也获得了对其导入a import a中所提供的内容的合格访问权。我们也可以选择直接导入这些内容，给它们一个更短的名称。

module Helpers {
  export provides f, T
  type T = int
  function f(): T { 0 }
}
module Mod {
  export reveals h, provides A
  import A = Helpers
  function h(): A.T { A.f() }
}

module Mod2 {
  import M = Mod
  import MA = M.A
  function j(): M.A.T { M.h() }
  function k(): MA.T { j() }
}

开放模板

有时，为导入的模块的成员加上名称前缀是乏味且难看的，即使您在导入时选择了一个简短的名称。在这种情况下，您可以将模块导入为“opened”，这将使其所有成员都可用，而无需添加模块名称。opened关键字必须紧跟在import之后，如果它存在的话。例如，我们可以将前面的addOne示例写为:

module Helpers {
  function method addOne(n: nat): nat
  {
    n + 1
  }
}

module Mod {
  import opened Helpers
  method m() {
    assert addOne(5) == 6;
  }
}

当打开模块时，新绑定的成员将具有较低的优先级，因此它们将被局部定义隐藏。这意味着，如果您定义了一个名为addOne的局部函数，则helper中的函数将不再以该名称提供。当模块被打开时，原始的名称绑定仍然存在，所以您总是可以使用绑定的名称来获取任何隐藏的内容。

module Helpers {
  function method addOne(n: nat): nat
  {
    n + 1
  }
}
module Mod {
  import opened Helpers
  function addOne(n: nat): nat {
    n + 2
  }
  method m() {
    assert addOne(5) == 6; // this is now false,
                           // as this is the function just defined
    assert Helpers.addOne(5) == 6; // this is still true
  }
}

module Mod {
  import opened Helpers
  function addOne(n: nat): nat {
    n + 2
  }
  method m() {
    assert addOne(5) == 6; // this is now false,
                           // as this is the function just defined
    assert Helpers.addOne(5) == 6; // this is still true
  }
}

如果打开两个都声明具有相同名称的成员的模块，那么在没有模块前缀的情况下，这两个成员都不能被引用，因为哪个成员的含义是不明确的。不过，只要您不试图使用具有共同名称的成员，仅仅打开这两个模块就不会出现错误。opened关键字可以用于任何类型的导入import声明，包括模块抽象形式。

抽象模块

有时，使用特定的实现是不必要的;相反，所需要的只是一个实现某些接口的模块。在这种情况下，您可以使用抽象模块导入。在Dafny,这是写import A : B.。这意味着绑定名称A,而是得到确切的模块B,你得到任何模块的细化B .通常情况下,模块B可能抽象类型定义,包含脱胎方法的类,或者直接不适合使用。由于细化的定义方式，B的任何细化都可以安全地使用。例如，如果我们以:

abstract module Interface {
  function method addSome(n: nat): nat
    ensures addSome(n) > n
}
abstract module Mod {
  import A : Interface
  method m() {
    assert 6 <= A.addSome(5);
  }
}

如果我们知道addSome实际上正好加了1，我们就可以更精确了。下面的模块具有这种行为。此外，后置条件更强，因此这实际上是对Interface模块的改进。

module Implementation refines Interface {
  function method addSome(n: nat): nat
    ensures addSome(n) == n + 1
  {
    n + 1
  }
}

然后，我们可以在一个新的模块中用Implementation代替A，通过声明Mod的精炼，它定义了A的Implementation。

abstract module Interface {
  function method addSome(n: nat): nat
    ensures addSome(n) > n
}
abstract module Mod {
  import A : Interface
  method m() {
    assert 6 <= A.addSome(5);
  }
}
module Implementation refines Interface {
  function method addSome(n: nat): nat
    ensures addSome(n) == n + 1
  {
    n + 1
  }
}
module Mod2 refines Mod {
  import A = Implementation
  method m() {
    ...;
    // this is now provable, because we know A is Implementation
    assert 6 == A.addSome(5);
  }
}

当你将一个抽象导入细化到一个具体的导入时，具体模块必须是抽象模块的显式细化(例如，用refines声明)。

模块排序和依赖关系

Dafny并不特别关注模块出现的顺序，但它们必须遵循一些规则才能形成良好的结构。作为一个经验法则，应该有一种方法来对程序中的模块进行排序，以便每个模块只引用源文本中在它之前定义的东西。这并不意味着模块必须按这个顺序排列。如果你没有做任何循环引用，Dafny会帮你弄清楚顺序的。例如，这显然毫无意义:

import A = B
import B = A

你可以在顶层有import语句，也可以导入在同一层定义的模块:

import A = B
method m() {
  A.whatever();
}
module B {
  method whatever() {}
}

import A = B
method m() {
  A.whatever();
}
module B { ... }

在本例中，所有内容都定义得很好，因为我们可以先放B，然后是A导入，最后是m()。如果没有顺序，那么Dafny将给出一个错误，抱怨循环依赖关系。 请注意，当重新排列模块和导入时，它们必须保持在相同的包含模块中，这就不允许一些病态的模块结构。此外，导入和子模块总是被认为是最前面的，即使在顶层也是如此。这意味着以下内容不是很好的格式:

method doIt() { }
module M {
  method m() {
    doIt();
  }
}

因为模块M必须出现在任何其他类型的成员之前，比如方法。要像这样定义全局函数，您可以将它们放在一个模块(比如称为Globals)中，并将其打开到任何需要其功能的模块中。最后，如果您通过路径导入，例如import a = B.C那么这将创建a对B的依赖关系，因为我们需要知道B是什么(它是抽象的还是具体的，还是细化的?)

名字分解

(待办事项:以下内容已在Dafny更改。这里的描述应该改变以反映新的规则。)

当Dafny看到像A.B.C这样的东西时，它怎么知道每个部分指的是什么?Dafny用来确定这样的标识符序列所引用的是名称解析。虽然规则可能看起来很复杂，但它们通常都符合您的预期。Dafny首先查找初始标识符。根据第一个标识符引用的内容，将在适当的上下文中查找标识符的其余部分。具体规则如下: 局部变量、参数和绑定变量。这些是x y和i在var x;，... returns (y: int)，forall i :: ... 数据类型和模块名(如果这不是标识符的唯一部分)。类允许以这种方式访问它们的静态成员，数据类型允许访问它们的构造函数。模块允许像这样引用它们的任何成员 构造函数名称(如果没有歧义)。任何不需要限定的数据类型(因此数据类型名称本身不需要前缀)，以及具有唯一命名构造函数的数据类型，都可以通过其名称引用。所以如果datatype List = Cons(List) | Nil是唯一声明 Cons和Nil构造函数的数据类型，那么你可以写Cons(Cons(Nil))。如果构造函数名不是唯一的，则需要在其前面加上数据类型的名称(例如List.Cons(List.Nil))。这是每个构造函数完成的，而不是每个数据类型。 当前类的字段、函数和方法(如果在静态上下文中，则只允许静态方法和函数)。您可以这样引用当前类的字段this.f或者f，当然假设f没有被上面的任何一个隐藏。如果需要，您总是可以加上前缀this，但不能隐藏它。(注意，名称是数字字符串的字段必须总是有一些前缀。) 封闭模块中的静态函数和方法。注意，这只引用在模块级声明的函数和方法，而不是命名类的静态成员。 打开的模块在每一层处理，在当前模块的声明之后。打开的模块只影响步骤2、3和5。如果发现有歧义的名称，将生成一个错误，而不是继续沿着列表向下。在第一个标识符之后，规则基本上是相同的，除了在新的上下文中。例如，如果第一个标识符是一个模块，那么下一个标识符将查看该模块。打开的模块只适用于它被打开的模块。在查找另一个模块时，只考虑在该模块中显式声明的内容。