abandoned verification bug

May 25, 2015 at 5:34 AM
It seems to me that there is a bug with respect to verification of code
that uses specified, but not-yet-implemented classes.
In particular, function methods in such classes appear to cause problems.
The example below illustrates the issue. It incorrectly gives no verification errors,
though the compiler correctly complains about the unimplemented methods.

class Queue 
{ 
ghost var q : set<int> ; 

constructor Init()
modifies this;  
ensures q == {} ; 


method insert(n:nat) 
modifies this; 
ensures q == old(q) + {n} ; 

function method nonEmpty():bool
ensures nonEmpty() == (q != {}); 

} 

method Main() 

{

// Dafny complains about the following, if included   
//assert false ; 

var q := new Queue.Init()  ; 

// and the following 
//assert false; 

q.insert(0) ;  

// and the following 
// assert false; 

// this is OK 
assert q.nonEmpty() ; 

// but there is no complaint about the following, or anything that follows! 
// it seems the verification is simply abandoned at this point. 

assert false; 

while q.nonEmpty() 
{ 
assert false ; 
} 

assert false ; 
}
May 28, 2015 at 5:28 AM
The problem goes away when I add "reads this" to the nonEmpty method. It would have been good to get the warning that this is necessary!