# Checking Observational Purity of Procedures

## TL;DR

This paper introduces a new verification method to determine if procedures are observationally pure, even with private mutable state and recursion, using formula encoding and theorem proving.

## Contribution

It presents a novel approach that encodes procedures as formulas and uses theorem proving to verify observational purity, handling complex cases involving recursion and mutable state.

## Key findings

- Effective verification of observational purity demonstrated on realistic examples
- Manual invariant construction is straightforward
- Approach successfully verifies procedures with recursion and mutable state

## Abstract

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.