To: csg379@lists.ccs.neu.edu
Subject: my proof for pointcut implication
Cc: lieber

My answer to hw 3, part 3D:

Claim:
If there is a polynomial algorithm for pointcut implication
then there is a polynomial algorithm for unsatisfiability
of boolean formulas.


This is an expansion of the proof that is in the paper
and what Robbie wrote in his solution.

We start with a boolean formula phi and translate it into
a pointcut S(phi) and a meta graph S(G), the "ladder graph"
following the construction
for Select-Sat. To summarize, we translate the operators as follows:
Without loss of generality, we assume the boolean formula is in
conjunctive normal form. This implies that negation is only applied
to variables. We translate following this table:

X1    -> cflow(call (void  X1.f()))
!X1   -> cflow(call (void NX1.f())) 
and -> intersection
or  -> union

The ladder graph has source s and target t.

Now we consider the poincut implication S(phi) => empty,
false is the pointcut that always returns the empty set.
Clearly, (S(phi) => empty) is true iff the pointcut S(phi)
will always return empty for all instances of the meta graph
(= executions of the program). We call such an S(phi) unsatisfiable.
The complement is the set of satisfiable pointcuts.

Next we claim that S(phi) returns empty for all instances (i.e., is unsatisfiable)
iff phi is unsatisfiable. (This is the same
argument as for Select-Sat):

Case 1: 
If phi is satisfiable, then S(phi) is satisfiable.

A satisfying assignment for phi is translated to  an instance
where S(phi) will select a node as follows:
X1 is true:   go through X1
X1 is false:  go through NX1
This will create an instance (a path) where S(phi) selects the target t.

Case 2:
If S(phi) is satisfiable, then phi is satisfiable.

S(phi) is satisfiable means that there is a path from s to t.
If the path goes through X1, we set X1 to true.
If the path goes through NX1, we set X1 to false.

Therefore, phi is satisfiable iff S(phi) is satisfiable and by 
contraposition: "iff property"  phi is unsatisfiable iff S(phi) is unsatisfiable. 

Here is the polynomial algorithm for unsatisfiablility of boolean
formulas in conjuctive normal form:

Translate phi to S(phi) and G(phi) ans ask the question:
Does S(phi) => false hold. If the answer is yes, \phi is unsatisfiable,
otherwise satisfiable. The correctness of the algorithm follows
from the "iff" property shown above.
QED