dafny assert 可以处理“！false”吗答案

【问题标题】：Can dafny assert cope with "! false"dafny assert 可以处理“！false”吗
【发布时间】：2020-11-09 07:58:21
【问题描述】：

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

【解决方案1】：

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

对于您的程序，证明某事物不是回文归结为显示违反回文属性的位置。就逻辑而言，您试图证明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];
  }
}

【讨论】：