Для следующего кода я получаю, что он не может установить существование значений LHS, удовлетворяющих предикату такой-то. Как мне доказать, что правая часть верна и такой x существует?
method Main() {
var n : int := 10;
var x : seq<int> :| n == |x| && forall i :: 0 <= i < |x| ==> -1 <= x[i] <= 1;
}
Вам нужно предоставить свидетеля. Следующее утверждение делает свое дело:
method Main() {
var n : int := 10;
assert |[0, 0, 0, 0, 0, 0, 0, 0, 0, 0]| == 10;
var x : seq<int> :| n == |x| && forall i :: 0 <= i < |x| ==> -1 <= x[i] <= 1;
}
Однако это подводит вас к следующему пункту, который заключается в том, что
Я собирался прокомментировать это выше как «следующий пункт», но, видимо, мое предложение как-то обрезалось. В этом сообщении об ошибке говорится, что верификатор теперь смог доказать существование значения для x
, но компилятор все еще не может понять, как сгенерировать для него код.
Кажется, что даже что-то тривиальное вроде этого на данный момент не поддерживается:
method Main() {
var n : int := 10;
var y : seq<int> :| y == [3];
var x : seq<int> :| x == y;
var z : seq<int> :| |z| == |y|;
}
Дафни удается создать экземпляр x
, но не z
.
Может, выложу в свой GitHub/Проблемы?
Верификатор доказывает существование таких y
, x
и z
, но компилятор не может обработать последний случай. В общем, следует ожидать, что проверяющий не в состоянии найти всех возможных свидетелей, поэтому вам, возможно, придется предоставить их самостоятельно. Один из способов обработки компилятором такого случая — перечисление во время выполнения всех возможных целочисленных последовательностей, пока не будет найдена та, которая удовлетворяет предикату. Это завершится, так как верификатор доказал, что такая последовательность существует. Однако вы будете разочарованы производительностью во время выполнения.
Если вы действительно думаете, что задача компилятора тривиальна, отправьте запрос на извлечение.
Это не работает ... я получаю
Error: this assign-such-that statement is too advanced for the current compiler; Dafny's heuristics cannot find any bound for variable 'x'