нарушение утверждения при проверке функции Max в Dafny?

Следующая программа приводит к нарушению утверждения assert v==40: почему ? Программа может быть проверена, когда массив a содержит только один элемент.

method Max(a:array<int>) returns(max:int)
requires 1<=a.Length
ensures forall j:int :: 0<=j< a.Length ==> max >= a[j]
ensures exists j:int :: 0<=j< a.Length &&  max == a[j]
{
   max:=a[0];
   var i :=1;
   while(i < a.Length)
   invariant 1<=i<=a.Length
   decreases a.Length-i
   invariant forall j:int :: 0<=j<i ==> max >= a[j]
   invariant exists j:int :: 0<=j<i &&  max == a[j]
   {
     if(a[i] >= max){max := a[i];}
     i := i + 1;
   }
}
method Test(){
   var a := new int[2];
   a[0],a[1] := 40,10;
   var v:int:=Max(a);
   assert v==40;
}

dafny
person Quentin Carbonnelle    schedule 30.04.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Это действительно странно! Все сводится к тому, как Дафни обращается с квантификаторами.

Давайте начнем с доказательства на человеческом уровне того, что утверждение действительно верно. Из постусловий Max мы знаем две вещи о v: (1) оно не меньше любого элемента в a и (2) оно равно некоторому элементу a. Согласно (2) v равно 40 или 10, а согласно (1) v равно как минимум 40 (потому что оно не меньше a[0], что равно 40). Поскольку 10 не меньше 40, v не может быть 10, поэтому должно быть 40.

Теперь, почему Дафни не может понять это автоматически? Это из-за квантификатора forall в (1). Dafny (на самом деле Z3) использует «триггеры» для аппроксимации поведения универсальных кванторов. (Без какого-либо приближения рассуждения с кванторами вообще неразрешимы, поэтому требуется некоторое ограничение, подобное этому.) Триггеры работают так, что для каждого квантификатора в программе выводится синтаксический шаблон, называемый триггером. Затем этот квантификатор полностью игнорируется, если триггер не соответствует какому-либо выражению в контексте.

В этом примере факт (1) будет иметь триггер a[j]. (Вы можете увидеть, какие триггеры выводятся в Visual Studio, VSCode или emacs, наведя указатель мыши на квантификатор. Или в командной строке, передав параметр /printTooltips и найдя номер строки.) Это означает, что квантификатор будет игнорироваться, если нет некоторое выражение формы a[foo] в контексте для любого выражения foo. Затем (1) будет создан экземпляр с foo для j, и мы узнаем max >= a[foo].

Поскольку в утверждении вашего метода Test не упоминается какое-либо выражение формы a[foo], Дафни вообще не сможет использовать факт (1), что приводит к ложному нарушению утверждения.

Один из способов исправить ваш метод Test — добавить утверждение

assert v >= a[0];

непосредственно перед другим утверждением. Это ключевое следствие факта (1), которое нам нужно для доказательства на человеческом уровне, и оно содержит выражение a[0], которое соответствует триггеру, позволяя Дафни создать экземпляр квантификатора. Затем остальная часть доказательства проходит автоматически.

Дополнительные сведения о триггерах в целом и о том, как их писать вручную, см. в этом ответе.

person James Wilcox    schedule 30.04.2018