Checking Observational Purity of Procedures

Abstract

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.

We present a deductive verification approach for this problem. Our approach encodes the procedure’s code as a logical formula, with recursive calls being modeled using a mathematical function symbol assuming that the procedure is observationally pure. Then, a theorem prover is invoked to check whether this logical formula agrees with the function symbol referred to above in terms of input-output behavior for all arguments. We prove the soundness of this approach.

We then present a conservative approximation of the first approach that reduces the verification problem to one of checking whether a quantifier-free formula is satisfiable and prove the soundness of the second approach.

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.

1 Introduction

A procedure in an imperative programming language is said to be observationally pure (OP) if for each specific argument value it has a specific return value, across all possible sequences of calls to the procedure, irrespective of what other code runs between these calls. In other words, the input-output behavior of an OP procedure mimics a mathematical function.

A deterministic procedure that does not read any pre-existing state other than its arguments is trivially OP. However, it is common for procedures to update and read global variables, typically for performance optimization, while still being OP. In this paper, we focus on the problem of checking observational purity of procedures that read and write global variables, especially in the presence of recursion, which makes the problem harder.

Motivating Example. We use procedure ‘factCache’ in Listing 1.1 as our running example. It returns n! for a given argument n, and caches the return value of the most recent call. It uses two private global variables, g and lastN, to implement the caching. g is initialized to $-1$. After the first call to the procedure onwards, g stores the return value of the most recent call, and lastN stores the argument of the most recent call. Clearly this procedure is OP, and mimics the input-output behavior of a factorial procedure that does not cache any results.

Proposed Approach. Our approach is based on Floyd-Hoare logic, which typically requires a specification of the procedure to be provided. One candidate specification would be a full functional specification of the procedure. If the user specifies that factCache realizes n!, then the verifier could replace Line 10 in the code with ‘g = n * (n − 1)!’. This, on paper, is sufficient to assert that Line 12 always assigns n! to result. However, to establish that Line 8 also does the same, an invariant would need to be provided that describes the possible values of g before an invocation to the procedure. In our example, a suitable invariant would be ‘(g = $-1$) $\vee$ (g = lastN!)’. The verifier would also need to verify that at the procedure’s exit the invariant is re-established. Lines 10–12, with the recursive call replaced by (n − 1)!, suffices on paper to re-establish the invariant.

The candidate approach described above, while plausible, suffers from two weaknesses. First, a mathematical specification of the function being computed may be complex and non-trivial to write. (Note, for example, that factCache is defined for negative integers while factorial is not. Thus, the previous candidate specification is actually incorrect for this edge case.) Second, the underlying theorem prover would need to prove complex arithmetic properties, e.g., that n * (n − 1)! is equal to n!. Complex proofs such as this may be beyond the scope of many existing theorem provers.

Our key insight is to sidestep the challenges mentioned by introducing a function symbol, say factCache, and replacing the recursive call for the purposes of verification with this function symbol. (Note that we reuse the same symbol for two purposes, which may be slightly confusing here. One denotes the procedure name, while the other denotes a function symbol for use in a logical formula. The italicized name here denotes the function symbol.) Intuitively, factCache represents the mathematical function that the given procedure mimics if the procedure is OP. In our example, Line 10 would become ‘g = n * factCache(n − 1)’. This step needs no human involvement. The approach needs an invariant; however, in a novel manner, we allow the invariant also to refer to factCache. In our example, a suitable invariant would be ‘(g = −1) $\vee$ (g = lastN * factCache(lastN − 1))’. This sort of invariant is relatively easy to construct; e.g., a human could arrive at it just by looking at Line 2 and with a local reasoning on Lines 10 and 11. Given this invariant, (a) a theorem prover could infer that the condition in Line 7 implies that Line 8 necessarily copies the value of ‘n * factCache(n − 1)’ into ‘result’. Due to the transformation to Line 10 mentioned above, (b) the theorem prover can infer that Line 12 also does the same. Note that since these two expressions are syntactically identical, a theorem prover can easily establish that they are equal in value. Finally, since Line 6 is reached under a different condition than Lines 8 and 12, the verifier has finished establishing that the procedure always returns the same expression in n for any given value of n.

Similarly, using the modified Line 10 mentioned above and from Line 11, the prover can re-establish that g is equal to ‘lastN * factCache(lastN $-\,1$)’ when control reaches Line 12. Hence, the necessary step of proving the given invariant to be a valid invariant is also complete.

Note, the effectiveness of the approach depends on the nature of the given invariant. For instance, if the given invariant was ‘(g = −1) $\vee$ (g = lastN!)’, which is also technically correct, then the theorem prover may not be able to establish that in Lines 8 and 12 the variable ‘g’ always stores the same expression in n. However, it is our claim that in fact it is the invariant ‘(g = − 1) $\vee$ (g = lastN * factCache(lastN − 1))’ that is easier to infer by a human or by a potential tool, as justified by us two paragraphs above.

Salient Aspects of Our Approach. This paper makes two significant contributions. First, it tackles the circularity problem that arises due to the use of a presumed-to-be OP procedure in assertions and invariants and the use of these invariants in proving the procedure to be OP. This requires us to prove the soundness of an approach that simultaneously verifies observational purity as well the validity of invariants (as they cannot be decoupled).

Secondly, we show that a direct approach to this verification problem (which we call the existential approach) reduces it to a problem of verifying that a logical formula is a tautology. The structure of the generated formula, however, makes the resulting theorem prover instances hard. We show how a conservative approximation can be used to convert this hard problem into an easier problem of checking satisfiability of a quantifier-free formula, which is something within the scope of state-of-the-art theorem provers.

The most closely related previous approaches are by Barnett et al. [1, 2], and by Naumann [3]. These approaches check observational purity of procedures that maintain mutable global state. However, none of these approaches use a function symbol in place of recursive calls or within invariants. Therefore, it is not clear that these approaches can verify recursive procedures. Barnett et al., in fact, state “there is a circularity - it would take a delicate argument, and additional conditions, to avoid unsoundness in this case”. To the best of our knowledge ours is the first paper to show that it is feasible to check observational purity of procedures that maintain mutable global state for optimization purposes and that make use of recursion.

Being able to verify that a procedure is OP has many potential applications. The most obvious one is that OP procedures can be memoized. That is, input-output pairs can be recorded in a table, and calls to the procedure can be elided whenever an argument is seen more than once. This would not change the semantics of the overall program that calls the procedure, because the procedure always returns the same value for the same argument (and mutates only private global variables). Another application is that if a loop contains a call to an OP procedure, then the loop can be parallelized (provided the procedure is modified to access and update its private global variables in a single atomic operation).

The rest of this paper is structured as follows. Section 2 introduces the core programming language that we address. Section 3 provides formal semantics for our language, as well as definitions of invariants and observational purity. Section 4 describes our approach formally. Section 5 discusses an approach for generating an invariant automatically in certain cases. Section 6 describes evaluation of our approach on a few realistic examples. Section 7 describes related work. More details about the proofs and the examples can be found in [4].

2 Language Syntax

In this paper, we assume that the input to the purity checker is a library consisting of one or more procedures, with shared state consisting of one or more variables that are private to the library. We refer to these variables as “global” variables to indicate that they retain their values across multiple invocations of the library procedures, but they cannot be accessed or modified by procedures outside the library (that is, the clients of the library).

Fig. 1.

Programming language syntax and meta-variables

In Fig. 1, we present the syntax of a simple programming language that we address in this paper. Given the foundational focus of this work, we keep the programming language very simple, but the ideas we present can be generalized. A return statement is required in each procedure, and is permitted only as the last statement of the procedure. The language does not contain any looping construct. Loops can be modelled as recursive procedures. The formal parameters of a procedure are readonly and cannot be modified within the procedure. We omit types from the language. We permit only variables of primitive types. In particular, the language does not allow pointers or dynamic memory allocation. Note that expressions are pure (that is, they have no side effects) in this language, and a procedure call is not allowed in an expression. Each procedure call is modelled as a separate statement.

For simplicity of presentation, without loss of conceptual generality, we assume that the library consists of a single (possibly recursive) procedure, with a single formal parameter. In the sequel, we will use the symbol $\textsc {p}$ (as a metavariable) to represent this library procedure, $p$ (as a metavariable) to represent the name of this procedure, and will assume that the name of the formal parameter is n. If the procedure is of the form “$p$ (n) { S; return r }”, we refer to r as the return variable, and refer to “S; return r” as the procedure body and denote it as $\text {body}(\textsc {p})$. The library also contains, outside of the procedure’s code, a sequence of initializing declarations of the global variables used in the procedure, of the form “g1 := c1; $\ldots$; gN := cN”. These initializations are assumed to be performed once during any execution of the client application, just before the first call to the procedure $\textsc {p}$ is placed by the client application.

Throughout this paper we use the word ‘procedure’ to refer to the library procedure $\textsc {p}$, and use the word ‘function’ to refer to a mathematical function.

3 A Semantic Definition of Purity

In this section, we formalize the input-output semantics of the procedure $\textsc {p}$ as a relation , where indicates that an invocation of $\textsc {p}$ with input n may return a result of r. The procedure is defined to be observationally pure if the relation is a (partial) function: that is, if and , then $r_1 = r_2$.

The object of our analysis is a single-procedure library, not the entire (client) application. (Our approach can be generalized to handle multi-procedure libraries.) The result of our analysis is valid for any client program that uses the procedure/library. The only assumptions we make are: (a) The shared state used by the library (the global variables) are private to the library and cannot be modified by the rest of the program, and (b) The client invokes the library procedures sequentially: no concurrent or overlapping invocations of the library procedures by a concurrent client are permitted.

The following semantic formalism is motivated by the above observations. It can be seen as the semantics of the so-called “most general sequential client” of procedure $\textsc {p}$, which is the program: while (*) x = $p$ (random());. The executions (of $\textsc {p}$) produced by this program include all possible executions (of $\textsc {p}$) produced by all sequential clients.

Fig. 2.

A small-step operational semantics for our language, represented as a relation $\sigma _1 \rightarrow _{\textsc {p}}\sigma _2$. A state $\sigma _i$ is a configuration of the form $((\texttt {S}, \rho _\ell ) \gamma , \rho _g)$ where $\texttt {S}$ captures statements to be executed in current procedure, $\rho _\ell$ assigns values to local variables, $\gamma$ is the call-stack (excluding current procedure), and $\rho _g$ assigns values to global variables.

Let $G$ denote the set of global variables. Let $L$ denote the set of local variables. Let $\mathcal {V}$ denote the set of numeric values (that the variables can take). An element $\rho _g\in \varSigma _G= G\hookrightarrow \mathcal {V}$ maps global variables to their values. An element $\rho _\ell \in \varSigma _L= L\hookrightarrow \mathcal {V}$ maps local variables to their values. We define a local continuation to be a statement sequence ending with a return statement. We use a local continuation to represent the part of the procedure body that still remains to be executed. Let $\varSigma _C$ represent the set of local continuations. The set of runtime states (or simply, states) is defined to be $(\varSigma _C\times \varSigma _L)^* \times \varSigma _G$, where the first component represents a runtime stack, and the second component the values of global variables. We denote individual states using symbols $\sigma , \sigma _1, \sigma _i$, etc. The runtime stack is a sequence, each element of which is a pair $(\texttt {S},\rho _\ell )$ consisting of the remaining procedure fragment $\texttt {S}$ to be executed and the values of local variables $\rho _\ell$. We write $(\texttt {S},\rho _\ell )\gamma$ to indicate a stack where the topmost entry is $(\texttt {S},\rho _\ell )$ and $\gamma$ represents the remaining part of the stack.

We say that a state $((\texttt {S},\rho _\ell )\gamma ,\rho _g)$ is an entry-state if its location is at the procedure entry point (i.e., if $\texttt {S}$ is the entire body of the procedure), and we say that it is an exit-state if its location is at the procedure exit point (i.e., if $\texttt {S}$ consists of just a return statement).

A procedure $\textsc {p}$ determines a single-step execution relation $\rightarrow _{\textsc {p}}$, where $\sigma _1 \rightarrow _{\textsc {p}} \sigma _2$ indicates that execution proceeds from state $\sigma _1$ to state $\sigma _2$ in a single step. Figure 2 defines this semantics. The semantics of evaluation of a side-effect-free expression is captured by a relation $({\rho },{\texttt {e}}) \Downarrow {v}$, indicating that the expression $\texttt {e}$ evaluates to value v in an environment $\rho$ (by environment, we mean an element of $(G\,\cup \,L) \hookrightarrow \mathcal {V}$). We omit the definition of this relation, which is straightforward. We use the notation $\rho _1 \uplus \rho _2$ to denote the union of two disjoint maps $\rho _1$ and $\rho _2$.

Note that most rules captures the usual semantics of the language constructs. The last two rules, however, capture the semantics of the most-general sequential client explained previously: when the call stack is empty, a new invocation of the procedure may be initiated (with an arbitrary parameter value).

Note that all the following definitions are parametric over a given procedure $\textsc {p}$. E.g., we will use the word “execution” as shorthand for “execution of $\textsc {p}$”.

We define an execution (of $\textsc {p}$) to be a sequence of states $\sigma _0 \sigma _1 \cdots \sigma _n$ such that $\sigma _i \rightarrow _{\textsc {p}} \sigma _{i+1}$ for all $0 \le i < n$. Let $\sigma _{\text {init}}$ denote the initial state of the library; i.e., this is the element of $\varSigma _G$ that is induced by the sequence of initializing declarations of the library, namely, “g1 := c1; $\ldots$; gN := cN”. We say that an execution $\sigma _0 \sigma _1 \cdots \sigma _n$ is a feasible execution if $\sigma _0 = \sigma _{\text {init}}$. Note, intuitively, a feasible execution corresponds to the sequence of states visited within the library across all invocations of the library procedure over the course of a single execution of the most-general client mentioned above; also, since the most-general client supplies a random parameter value to each invocation of $\textsc {p}$, in general multiple feasible executions of the library may exist.

We define a trace (of $\textsc {p}$) to be a substring $\pi = \sigma _0 \cdots \sigma _n$ of a feasible execution such that: (a) $\sigma _0$ is entry-state (b) $\sigma _n$ is an exit-state, and (c) $\sigma _n$ corresponds to the return from the invocation represented by $\sigma _0$. In other words, a trace is a state sequence corresponding to a single invocation of the procedure. A trace may contain within it nested sub-traces due to recursive calls, which are themselves traces. Given a trace $\pi = \sigma _0 \cdots \sigma _n$, we define $\textit{initial}(\pi )$ to be $\sigma _0$, $\textit{final}(\pi )$ to be $\sigma _n$, $\textit{input}(\pi )$ to be value of the input parameter in $\textit{initial}(\pi )$, and $\textit{output}(\pi )$ to be the value of the return variable in $\textit{final}(\pi )$.

We define the relation to be $\{ (\textit{input}(\pi ),\textit{output}(\pi )) \; | \; \pi \text { is a trace of } \textsc {p}\}$.

Definition 1

(Observational Purity). A procedure $\textsc {p}$ is said to be observationally pure if the relation is a (partial) function: that is, if for all n, $r_1$, $r_2$, if and , then $r_1 = r_2$.

Logical Formula and Invariants. Our methodology makes use of logical formulae for different purposes, including to express a given invariant. Our logical formulae use the local and global variables in the library procedure as free variables, use the same operators as allowed in our language, and make use of universal as well as existential quantification. Given a formula $\varphi$, we write $\rho \models \varphi$ to denote that $\varphi$ evaluates to true when its free variables are assigned values from the environment $\rho$.

As discussed in Sect. 1, one of our central ideas is to allow the names of the library procedures to be referred to in the invariant; e.g., our running example becomes amenable to our analysis using an invariant such as ‘(g = $-1$) $\vee$ (g = lastN * factCache(lastN − 1))’. We therefore allow the use of library procedure names (in our simplified presentation, the name $p$) as free variables in logical formulae. Correspondingly, we let each environment $\rho$ map each procedure name to a mathematical function in addition to mapping variables to numeric values, and extend the semantics of $\rho \models \varphi$ by substituting the values of both variables and procedure names in $\varphi$ from the environment $\rho$.

Given an environment $\rho$, a procedure name $p$, and a mathematical function f, we will write $\rho [p\mapsto f]$ to indicate the updated environment that maps $p$ to the value f and maps every other variable x to its original value $\rho [x]$. We will write $(\rho ,f) \models \varphi$ to denote that $\rho [p\mapsto f] \models \varphi$.

Given a state $\sigma = ((\texttt {S},\rho _\ell )\gamma ,\rho _g)$, we define $\text {env}(\sigma )$ to be $\rho _\ell \uplus \rho _g$, and given a state $\sigma = ([],\rho _g)$, we define $\text {env}(\sigma )$ to be just $\rho _g$. We write $(\sigma ,f) \models \varphi$ to denote that $(\text {env}(\sigma ),f) \models \varphi$. For any execution or trace $\pi$, we write $(\pi ,f) \models \varphi$ if for every entry-state and exit-state $\sigma$ in $\pi$, $(\sigma ,f) \models \varphi$. We now introduce another definition of observational purity.

Definition 2

(Observational Purity wrt an Invariant). Given an invariant $\varphi ^{inv}$, a library procedure $\textsc {p}$ is said to satisfy $\mathrm {pure}(\varphi ^{inv})$ if there exists a function f such that for every trace $\pi$ of $\textsc {p}$, $\textit{output}(\pi ) = f(\textit{input}(\pi ))$ and $(\pi ,f) \models \varphi ^{inv}$.

It is easy to see that if procedure $\textsc {p}$ satisfies $\mathrm {pure}(\varphi ^{inv})$ wrt any given candidate invariant $\varphi ^{inv}$, then $\textsc {p}$ is observationally pure as per Definition 1.

4 Checking Purity Using a Theorem Prover

In this section we provide two different approaches that, given a procedure $\textsc {p}$ and a candidate invariant $\varphi ^{inv}$, use a theorem prover to check conservatively whether procedure $\textsc {p}$ satisfies $\mathrm {pure}(\varphi ^{inv})$.

4.1 Verification Condition Generation

We first describe an adaptation of standard verification-condition generation techniques (e.g., see [5]) that we use as a common first step in both our approaches. Given a procedure $\textsc {p}$, a candidate invariant $\varphi ^{inv}$, our goal is to compute a pair $(\varphi ^{post},\varphi ^{vc})$ where $\varphi ^{post}$ is a postcondition describing the state that exists after an execution of $\text {body}(\textsc {p})$ starting from a state that satisfies $\varphi ^{inv}$, and $\varphi ^{vc}$ is a verification-condition that must hold true for the execution to satisfy its invariants and assertions.

We first transform the procedure body as below to create an internal representation that is input to the postcondition and verification condition generator. In the internal representation, we allow the following extra forms of statements (with their usual meaning): havoc(x), assume e, and assert e.

• 1. For any assignment statement “x := e” where e contains x, we introduce a new temporary variable t and replace the assignment statement with “t := e; x := t”.

• 2. For every procedure invocation “x := $p$ (y)”, we first ensure that y is a local variable (by introducing a temporary if needed). We then replace the statement by the code fragment “assert $\varphi ^{inv}$ ; havoc(g1); ... havoc(gN); assume $\varphi ^{inv}\wedge$ x = $p$ (y)”, where g1 to gN are the global variables. Note that the procedure call has been eliminated, and replaced with an “assume” expression that refers to the function symbol $p$. In other words, there are no procedure calls in the transformed procedure.

• 3. We replace the “return x” statement by “assert $\varphi ^{inv}$”. Note that we intentionally do not assert that the return value equals $p(n)$.

Let $\textsc {TB}(\textsc {p}, \varphi ^{inv})$ denote the transformed body of procedure $\textsc {p}$ obtained as above.

Fig. 3.

Generation of verification-condition and postcondition.

We then compute postconditions as formally described in Fig. 3. This lets us compute for each program point $\ell$ in the procedure, a condition $\varphi _{\ell }$ that describes what we expect to hold true when execution reaches $\ell$ if we start executing the procedure in a state satisfying $\varphi ^{inv}$ and if every recursive invocation of the procedure also terminates in a state satisfying $\varphi ^{inv}$. We compute this using the standard rules for the postcondition of a statement. For an assignment statement “x := e”, we use existential quantification over x to represent the value of x prior to the execution of the statement. If we rename these existentially quantified variables with unique new names, we can lift all the existential quantifiers to the outermost level. When transformed thus, the condition $\varphi _{\ell }$ takes the form $\exists x_1 \cdots x_n. \varphi$, where $\varphi$ is quantifier-free and $x_1, \cdots , x_n$ denote intermediate values of variables along the execution path from procedure-entry to program point $\ell$.

We compute a verification condition $\varphi ^{vc}$ that represents the conditions we must check to ensure that an execution through the procedure satisfies its obligations: namely, that the invariant holds true at every call-site and at procedure-exit. Let $\ell$ denote a call-site or the procedure-exit. We need to check that $\varphi _{\ell } \Rightarrow \varphi ^{inv}$ holds. Thus, the generated verification condition essentially consists of the conjunction of this check over all call-sites and procedure-exit.

Finally, the function $\textsc {postvc}$ computes the postcondition and verification condition for the entire procedure as shown in Fig. 3. (Thus, it returns a pair of formulae.) Note that this function also adds the check that the initial state must satisfy $\varphi ^{inv}$ to the verification condition (as the basis condition for induction). $\textsc {init}(\textsc {p})$ is basically the formula “g1 = c1 $\wedge \ldots$ gN = cN” (see Sect. 2).

Example

We now illustrate the postcondition and verification condition generated from our factorial example presented in Listing 1.1. Listing 1.2 shows the example expressed in our language and transformed as described earlier (using function $\textsc {TB}$), using a supplied candidate invariant $\varphi ^{inv}$.

Figure 4 illustrates the computation of postcondition and verification condition from this transformed example. In this figure, we use $\varphi ^{pre}_{cs}$ to denote the precondition computed to hold just before the recursive callsite, and $\varphi ^{post}_{cs}$ to denote the postcondition computed to hold just after the recursive callsite. The postcondition $\varphi ^{post}$ (at the end of the procedure body) is itself a disjunction of three path-conditions representing execution through the three different paths in the program. In this illustration, we have simplified the logical conditions by omitting useless existential quantifications (that is, any quantification of the form $\exists x. \psi$ where x does not occur in $\psi$). Note that the existentially quantified g and lastN in $\varphi ^{post}_{cs}$ denote the values of these globals before the recursive call. Similarly, the existentially quantified g and lastN in $\varphi ^{path}_3$ denote the values of these globals when the recursive call terminates, while the free variables g and lastN denote the final values of these globals.

Fig. 4.

The different formulae computed from the procedure in Listing 1.2 by our postcondition and verification-condition computation.

4.2 Approach 1: Existential Approach

Let $\textsc {p}$ be a procedure with input parameter n and return variable r. Let $\textsc {postvc}({\textsc {p}},{\varphi ^{inv}}) = (\varphi ^{post},\varphi ^{vc})$. Let $\psi ^e$ denote the formula $\varphi ^{vc}\wedge (\varphi ^{post}\Rightarrow (r = p(n)))$. Let $\overline{x}$ denote the sequence of all free variables in $\psi ^e$ except for p. We define $\textsc {ea}(\textsc {p},\varphi ^{inv})$ to be the formula $\forall \overline{x}. \psi ^e$.

In this approach, we use a theorem prover to check whether $\textsc {ea}(\textsc {p},\varphi ^{inv})$ is satisfiable. As shown by the following theorem, satisfiability of $\textsc {ea}(\textsc {p},\varphi ^{inv})$ establishes that $\textsc {p}$ satisfies $\mathrm {pure}(\varphi ^{inv})$.

Theorem 1

A procedure $\textsc {p}$ satisfies $\mathrm {pure}(\varphi ^{inv})$ if $\exists p. \textsc {ea}(\textsc {p},\varphi ^{inv})$ is a tautology (which holds iff $\textsc {ea}(\textsc {p},\varphi ^{inv})$ is satisfiable).

Proof

Note that p is the only free variable in $\textsc {ea}(\textsc {p},\varphi ^{inv})$. Assume that $[p \mapsto f]$ is a satisfying assignment for $\forall \overline{x}. \psi ^e$. We show that for every feasible execution $\pi$: (P1) $(\pi , f) \vdash \varphi ^{inv}$, and (P2) for every trace $\pi '$ inside $\pi$, $\textit{output}(\pi ') = f(\textit{input}(\pi '))$. This implies that $\textsc {p}$ satisfies $\mathrm {pure}(\varphi ^{inv})$.

In particular, for any feasible execution $\pi$, we prove by induction over the execution steps in $\pi$ that

• 1. For any entry state $\sigma$ in $\pi$, $(\sigma ,f) \vdash \varphi ^{inv}$.

• 2. For any exit state $\sigma$ in $\pi$, $(\sigma ,f) \vdash \varphi ^{inv}$.

• 3. For any exit state $\sigma$ in $\pi$, if it is the exit state of a trace $\pi '$, then $\textit{output}(\pi ') = f(\textit{input}(\pi '))$.

If the above properties fail to hold, we can identify a trace $\pi '$ corresponding to the first such failure. It can be shown that the sequence of states visited by this trace, when substituted for $\overline{x}$, are a witness that $[p \mapsto f]$ is not a satisfying assignment for $\forall \overline{x}. \psi ^e$. This is a contradiction of our original assumption.

Please see [4] for more details of the proof.    $\square$

4.3 Approach 2: Impurity Witness Approach

The existential approach presented in the previous section has a drawback. Checking satisfiability of $\textsc {ea}(\textsc {p},\varphi ^{inv})$ is hard because it contains universal quantifiers and existing theorem provers do not work well enough for this approach. We now present an approximation of the existential approach that is easier to use with existing theorem provers. This new approach, which we will refer to as the impurity witness approach, reduces the problem to that of checking whether a quantifier-free formula is unsatisfiable, which is better suited to the capabilities of state-of-the-art theorem provers. This approach focuses on finding a counterexample to show that the procedure is impure or it violates the candidate invariant.

Let $\textsc {p}$ be a procedure with input parameter n and return variable r. Let $\textsc {postvc}({\textsc {p}},{\varphi ^{inv}}) = (\varphi ^{post},\varphi ^{vc})$. Let $\varphi ^{post}_\alpha$ denote the formula obtained by replacing every free variable x other than p in $\varphi ^{post}$ by a new free variable $x_\alpha$. Define $\varphi ^{post}_\beta$ similarly. Define $\textsc {iw}(\textsc {p}, \varphi ^{inv})$ to be the formula $(\lnot \varphi ^{vc}) \,\vee \, (\varphi ^{post}_\alpha \,\wedge \, \varphi ^{post}_\beta \,\wedge \, (n_\alpha = n_\beta ) \,\wedge \, (r_\alpha \ne r_\beta ))$.

The impurity witness approach checks whether $\textsc {iw}(\textsc {p}, \varphi ^{inv})$ is satisfiable. This can be done by separately checking whether $\lnot \varphi ^{vc}$ is satisfiable and whether $(\varphi ^{post}_\alpha \,\wedge \, \varphi ^{post}_\beta \,\wedge \, (n_\alpha = n_\beta )\, \wedge \, (r_\alpha \ne r_\beta ))$ is satisfiable. As formally defined, $\varphi ^{vc}$ and $\varphi ^{post}$ contain embedded existential quantifications. As explained earlier, these existential quantifiers can be moved to the outside after variable renaming and can be omitted for a satisfiability check. (A formula of the form $\exists \overline{x}. \psi$ is satisfiable iff $\psi$ is satisfiable.) As usual, these existential quantifiers refer to intermediate values of variables along an execution path. Finding a satisfying assignment to these variables essentially identifies a possible execution path (that satisfies some other property).

Theorem 2

A procedure $\textsc {p}$ satisfies $\mathrm {pure}(\varphi ^{inv})$ if $\textsc {iw}(\textsc {p}, \varphi ^{inv})$ is unsatisfiable.

Proof

We say that two traces disagree if they receive the same argument value but return different values. We say that a pair of feasible executions $(\pi _1, \pi _2)$ is an impurity witness if there is a trace $\pi _a$ in $\pi _1$ and a trace $\pi _b$ in $\pi _2$ such that $\pi _a$ and $\pi _b$ disagree.

A trace is said to be compatible with a function f (and vice versa) if the trace’s input-output behavior matches that of the function. An execution is said to be compatible with a function (and vice versa) if every trace in the execution is compatible with the function. We say that a feasible execution $\pi$ strongly satisfies $\varphi ^{inv}$ if for every function f that is compatible with $\pi$, $(\pi ,f) \models \varphi ^{inv}$.

We prove the theorem using the following lemmas: if $\textsc {iw}(\textsc {p}, \varphi ^{inv})$ is unsatisfiable, then Lemmas 2 and 3 imply that the preconditions of Lemma 1 hold and, hence, $\textsc {p}$ satisfies $\mathrm {pure}(\varphi ^{inv})$.

• 1. If there exists no impurity witness, and every feasible execution strongly satisfies $\varphi ^{inv}$, then $\textsc {p}$ satisfies $\mathrm {pure}(\varphi ^{inv})$.

• 2. If a feasible execution $\pi$ that does not strongly satisfy $\varphi ^{inv}$ exists, $\textsc {iw}(\textsc {p}, \varphi ^{inv})$ is satisfiable.

• 3. If an impurity witness exists, then $\textsc {iw}(\textsc {p}, \varphi ^{inv})$ is satisfiable.

1 is straightforward.

For 2, we use a “minimal” feasible execution $\pi$ that does not strongly satisfy $\varphi ^{inv}$ to construct a satisfying assignment to $\lnot \varphi ^{vc}$.

For 3, we use a “minimal” impurity witness to construct a satisfying assignment to $(\varphi ^{post}_\alpha \wedge \varphi ^{post}_\beta \wedge (n_\alpha = n_\beta ) \wedge (r_\alpha \ne r_\beta ))$.

Please see [4] for more details of the proof.    $\square$

5 Generating the Invariant

We now describe a simple but reasonably effective semi-algorithm for generating a candidate invariant automatically from the given procedure. Our approach of Sect. 4 can be used with a manually provided invariant or the candidate invariant generated by this semi-algorithm (whenever it terminates).

The invariant-generation approach is iterative and computes a sequence of progressively weaker candidate invariants $I_0, I_1, \cdots$ and terminates if and when $I_m \equiv I_{m+1}$, at which point $I_m$ is returned as the candidate invariant. The initial candidate invariant $I_0$ captures the initial values of the global variable. In iteration k, we apply a procedure similar to the one described in Sect. 4 and compute the strongest conditions that hold true at every program point if the execution of the procedure starts in a state satisfying $I_{k-1}$ and if every recursive invocation terminates in a state satisfying $I_{k-1}$. We then take the disjunction of the conditions computed at the points before the recursive call-sites and at the end of the procedure, and existentially quantify all local variables. We refer to the resulting formula as $\textsc {Next}(I_{k-1}, \textsc {TB}(\textsc {p},I_{k-1}))$. We take the disjunction of this formula with $I_{k-1}$ and simplify it to get $I_k$.

Figure 5 formalizes this semi-algorithm. Here, we exploit the fact that the assert statements are added precisely at every recursive callsite and end of procedure and these are the places where we take the conditions to be disjuncted.

Fig. 5.

Iterative computation of invariant.

In our running example, $I_0$ is ‘g = $-1\,\wedge$ lastN = 0’. Applying $\textsc {Next}$ to $I_0$ yields $I_0$ itself as the pre-condition at the point just before the recursive call-site, and ‘(g = $-1\,\wedge$ lastN = 0) $\vee$ g = lastN * $p$(lastN − 1)’ (after certain simplifications) as the pre-condition at the end of the procedure. Therefore, $I_1$ is ‘(g = $-1\,\wedge$ lastN = 0) $\vee$ g = lastN * $p$(lastN − 1)’. When we apply $\textsc {Next}$ to $I_1$, the computed pre-conditions are $I_1$ itself at both the program points mentioned above. Therefore, the approach terminates with $I_1$ as the candidate invariant.

6 Evaluation

We have implemented our OP checking approach as a prototype using the Boogie framework [6], and have evaluated the approach using this implementation on several examples. The objective of this evaluation was primarily a sanity check, to test how our approach does on a set of OP as well as non-OP procedures.

We tried several simple non-OP programs, and our implementation terminated with a “no” answer on all of them. We also tried the approach on several OP procedures: (1) the ‘factCache’ running example, (2) a version of a factorial procedure that caches all arguments seen so far and their corresponding return values in an array, (3) a version of factorial that caches only the return value for argument value 19 in a scalar variable, (4) a recursive procedure that returns the $n^ th$ Fibonacci number and caches all its arguments and corresponding return values seen so far in an array, and (5) a “matrix chain multiplication” (MCM) procedure. The last example is based on dynamic programming, and hence naturally uses a table to memoize results for sub-problems. Here, observational purity implies that the procedure always returns the same solution for a given sub-problem, whether a hit was found in the table or not. The appendix of a technical report associated with this paper depicts all the procedures mentioned above as created by us directly in Boogie’s language, as well as the invariants that we supplied manually (in SMT2 format).

It is notable that the theorem prover was not able to handle the instances generated by the“existential approach” even for simple examples. The “impurity witness” approach, however, terminated on all the examples mentioned above with the correct answer, with the theorem prover taking less than 1 s on each example. Please see [4] for more information about the examples used in our evaluation.

7 Related Work

The previous work that is most closely related to our work is by Barnett et al. [1, 2]. Their approach is based on the same notion of observational purity as our approach. Their approach is structurally similar to ours, in terms of needing an invariant, and using an inductive check for both the validity of the invariant as well as the uniqueness of return values for a given argument. However, their approach is based on a more complex notion of invariant than our approach, which relates pairs of global states, and does not use a function symbol to represent recursive calls within the procedure. Hence, their approach does not extend readily to recursive procedures; they in fact state that “there is a circularity - it would take a delicate argument, and additional conditions, to avoid unsoundness in this case”. Our idea of allowing the function symbol in the invariant to represent the recursive call allows recursive procedures to be checked, and also simplifies the specification of the invariant in many cases.

Cok et al. [7] generalize the work of Barnett et al.’s work, and suggest classifying procedures into categories “pure”, “secret”, and “query”. The “query” procedures are observationally pure. Again, recursive procedures are not addressed.

Naumann [3] proposes a notion of observational purity that is also the same as ours. Their paper gives a rigorous but manual methodology for proving the observational purity of a given procedure. Their methodology is not similar to ours; rather, it is based finding a weakly pure procedure that simulates the given procedure as far as externally visible state changes and the return value are concerned. They have no notion of an invariant that uses a function symbol that represents the procedure, and they don’t explicitly address the checking of recursive procedures.

There exists a significant body of work on identifying differences between two similar procedures. For instance, differential assertion checking [8] is a representative from this body, and is for checking if two procedures can ever start from the same state but end in different states such that exactly one of the ending states fails a given assertion. Their approach is based on logical reasoning, and accommodates recursive procedures. Our impurity witness approach has some similarity with their approach, because it is based on comparing the given procedure with itself. However, our comparison is stricter, because in our setting, starting with a common argument value but from different global states that are both within the invariant should not cause a difference in the return value. Furthermore, technically our approach is different because we use an invariant that refers to a function symbol that represents the procedure being checked, which is not a feature of their invariants. Partush et al. [9] solve a similar problem as differential assertion checking, but using abstract interpretation instead of logical reasoning.

There is a substantial body of work on checking if a procedure is pure, in the sense that it does not modify any objects that existed before the procedure was invoked, and does not modify any global variables. Sălcianu et al. [10] describe a static analysis to check purity and Madhavan et al. [11] present an abstract-interpretation based generalization of this analysis. Various tools exist, such as JML [12] and Spec# [13], that use logical techniques based on annotations to prove procedures as pure. Purity is a more restrictive notion than observational purity; procedures such as our ‘factCache’ example are observationally pure, but not pure because they use as well as update state that persists between calls to the procedure.