Dafny 中可以存在静态变量吗？

Question

在验证上下文中，我们通常将值传递给函数，以便将它们作为 "units" 与周围的上下文隔离开来。但是，从编程的角度来看，静态字段也有其用途。

由于 Dafny 编译到 .NET 平台，因此期望以某种方式公开静态变量是合理的。

例如，为了实现单例模式，我希望是这样的：

class A { constructor () {}
  static var instance: A? := null;
  static method getInstance() returns (r: A)
    ensures A.instance() != null
  {
    if A.instance == null { var i := new A(); A.instance := i; }
    r := A.instance;
  }
}

但是，这会导致错误 Fields cannot be declared 'static'.

有什么方法可以表达这一点（不使用未解释的函数，因为这可能仅用于验证目的但不会生成有用的代码）。

Answer 1

今天在 Dafny 中，您不能对对象执行此操作。您需要将单例对象作为参数传递。

如果您不需要对象，而是可以使用不可变值，那么您可以使用 const（class 或 trait 中的 static const , 或模块级 const).

这个问题时常出现，尤其是在标准输入和输出的上下文中。我有一个针对此类单例对象的 resource 设计草图（有点像 Scala 中的 object 或类似于 Eiffel 中的 once），但它从未达到最高优先级。欢迎您以其他方式说服我（或者您自己提出并提供这样的功能）。

鲁斯坦

Dafny 中可以存在静态变量吗？

Can static variables exist in Dafny?

dafny