heap_free and pure

[davidcok]

A heap_free clause ought to be also pure, I think -- intuitively a method that does not read the heap ought also not to cause changes in it (which makes it checkable as part of type checking rather than needing reasoning) -- though I recognize that Mattias has some corner cases that could be argued.

My question is should a) it be an error if a heap_free method is not also declared pure, or b) should heap_free implicitly imply pure, or c) should we keep them independent, requiring the user to indicate both where appropriate.

I'm in favor of (b)

[leavens]

I also favor (b). This will generate a warning if a method that is annotated as heap_free also assigns to static fields or does I/O, which are the only other ways to violate purity in a heap-free method.

[mattulbrich]

I think I favour as few special rules as possible, so that I'd favour (c) (or perhaps a) I agree that heap_free only makes sense for pure methods.