vdm++ - 纯操作调用可能不是引用透明的？

Question

当我尝试对序列的前两个元素使用纯操作时，会收到此警告。

代码看起来像这样：

class A
functions
  public func: Seq -> bool
  func(sq) == (
    (hd sq).pureOperation() inter (hd (tl sq)).pureOperation() <> {}
  );
end A

它会导致警告：“纯操作调用可能不是引用透明的”，并且 Overture 在函数下方放置了波浪状的黄线hd。

是什么导致了这个警告，我该怎么办？

Answer 1

This warning was the result of considerable debate when pure operations were added to the language definition. The problem is that, ultimately, even if an operation is labelled as pure (and obeys all the rules that follow) we cannot be certain that calling the operation with the same arguments will always yield the same value. This is required for referential transparency in functions, so we produce a warning.

The warning only occurs when pure operations are called from functions, but there is no way to avoid the warning if you have to do this.

For example, consider the following - the pure_i operation is "pure", since it simply returns a state value, but that state can be changed by the not_transparent operation, and so the function f(x) will return different values for the same argument:

class A
instance variables
    static public i : nat := 0

operations
    static public pure pure_i : () ==> nat
    pure_i() == return i;

functions
    f : nat -> nat
    f(x) == pure_i() + x;

operations
    static public not_transparent : () ==> ()
    not_transparent() == (
        i := 1;
    );
end A