Verifying a bounded queue

Oct 2, 2013 at 7:32 PM
My question is: if I remove the assumption in the dequeue method (in the body), why won't dequeue verify? (see below)

I'm attempting to verify a FIFO queue. The queue is a bounded: it's implemented as an array and will not grow passed size n ('items' in the code example).

It will not verify without 'assume fifo[1..items] == q[0..items-1];' in the dequeue() method. Notice the array is shifted every time the first item is dequeued and the sequence is just 'fifo := fifo[1..]'. I want Dafny to verify the shifting the array is the same as removing the front item of the fifo sequence.

I'm also assuming using assumptions aren't good practice in Dafny, since one false assumption can cause bad side effects. Therefore, I'm trying to get this to verify without assumptions.

So, why won't dequeue verify? (Enqueue won't verify without an assumption also, but I'm much more curious regarding to dequeue).
class {:autocontracts} Queue<Data> {
    ghost var fifo : seq<Data>;
    var q : array<Data>;
    var items : int;
    var maxSize : int;

    predicate Valid 
        reads this;
        reads q;
    {
        q != null &&
        0 <=  items <= |fifo| < maxSize+1 <= q.Length &&
        fifo == q[0..items]
    }

    constructor(size : int) 
        modifies this;
        requires 0 < size;
        ensures maxSize == size;
        ensures items == 0;
        ensures maxSize >= 0;
        ensures q.Length > 0;
    {
        maxSize := size;
        q := new Data[maxSize+1];
        items := 0;
        fifo := q[0..items];
    }

    method enqueue(d : Data) 
        ensures fifo == old(fifo) + [d];
    {
        assume items < maxSize; // will not verify without this
        q[items] := d;
        items := items + 1;
        fifo := fifo + [d];
        assert items <= maxSize;
    }

    method dequeue() returns (d : Data)
        requires items >= 1;
        ensures fifo == old(fifo)[1..] && d == old(fifo)[0];
        ensures items == old(items)-1;
    {
        
        var j: int := 0;    
        d := q[0];
        assert d == q[0] == q[0..items][0];
        assert fifo == q[0..items];

        while (0 <= j && j < items)
            invariant 0 <= j <= items;
            modifies q;
            decreases items-j;
        {
            q[j] := q[j+1];
            j := j + 1;
        }

        assume fifo[1..items] == q[0..items-1]; // will not verify without this
        fifo := fifo[1..];
        items := items - 1;
    }

}
I would appreciate any other tips as well.

Thank you,

Matt
Oct 7, 2013 at 3:51 PM
I found the problem.

The main culprit was Dafny can't reason the shifted array (after while loop in dequeue()) is the same as 'fifo[1..]'. I created a different queue and was able to verify it using a lemma. I added the lemma after the array shifting. The lemma seems to assist Dafny in the reasoning process.

I should have paid more attention to the lemma tutorial. Sorry :(

Matt