  Verifying whether a procedure is observationally pure is useful in many
software engineering scenarios. An observationally pure procedure always
returns the same value for the same argument, and thus mimics a mathematical
function. The problem is challenging when procedures use private mutable global
variables, e.g., for memoization of frequently returned answers, and when they
involve recursion.
  We present a novel verification approach for this problem. Our approach
involves encoding the procedure's code as a formula that is a disjunction of
path constraints, with the recursive calls being replaced in the formula with
references to a mathematical function symbol. Then, a theorem prover is invoked
to check whether the formula that has been constructed agrees with the function
symbol referred to above in terms of input-output behavior for all arguments.
  We evaluate our approach on a set of realistic examples, using the Boogie
intermediate language and theorem prover. Our evaluation shows that the
invariants are easy to construct manually, and that our approach is effective
at verifying observationally pure procedures.
