Reference-type pure methods

Feb 26, 2010 at 7:21 PM

Hi,

I am trying to define some pure abstract methods to use later in writing specifications. I get errors when running Boogie on these methods about not being able to establish pure method consistency. 

I would appreciate any help about writing reference-type pure methods.

Thanks!

Iman

 

Coordinator
Mar 31, 2010 at 10:03 PM

There are a number of difficulties involved in using pure methods in Spec#.  They may get especially tricky when you return references, because there are issues like "Is the reference returned a peer of the receiver?", "Is it a representation object of the receiver?", "Is the returned object consistent?", and "Is the object newly allocated?".  I would recommend looking at section 7 ("Abstraction") of the Spec# tutorial:  http://research.microsoft.com/en-us/um/people/leino/papers/krml189.pdf.  It attempts to explain what's going on.