Help with ensuring a sorted Dafny array

Jan 15, 2013 at 1:46 PM
Edited Jan 15, 2013 at 5:04 PM

Hi, I want to create a simple method that inserts an element (sorted) into a sorted array.

I have tried many things but I cannot get Dafny to ensure that the returning array is sorted. Additionally, I'm having trouble finding things in the documentation (I find it not to be very extensive and well organized). 

Please, if someone with more experience could lend a hand and teach, I'll appreciate it a lot.

The two links below show two different ways I've come up to do this (they both recreate an array and return it). The error they both produce is "Error BP5003: A postcondition might not hold on this return path." (I also don't want to touch the ensures clauses).

Here are the 2 versions:

http://rise4fun.com/Dafny/r5OH

http://rise4fun.com/Dafny/qC9X

Thanks!

Coordinator
Jan 15, 2013 at 8:46 PM

Hello guatebus,

What you're missing is something that trips up many new users of static verification: the loop invariant needs to say everything that is relevant about the state that the loop changes.  Your loop changes the elements of b, but you don't say anything in the invariant about the elements of b.  Hence, the only thing the verifier knows at the end of the loop is that i==a.Length, and nothing is known about the elements of b.

Your job is to specify in the loop invariant what holds true at the very top of every loop iteration.  What you say needs to be strong enough so that, together with the condition i==a.Length, the postcondition follows.  The loop invariant will, more or less, say that b is sorted up until index i.  You will need to think about exactly what the condition "inserted==false" means, for example.

Completing this task will be an instructive experience, and it will help you fix the error in your program.

In your second program, you're trying to use Dafny's "parallel" statement.  In fact, you can solve your problem completely without a loop and instead using a "parallel" statement, see http://www.rise4fun.com/Dafny/ZV3C.  It's possible that looking at my program will help you construct the loop invariant of your first program.

Good luck, and have fun!

  Rustan

Jan 15, 2013 at 11:07 PM

Hello Rustan,

Thanks for your reply. It was very helpful to see your example using parallel to do this task. I don't understand what kind of invariant I can use to get my first program to work, i've tried various things but I still can't get my head around it. Could you please be a bit more specific as to how to get the invariant? (I don't mind if you just tell me your answer, I actually think I can learn from it - this is very new to me).

Thanks again.

G