search

numairmansur / Error-Localization

http://numairmansur.github.io/Error-Localization/final/final.pdf
4 stars 0 forks source link

Does the theorem / Proof still makes sense with the new definition ? #16

Open numairmansur opened 7 years ago

numairmansur commented 7 years ago

Problem in the proof.

An assignment in a trace, is relevant if and only if the following implication does not hold : P ==> WP( Q, havoc(x) )

"==>" If the assignment is relevant, then the implication does not hold.

"<==" If the implication does not hold, then the assignment is relevant.

numairmansur commented 7 years ago

"-->" If "x:=t" is relevant (changing it to havoc cause some assume statement to become restrictive), then the following implication does not hold. This is totally fine. I think the previous definition is somehow exactly the same as our new definition but it models less cases. The new definition is more general. If the old definition holds, then the new definition also definitely holds and hence the implication should also not hold. "<--" If the implication does not hold, then the assignment is relevant. relevant means that some assume is becoming restrictive which was not restrictive before. Not inconsistent with our new definition.

numairmansur commented 7 years ago

I think the previous definition is somehow the sub case of the new definition. In previous definition we somehow make an assumption that the trace initially was not restrictive, that means that initially the trace had no blocking executions but replacing the assignment statement with havoc makes an assume statement restrictive (that means some new blocking executions are now introduced). So if the theorem is proving "<--" side correctly then it really is no problem because that means that if the implication does not hold, then the assignment is introducing some blocking executions. That is all what the old defintion says. that assuming the trace dont have a blocking execution, changing the assignment will introduce blocking executions. This is also consistent with our new definition. WIth the new definiton, we are saying that if the trace already have blocking executions, and if we change the assignment to havoc and new blocking executions are introduced, then the assginemnt is relevant.

numairmansur commented 7 years ago

image