Checking Observational Purity of Procedures
This addresses a software engineering problem for developers needing to ensure functional behavior in code, but it is incremental as it builds on existing verification techniques.
The paper tackles the problem of verifying observational purity of procedures, which is challenging with private mutable globals and recursion, by presenting a novel verification approach that encodes procedures as formulas and uses a theorem prover, showing effectiveness on realistic examples with easy manual invariant construction.
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.