schillic
commented
7 years ago This is good news! It means two things:
- You found the place where the old proof was wrong - because it did not match the old definition.
- The old proof works for the new definition (i.e., we do not need to change it).
Hi @schillic and @Heizmann, Last time we discussed a bit about our new definition of error relevancy and also what does it mean for our theorem and its proof. And we came to the conclusion that the proof might be wrong. But i think maybe it is not that simple to just plainly say that it is wrong. Here is the theorem:
In the theorem, if we think of the term "relevant" according to the old definition then it means that if we replace "x:=t" with havoc then some assume statement is becoming "restrictive" which was not restrictive before. That is another way of saying that replacing the assignment with havoc now introduces blocking executions in the trace that were not there before. and that is also our new definition of relevancy. The only difference is, that in our new definition, we say that the trace might already contain blocking executions and if changing an assignment with havoc introduces more blocking executions then that assignment is relevant.
So, when in the proof, we say in "<--" direction , that if the implication does not hold then the assignment is relevant (according to old definition), we are just saying that the if the implication does not hold then that means if we replace the assignment with havoc, then we are introducing blocking executions in a trace which had no blocking executions before. Which is absolutely true and consistent with our new definition and there fore i think there should not be a mistake in the proof.
But i am not exactly sure what i said above is 100% correct :D Maybe you can comment on it and let me know what you think. We definitely need to modify the proof a little bit, but not rewrite it from the beginning.