functional-programmingdafnyformal-verificationmultiset

Dafny verifier fails to prove the consequence of multiset

I'm working with Dafny and trying to understand how specifications, particularly modifies and ensures multiset, affect verification.

I have a method do_nothing which is specified to modify an array a but ensures that the multiset of its elements remains unchanged. The body of the method is empty.

method do_nothing(a: array<int>)
  modifies a
  ensures multiset(a[..]) == multiset(old(a[..]))
{
  // nothing is done
}

method test()
{
  var a := new int[6] [2, -3, 4, 1, 1, 7];
  assert a[..] == [2, -3, 4, 1, 1, 7]; // Verifies
  assert a[0] !=0 ;                    // Verifies

  do_nothing(a);

  assert a[0] != 0; // <-- Verification Error: This assertion cannot be proved
}

My Expectation:

Since there is no 0 inside a at all, and dafny agrees that do_nothing ensures multiset(a[..]) == multiset(old(a[..])). Therefore, the assertion a[0] != 0 should hold and verify successfully.

The Problem:

Dafny fails to verify the final assertion assert a[0] != 0;

Solution

  • Multisets have hidden triggers to avoid overwhelming Dafny's verifier with triggerS.

    You can add this assertion after do_nothing to help Dafny trigger some necessary axioms on multisets.

    assert 0 !in multiset(a[..]);

    This will make your code to pass verification. Note that, because this is about triggers, inserting the following no-op code would do the same

    ghost var _ := 0 !in multiset(a[..]);