CODEWITHSUNDEEP
dafnyformal-verificationinduction
Kropius Dop
Kropius Dop

Reputation: 105

Deleting element at specific index failing in Dafny

I have the following problem: I have to implement a priority queue in Dafny. I have the following interface:

trait PQSpec {

var nrOfElements: int;
var capacity: int;
var contents: array<int>;
var priorities: array<int>;
predicate Valid()
reads this
{
    0 <= nrOfElements <= capacity && 
    capacity == contents.Length &&
    capacity == priorities.Length 
}

method isEmpty() returns (b: bool)
requires capacity > 0
{
    return nrOfElements > 0; 
}

I did not inserted the abstract methods in the trait, because they are not relevant to my problem

nrOfElements - will hold the number of elements in the priority queue

capacity - will hild the maximum number of elements that can be stored

contents will hold the values

priorities will hold the priorities

Valid - should ensure the fact that my priority queue is valid in terms of nrOfElements and capacity(or at least I hope I do that)

The problem is the following piece of code:

class PQImpl extends PQSpec{
    constructor (aCapacity: int)
    requires aCapacity > 0
    ensures Valid(){
        contents :=  new int[aCapacity](_ => 1);
        priorities := new int[aCapacity](_ => -1);
        nrOfElements:= 0;
        capacity := aCapacity;
    }
   method eliminateElementAtIndexFromArray(indexOfElementToBeEliminated: int)
    modifies this
    requires Valid()
    requires indexOfElementToBeEliminated < nrOfElements
    requires indexOfElementToBeEliminated < capacity
    requires nrOfElements <= capacity
    requires nrOfElements > 0
    ensures Valid()
    {   
        var copyOfContents := new int[capacity](_ => 0);
        var copyOfPriorities := new int[capacity](_ => -1);
        var currentIndex := 0;
        var indexOfCopy := 0;

        while(currentIndex < nrOfElements )
        decreases nrOfElements - currentIndex
        invariant currentIndex + 1 <= capacity
        invariant indexOfCopy + 1 <= capacity
        invariant indexOfElementToBeEliminated < nrOfElements
        {   
            assert nrOfElements <= capacity
            assert currentIndex <= nrOfElements + 1;
            assert indexOfCopy < capacity;
            if(indexOfElementToBeEliminated != currentIndex){
                copyOfContents[indexOfCopy] := contents[currentIndex];
                copyOfPriorities[indexOfCopy] := priorities[currentIndex];
                indexOfCopy:=indexOfCopy+1;
            }
            
            currentIndex:=currentIndex+1;
                    
        }

        contents := copyOfContents;
        priorities := copyOfPriorities;
        nrOfElements := nrOfElements - 1;
      
    }

What I try to do is to delete the element that is found at a given index from the array. The way to do it is simply create a new array and not include that value. However, I face the index out of bounds error whenever I do an assignment in the while.

Any help would be appreciated!

Upvotes: 1

Views: 632

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

None of your existing loop invariants are necessary. You need several new invariants:

while currentIndex < nrOfElements
    invariant this.Valid()
    invariant this.capacity == old(this.capacity)
    invariant 0 < this.nrOfElements
    invariant indexOfCopy <= currentIndex
{   
    if indexOfElementToBeEliminated != currentIndex {
        copyOfContents[indexOfCopy] := contents[currentIndex];
        copyOfPriorities[indexOfCopy] := priorities[currentIndex];
        indexOfCopy := indexOfCopy + 1;
    }
    currentIndex := currentIndex + 1;
}

Notice that the first three invariants are about fields of this. (For emphasis, I have explicitly included this. on all the fields.) But this loop does not change this at all! It only changes the newly allocated arrays. By default, Dafny assumes that you intend the loop to modify everything the method is allowed to modify, so the default modifies clause on the loop includes this, since the containing method has a modifies clause that includes this. We can override the default by providing an explicit modifies clause on the loop, which states that only these arrays are modified. Then you can remove the first three invariants, like this:

while currentIndex < nrOfElements
    modifies copyOfContents, copyOfPriorities
    invariant indexOfCopy <= currentIndex
{   
    if indexOfElementToBeEliminated != currentIndex {
        copyOfContents[indexOfCopy] := contents[currentIndex];
        copyOfPriorities[indexOfCopy] := priorities[currentIndex];
        indexOfCopy := indexOfCopy + 1;
    }
    currentIndex := currentIndex + 1;
}

If you prefer, another equivalent way to do this last version is to use unchanged to express that this is not modified by the loop:

while currentIndex < nrOfElements
    invariant indexOfCopy <= currentIndex
    invariant unchanged(this)
{   
    if indexOfElementToBeEliminated != currentIndex {
        copyOfContents[indexOfCopy] := contents[currentIndex];
        copyOfPriorities[indexOfCopy] := priorities[currentIndex];
        indexOfCopy := indexOfCopy + 1;
    }
    currentIndex := currentIndex + 1;
}

I prefer to use the modifies clause instead of unchanged, because the modifies clause allows us to express what changed syntactically to the solver, whereas unchanged only expresses what changed semantically "after the fact" using an additional invariant. But they both work fine, so you should pick whichever one you like better.

Upvotes: 0

Related Questions