Мне было интересно, есть ли способ добавить проверки предварительных условий в сгенерированный код Dafny. Например, возьмем следующий фрагмент кода:
method MultipleReturns(x: int, y: int) returns (more: int, less: int)
requires 0 < y
ensures less < x < more
{
more := x + y;
less := x - y;
}
Я бы хотел, чтобы полученный код на C++ имел следующую проверку:
assert(0 < y);
Если это недоступно в Dafny, какие у меня есть варианты? Благодарю вас!
Не существует автоматического способа превратить предложение requires в проверку во время выполнения. Условие предложения requires находится в призрачном контексте, поэтому в общем случае оно может быть не компилируемым. Кроме того, если вы проверяете свою программу, то вы знаете, что условие всегда будет оцениваться как true, поэтому нет смысла также проверять его во время выполнения.
Для поддержки ситуаций, когда проверяемое условие слишком сложно проверить статически, и особенно для поддержки межъязыковых ситуаций, когда вызывающий код не написан на Dafny и, следовательно, не проверяется, Dafny имеет expect операторов. Вы можете использовать expect в своем примере, чтобы обменять статически проверенное предварительное условие на проверку во время выполнения:
method MultipleReturns(x: int, y: int) returns (more: int, less: int)
ensures less < x < more
{
RuntimeRequires(0 < y);
more := x + y;
less := x - y;
}
method RuntimeRequires(cond: bool)
ensures cond
{
expect cond, "precondition failure";
}
Обратите внимание, что без предложения requires вы не получите никакой статической проверки на сайтах вызовов.
В качестве еще одного варианта вы можете использовать как предложение requires, так и метод RuntimeRequires, который я показал. Если вы это сделаете, я бы посоветовал вам изменить спецификацию RuntimeRequires с ensures на requires, чтобы убедиться, что вы правильно скопировали условие.
method MultipleReturns(x: int, y: int) returns (more: int, less: int)
requires 0 < y
ensures less < x < more
{
RuntimeRequires(0 < y); // try changing this to 10 < y and see what happens
more := x + y;
less := x - y;
}
method RuntimeRequires(cond: bool)
requires cond
{
expect cond, "precondition failure";
}
