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

В 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 другого класса?


formal-verification formal-semantics dafny
person ssice    schedule 22.10.2018    source источник

Ответы (3)


arrow_upward
2
arrow_downward

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

Рустан

person Rustan Leino    schedule 28.11.2018

arrow_upward
0
arrow_downward

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

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

person Julien    schedule 21.11.2018
comment
Это не решает заявленную проблему. Цель состоит в том, чтобы метод test() был вызовом клиента, реализованным и вызываемым во время выполнения. Код леммы является кодом-призраком, что означает, что он будет стерт во время выполнения, вы тут как тут; однако вызов фантомного кода из реализованных методов иногда необходим, чтобы следовать нетривиальным путям рассуждений. И кажется, Дафни не поддерживает это соглашение о вызове <ghost variable>.<ghost method>(<params>), а только this.<ghost method>(<params>) - person ssice; 22.11.2018
comment
@Julien, Дафни допускает призраков с более высокой степенью детализации, чем методы. Например, метод, не являющийся призраком, может содержать присваивания переменным-призракам и даже может иметь смесь параметров-призраков и не-призраков. - person Rustan Leino; 28.11.2018

arrow_upward
0
arrow_downward

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

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

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), не сталкиваясь с проблемой вызова метода-призрака переменной-призрака из не-призрачного метода.

person ssice    schedule 22.11.2018