Сможет ли дафний ассерт справиться с ! ЛОЖЬ

Окончательное закомментированное утверждение не будет проверено, но при запуске приведенного выше оператора if будет напечатано. ВЫХОД

ohb= true
ohx= false
palin(xe) == false
ohx ==false

function method palin(a:seq<int>) :bool {
    forall i:int :: (0<=i && i<(|a|/2)) ==> a[i]==a[|a|-i -1]
}
method Main() {   
    var xe:seq<int> := [0,1,2,3,0];
    var se:seq<int> := [0,1,2,1,0];
    var ohb := palin(se);
    var ohx :bool := palin(xe);
    print "ohb= ",ohb,"\n";
    print "ohx= ",ohx,"\n";
    assert palin(se);
    if (palin(xe) == false) {print "palin(xe) == false\n";}
    if (!ohx)  {print "ohx ==false\n";}
    //assert !ohx;
}

dafny
person david streader    schedule 20.07.2020    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Неудачное утверждение означает, что верификатор не может автоматически найти доказательство. Если вы считаете, что свойство выполняется, вам нужно написать доказательство (или часть доказательства).

Для вашей программы доказательство того, что что-то не является палиндромом, сводится к показу позиции, нарушающей свойство палиндрома. С точки зрения логики, вы пытаетесь доказать отрицание forall, которое является exists, а для доказательства exists вам нужно предоставить свидетеля для связанной переменной i.

В вашем примере достаточно следующего:

predicate method palin(a: seq<int>) {
  forall i :: 0 <= i < |a| / 2 ==> a[i] == a[|a| - i - 1]
}

method Main() {   
  var xe := [0,1,2,3,0];
  var se := [0,1,2,1,0];
  var ohb := palin(se);
  var ohx := palin(xe);
  print "ohb= ", ohb, "\n";
  print "ohx= ", ohx, "\n";
  assert palin(se);
  if palin(xe) == false { print "palin(xe) == false\n"; }
  if !ohx { print "ohx == false\n"; }
  assert !ohx by {
    assert xe[1] != xe[3];
  }
}
person Rustan Leino    schedule 21.07.2020