Почему я не могу вызвать (нестатическую) лемму из призрачного поля в Дафни?

Question

В Dafny, lemma реализовано как ghost method, поэтому оно полезно только для спецификации.

Однако вы не можете вызвать лемму из ghost field, например:

class A {
    var i: int;
    lemma sum_is_commutative(i: int, j: int)
        ensures i + j == j + i
    {}
}
class B {
    ghost var a: A;
    lemma a_sum_is_commutative(i: int, j: int)
        ensures i + j == j + i
    { a.sum_is_commutative(i, j); }
    method test() {
        // a.sum_is_commutative(3, 2); // <- Cannot use directly this
        a_sum_is_commutative(3, 2);
    }
}

В чем причина такого поведения?Как это можно обойти?Является ли лучший выбор, чтобы просто повторить лемму во внутреннем классе и использовать (обычно вызывать) lemma?

другого класса

Answer 1

Я не могу прокомментировать обоснование такого поведения (и я обновлю выбранный ответ, если он академический, а не просто ошибка или отсутствие реализации).

Для обхода этой проблемыСемантически то же самое, чтобы определить

class A {
  lemma sum_commutative(i: int, j: int) {}
}

как что-то вроде

class A {
  static lemma sum_commutative(a: A, i: int, j: int) {}
}

Так что, даже если вам нужен доступ к экземпляру this, вы можете передать его какпараметр вместо того, чтобы полагаться на него неявным образом.

Затем вы можете вызывать из любого другого класса свою лемму как A.sum_commutative(a, i, j), не сталкиваясь с проблемой вызова метода-призрака для переменной-призрака из не-призрачный метод.

Answer 2

Спасибо за обнаружение и сообщение об этом.Это ошибка.Я только что исправил это.

Растан

Answer 3

Я не знаком с Дафни, но я думаю, что вам также нужно объявить свой метод test как ghost, чтобы иметь возможность использовать в нем параметр ghost.

Обычно в средах проверки программ, ghost означает, что определение будет стерто во время выполнения и приведено здесь только для целей проверки.Таким образом, ваш метод test не должен содержать код, определение которого будет стерто, или он должен быть помечен как стираемый (ghost).