Могут ли статические переменные существовать в Дафни?

Question

В контексте проверки мы обычно передаем значения в функции, чтобы изолировать их как «единицы» от окружающего контекста.Тем не менее, с точки зрения программирования, статические поля тоже имеют свое применение.

Поскольку Dafny компилируется в платформу .NET, разумно ожидать некоторого способа предоставления статических переменных.

Например, для реализации шаблона Singleton я ожидал бы что-то вроде:

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

Вы не можете сделать это в Дафни сегодня для объектов.Вам нужно передать одноэлементный объект в качестве параметра.

Если вам не нужен объект и вместо этого вы можете получить неизменное значение, тогда вы можете использовать const (либо static const внутри класса или признака или на уровне модуля const).

Эта проблема время от времени возникала, особенно в контексте стандартного ввода и вывода.У меня есть набросок resource дизайна для таких одноэлементных объектов (немного похожий на object в Scala или сродни once в Eiffel), но он никогда не достиг высшего приоритета.Вы можете попытаться убедить меня в обратном (или предложить и предоставить такую ​​функцию самостоятельно).

Rustan