时间戳

首页 > 解决方案 > Dafny 中可以存在静态变量吗？

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

问题描述

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

由于 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'.

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

标签： dafny

解决方案

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

如果您不需要对象而是可以使用不可变值来解决问题，那么您可以使用 a const（static const类或特征内部的 a ，或模块级别的const）。

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

鲁斯坦

推荐阅读