Дафни: не найдены термины для запуска и последующая ошибка утверждения - PullRequest
Новая
       54

Дафни: не найдены термины для запуска и последующая ошибка утверждения

2 голосов
/ 19 марта 2020

Это код, который я написал для метода, который возвращает максимум два целых числа: 

predicate greater(x: int, a: int, b: int){
    (x >= a) && (x >= b)
}

method Max(a: int, b: int) returns (max: int)
    ensures max >= a
    ensures max >= b
    ensures forall x /*{:trigger greater(x,a,b)}*/ :: (greater(x,a,b)) ==> x >= max
{
    if (a > b){
        max := a;
    }else{
        max := b;
    }
//  assert greater(max, a, b); - trivial assertion
}

method Main(){
    var res:= Max(4, 5);

    assert res == 5;
}

Как вы можете видеть, я попробовал оба эти метода, встречающихся на странице Wiki. (ручное назначение триггеров, а также добавление тривиального бесполезного утверждения в тело метода. Однако я все еще получаю ошибку подтверждения.

Я не уверен, что еще делать. Я прочитал другие ответы как это , это и это , но никто не помог мне до сих пор.

PS: я знаю, что есть более простой способ написать однако, постусловия для этого конкретного метода, я действительно буду sh моделировать постусловия только в терминах квантификатора Форалла.

1 Ответ

1 голос
/ 20 марта 2020

Давайте на время забудем greater и просто посмотрим, чего вы пытаетесь достичь. После вызова Max в Main вы знаете следующее (из постусловия Max): 

res >= 4
res >= 5
forall x :: x >= 4 && x >= 5 ==> x >= res

Вы пытаетесь доказать res == 5 из этого. Вторая из этих трех вещей сразу дает вам половину этого равенства, поэтому все, что вам нужно сделать, это получить 5 >= res. Если вы создадите экземпляр квантификатора с 5 для x, вы получите 

5 >= 4 && 5 >= 4 ==> 5 >= res

, который упрощается до 5 >= res, что вам нужно, так что это конец вашего доказательства.

Таким образом, доказательство сводится к созданию экземпляра квантификатора с 5 для x. Далее вам нужно немного узнать о том, как верификатор Dafny создает квантификаторы. По сути, он делает это, просматривая «форму» квантификатора и ища похожие вещи в контексте того, что вы пытаетесь доказать. Под «формой» я подразумеваю такие вещи, как «функции и предикаты, которые он использует». Обычно этот метод работает хорошо, но в вашем случае квантификатор настолько прост, что не имеет никакой «формы», о которой можно было бы говорить. Следовательно, верификатор не может найти необходимое создание экземпляра.

Было бы хорошо, если бы мы могли просто сказать «эй, попробуйте создать экземпляр этого количественного выражения с помощью 5 для x». Ну, мы можем, если мы дадим квантификатору некоторую «форму», к которой мы можем обратиться. Вот что пытаются сказать вики и другие руководства. Здесь полезно ввести предикат greater. (Не пытайтесь писать аннотации триггера вручную.)

Хорошо, после введения greater ваша спецификация говорит: 

ensures greater(max, a, b)
ensures forall x :: greater(x, a, b) ==> x >= max

Это говорит "max удовлетворяет greater(max, a, b)" и «среди всех значений x, которые удовлетворяют greater(x, a, b), max является наименьшим». После вызова Max в Main у нас тогда будет: 

greater(res, 4, 5)
forall x :: greater(x, 4, 5) ==> x >= res

Напомним, я сказал, что верификатор пытается выяснить, как создаются кванторы, просматривая квантификатор и просматривая контекст вокруг вашего утверждения. и вы пытаетесь создать экземпляр квантификатора с 5 для x. Итак, если вы можете добавить что-то в контекст непосредственно перед утверждением, которое побуждает верификатора выполнить это создание, тогда все готово.

Вот ответ: вы хотите ввести термин greater(5, 4, 5). Это имеет форму, очень похожую на greater(x, 4, 5) в квантификаторе. Из-за этого сходства верификатор будет создавать экземпляр x с 5, что дает 

greater(5, 4, 5) ==> 5 >= res

И поскольку greater(5, 4, 5) легко доказывается как true, следует необходимый факт 5 >= res.

Итак, измените тело Main на 

var res := Max(4, 5);
assert greater(5, 4, 5);
assert res == 5;

и все готово. Верификатор докажет оба утверждения. Первое тривиально, и после его подтверждения верификатор может использовать термин greater(5, 4, 5) в доказательстве второго утверждения. Именно этот термин вызывает квантификатор, который выдает факт 5 >= res, который подтверждает второе утверждение.

Я хочу отметить, что большинство кванторов, которые мы пытаемся доказать do , имеют некоторую форму уже. В вашем случае предикат greater был введен для того, чтобы придать квантификатору некоторую форму. Техника добавления дополнительного утверждения (здесь assert greater(5, 4, 5)) остается той же самой, независимо от того, был ли greater уже определен или был введен как тривиальный предикат, обеспечивающий форму.

...