Pure operation call may not be referentially transparent?

Question

I get this warning when i try to use a pure operation on the two first elements of a sequence.

The code looks something like this:

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

It results in the warning: "Pure operation call may not be referentially transparent" and Overture puts squiggly yellow lines under the hd functions.

What causes this warning and what can I do about it?

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