CODEWITHSUNDEEP
dafny
david streader
david streader

Reputation: 589

Can dafny assert cope with "! false"

The final commented out assert will not validate but when run the if statement above will prints. OUTPUT

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;
}

Upvotes: 1

Views: 432

Answers (1)

Rustan Leino
Rustan Leino

Reputation: 2087

A failing assert means the verifier cannot automatically find a proof. If you think the property holds, you need to write the proof (or part of the proof).

For your program, proving that something is not a palindrome comes down to showing a position that violates the palindrome property. In terms of logic, you're trying to prove the negation of a forall, which is an exists, and to prove an exists you'll need to supply the witness for the bound variable i.

In your example, the following suffices:

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];
  }
}

Upvotes: 1

Related Questions