Problem while trying to use the quantifiers in pre-post condition

Jan 2, 2013 at 3:42 AM

When I try to write a simple program postcondition, which should be trivially true,I get  unsatisfied postcondition  as output.

Here is my postcondition:

there exists an integer i in range (-10:10), such that i==0,i.e.

ensures exists{int i in (-10:10); i==0};

according to me this postcondition should be trivially true for all examples, but thats not the case.

Please help me

Thanks, in advance

Developer
Jan 2, 2013 at 10:18 PM

Unfortunately, SMT solvers such as Z3, which is the prover behind Spec#, have weak support for existential quantifiers. It is sometimes possible to provide intermediate assertions that help Z3 find a witness for the quantified variable, but I have no suggestion how to fix your example. If this is part of a bigger example, you could post the entire method; maybe we can come up with a fix then.

Cheers,
   Peter

Jan 4, 2013 at 10:58 AM

I am not talking about any specific example, but in general. The post-condition and example i have is pretty complex,so I am not posting it here, I tried, in all the examples provided on the page, this assertion seems to fail for all of them. It would nice of you even if you could give me any workaround,such that I could write my conditions in a different way and make them work(I tried negating, and using forall quantifier but that doesnot works ).

For example:

class Example

{

  int x;
  void Inc(int y) 

  ensures exists{int i in (-10:10); i==0};

   {    x += y; 

   }

}