Ensures unproven even with Assume using Static Checker

hello,

in writing new code using code contracts, i've encountered problem using contract.ensures postcondition.

i'm using contract.assume assume postcondition true, static checker still warning me ensures unproven.

take following code example:

public class testclass {  	private queue<int> queue;  	[contractinvariantmethod] 	private void objectinvariants() { 		contract.invariant(queue != null); 	}  	private testclass() { 		queue = new queue<int>(); 	}  	public void testmethod() { 		contract.ensures(queue.count == contract.oldvalue<int>(queue.count) + 1);  		enqueue(); 	}  	public void enqueue() { 		contract.ensures(queue.count == contract.oldvalue<int>(queue.count) + 1);  		queue.enqueue(10); 		contract.assume(queue.count == contract.oldvalue<int>(queue.count) + 1); 	}  }

the queue<t> class doesn't appear have contracts yet, it's expected static checker won't able tell item has been added queue.

what can't understand, however, why contract.assume call isn't enough stop static checker giving warning. i'm explicitly stating post-condition met.

if can shed light on this, appreciated.

thanks in advance.

hi,

my first idea repeat contract.assume call in testmethod body. so i've tried load code in own project. immediatly gives error, not surprising. call contract.oldvalue<> allowed in contract.ensures calls, , hence not possible in contract.assume call.

on other hand, how ensure count indeed oldvalue + 1? thread may have take enqueued item out of queue already, before exit testmethod.

what explicitly count before enqueue , make assumption on local stored count. example become this:

   public class testclass   {      private queue<int> queue;      [contractinvariantmethod]    private void objectinvariants()    {     contract.invariant(queue != null);    }      private testclass()    {     queue = new queue<int>();    }      public void testmethod()    {     contract.ensures(queue.count == contract.oldvalue<int>(queue.count) + 1);       int count = queue.count;     enqueue();     contract.assume(queue.count == count + 1);    }      public void enqueue()    {     contract.ensures(queue.count == contract.oldvalue<int>(queue.count) + 1);     int count = queue.count;       queue.enqueue(10);     contract.assume(queue.count == count + 1);    }     }  

maybe helpfull you.

meile zetstra

---

http://blogger.xs4all.nl/mzetstra

DevLabs  >  Code Contracts