Does [Pure] have any implications other than "no visible side-effects" to Code Contracts?

Question

Indicates that a type or method is pure, that is, it does not make any visible state changes

Is this the only requirement of a Pure function under in Microsoft Code Contracts?
And; does this model assume that Exceptions are results (as opposed to side-effects)?

I ask because, in a more general context, a pure function also implies that the output is only dependent upon the input; ie. it cannot be the result of I/O or a stochastic function.

One might also argue that a pure function always yields a value to the outer expression, possibly in opposition to Exceptions.

If [Pure] is indeed limited to the less restrictive form, is there an equivalent of a "[FunctionalPure]"?

Related discussion: http://stackoverflow.com/questions/12335245/why-is-catching-an-exception-non-pure-but-throwing-an-exception-is-pure — 500 - Internal Server Error, Jan 02 '15 at 20:56
@500-InternalServerError Thanks - that's a very good read. I hadn't thought about it in terms of that deterministic (or lack of) nature. — user2864740, Jan 02 '15 at 20:59

score 2 · Accepted Answer · answered Jan 02 '15 at 21:04

The static analyser assumes that calling the same pure function with the same arguments twice in a row produces the same result.

Given

[Pure]
public delegate int F(int i);

public class A
{
  public void f(F f)
  {
    var i = f(1);
    Contract.Assert(i == f(1));
  }
}

a warning is generated: "Suggested assumption: Assumption can be proven: Consider changing it into an assert."

So for instance DateTime.Now must not be annoted with the Pure attribute.

As for exceptions, there doesn't seem to be anything disallowing them, nor for requiring them to be thrown consistently. In general, there cannot be. You can always get an OutOfMemoryException for pretty much any code, even a pure function with the same arguments that previously succeeded.

Does [Pure] have any implications other than "no visible side-effects" to Code Contracts?

1 Answers1