dafny - dafny assert 可以处理“！false”吗

Question

最终注释掉的断言将不会验证，但是当运行上面的 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

Answer 1

失败的断言意味着验证者无法自动找到证明。如果您认为该属性成立，则需要编写证明（或部分证明）。

对于您的程序，证明某事不是回文归结为显示违反回文属性的位置。在逻辑方面，您试图证明 a 的否定，forall即a exists，并且要证明 aexists您需要为绑定变量提供见证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];
  }
}