Дафни: леммы без тел

Я использовал абстрактные леммы и функции (без тел) в задаче моделирования. В этом примере

lemma py(c : int) returns (a: int, b :int)
    ensures a*a + b*b == c*c

lemma main(c : int) returns (a: int, b :int)
    ensures a*a + b*b == c*c
{
    a, b := py(c);
}

вызов py в main гарантирует, что пост-условие истинно независимо от того, как реализован py. У меня есть 2 вопроса:

  1. Безопасно ли использовать абстрактные леммы/функции в Dafny? Следующая модификация приведенного выше кода проверена Dafny:

    lemma py(c : int) returns (a: int, b :int)  
    ensures a*a + b*b == c*c  
    ensures a*a + b*b != c*c

    в то время как я думаю, что, возможно, Дафни должен был выдать ошибку.

  2. Должен ли я сказать lemma {:axiom} py(...)? Я не заметил разницы при включении {:axiom} или {:imported}.


dafny
person Abhishek    schedule 29.10.2017    source источник

Ответы (2)


arrow_upward
0
arrow_downward

Методы и функции без тел действительно полезны при моделировании частей системы, которые вы не реализуете.

Однако нужно быть осторожным, давая таким методам и функциям постусловия, потому что они становятся доверенными и не проверяются Дафни. Другими словами, потенциально небезопасно использовать леммы или функции без тел, если они имеют постусловия.

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

Если вы передадите Dafny флаг /noCheating:1, он будет жаловаться на любые методы или функции без тел, которые имеют постусловия, и заставит вас использовать атрибут {:axiom}. Это может быть полезно, даже если не передается /noCheating:1, просто чтобы отметить тот факт, что постусловию доверяют. Вам решать, передавать ли /noCheating:1 или использовать атрибут в любом случае.

person James Wilcox    schedule 29.10.2017

arrow_upward
1
arrow_downward

Как упоминает Джеймс, лемма без тела может быть полезна при моделировании поведения, которое вы не реализуете. Если вы не укажете тело, верификатор не будет пытаться проверить правильность леммы. Поэтому по сути это аксиома.

Даже без флага /noCheating, о котором упоминает Джеймс, компилятор Dafny будет жаловаться на леммы без тела (а также на методы и функции). Обратите внимание, что компилятор не запускается до тех пор, пока верификатор не будет удовлетворен. Атрибут {:axiom} говорит о том, что вы готовы взять на себя ответственность за истинность леммы. Для нефантомного метода без тела вы также можете использовать атрибут {:extern}, который позволяет вам связываться с кодом, написанным на других языках. Опять же, вы берете на себя ответственность за правильность этого внешнего кода, поскольку верификатор Dafny не будет его проверять.

Рустан

person Rustan Leino    schedule 31.10.2017