Reference-type pure methods

Feb 26, 2010 at 6:21 PM


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.




Mar 31, 2010 at 9: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:  It attempts to explain what's going on.