除了 "no visible side-effects" 之外，[Pure] 是否对代码合同有任何影响？

Question

PureAttribute documentation 说：

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

1. 这是 Microsoft Code Contracts 中纯函数的唯一要求吗？

2. 并且；该模型是否假设异常是结果（而不是副作用）？

我问是因为，在更一般的上下文中，a pure function 也 意味着输出仅取决于输入； IE。它不能是 I/O 或随机函数的结果。

有人可能还会争辩说，纯函数总是为外部表达式产生一个值，这可能与异常相反。

如果 [Pure] 确实限于限制较少的形式，是否有等效于“[FunctionalPure]”的形式？

Answer 1

静态分析器假定连续两次调用具有相同参数的同一个纯函数会产生相同的结果。

给出

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

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

生成警告："Suggested assumption: Assumption can be proven: Consider changing it into an assert."

因此，例如 DateTime.Now 不能使用 Pure 属性进行注释。

至于异常，似乎没有什么不允许的，也没有要求始终抛出它们。一般来说，不可能有。对于几乎任何代码，您总是可以获得 OutOfMemoryException，甚至是具有先前成功的相同参数的纯函数。