Checking Observational Purity of Procedures.

Verifying whether a procedure is observationally pure (that is, it always returns the same result for the same input argument) is challenging when the procedure uses mutable (private) global variables, e.g., for memoization, and when the procedure is recursive.