Spec# didn't add postcondition to pure method

Aug 9, 2010 at 11:08 AM
Edited Aug 9, 2010 at 11:09 AM


I just installed Spec# 2010-07-20 and the latest stable release of Z3. I discovered that in the code I try to verify, some methods didn't verify anymore. The reason is that these methods use a pure method of the form

[pure] public bool foo() {
  return internal_object.bar() > 0;

If I supply a postcondition ensures result == (internal_object.bar() > 0), then these methods verify. However, according to p. 43 of the tutorial, this postcondition should be added automatically. Hence, I suspect there's a bug in Spec#.

Regards, Boris

Aug 10, 2010 at 12:36 AM

By golly.  I am able to reproduce this with the current version.  It seems that the admissibility check that is performed on the returned expression (to see if it is legal to make an automatic ensures clause from it) is somehow different from the admissibility check performed on a manually supplied ensures clause.  I don't particularly remember any change to that code in the last year, so I'm surprised it's not working now if it used to work in a previous version.  It seems to have something to do with the call to bar(), because I can see that the automatic ensures clause is generated if bar were a field.

So, it seems you have found a bug.