CODEWITHSUNDEEP
verificationassertiondafny
user12905235
user12905235

Reputation: 1

Dafny not verifying trivial assertion

The code below, also at https://rise4fun.com/Dafny/I4wM ,

function abst(bits: array<int>,low:int,high: int): int
    requires 0<=low<=high<=8
    requires bits.Length==8
    decreases high-low
    reads bits
{   if low==high
        then 0 
        else 2*abst(bits,low+1,high) + bits[low]
}

method M() {

    var byte: int;
    var bits:= new int[8];
    bits[0]:= 1;
    bits[1]:= 1;
    bits[2]:= 1;
    bits[3]:= 1;
    bits[4]:= 1;
    bits[5]:= 1;
    bits[6]:= 1;
    bits[7]:= 1;

    // assert abst(bits,2,2) == 0; // Why is this needed?
    assert abst(bits,0,2) == 3;

}

fails to verify the assertion on the last line. (I'm using the on-line Dafny at Rise4Fun.) If the assertion just before is uncommented, the verification succeeds.

I'd be grateful for help. Thanks!

Upvotes: 0

Views: 332

Answers (1)

Rustan Leino
Rustan Leino

Reputation: 2087

The Dafny verifier unrolls functions only once or twice. Specifically, if the function occurs in an assertion you're trying to prove (like abst does in your example), then the function gets unrolled twice. However, to prove your assertion, the definition of abst needs to be unrolled 3 times. Therefore, the verifier can't prove it automatically. You'll have to help it along.

When you uncomment the first assertion, it gets used in the proof of the second assertion. Since the first assertion provides the last instantiation of abst that you need, it helps prove the second assertion. The first assertion itself is also proved, but that's automatic, since it only requires one unrolling of abst.

If you write out the proof in detail, it looks like:

calc {
  abst(bits,0,2);
==  // def. abst
  2*abst(bits,1,2) + bits[0];
==  // def. abst
  2*(2*abst(bits,2,2) + bits[1]) + bits[0];
==  // def. abst
  2*(2*0 + bits[1]) + bits[0];
==  // def. bits[0] and bits[1]
  2*(2*0 + 1) + 1;
==  // arithmetic
  3;
}

In this proof, you can see the needed instantiations of the function.

Do you really need arrays in your application? Arrays are allocated on the heap and are mutable (which means you need the reads clause and other complications). If you only need an immutable sequence, then I would recommend you change array<int> to seq<int>. This will make things easier (again--if you don't need the mutable qualities of arrays). Moreover, for your assertion above, it brings another benefit: All the arguments you then pass to abst are literals. For literals, Dafny is willing to unroll functions (more or less) without limits. So, then your original assertion verifies automatically.

Rustan

Upvotes: 1

Related Questions