Assertion Checking Unified
We revisit the connection between equality assertion checking in
programs and unification that was recently described in [GT06].
Using a general formalization of this
connection, we establish interesting
connections between the complexity of assertion checking in programs
and unification theory of the underlying program expressions.
In particular, we show that assertion checking is:
These results generalize several recently published results and also
establish several new results.
In essence, they provide new techniques for backward analysis of programs
based on novel integration of theorem proving technology in program analysis.
- PTIME for programs with
nondeterministic conditionals that use
expressions from a strict unitary theory,
coNP-hard for programs with
nondeterministic conditionals that use expressions from a
bitary theory, and
decidable for programs with
disequality guards that use expressions from a convex finitary theory.