Abstract: Often when programmers modify source code they intend to preserve some parts of the program behaviour. We propose a formal criterion by which to characterise the preserved part of the program behaviour. Two program versions are equivalent up to a set of affected objects A, if executions of the two versions correspond at each execution step when we do not consider the objects in A. We propose a sufficient condition for this criterion. It suffices to establish that traces of method calls and returns between A objects and other objects are equivalent. Examining the stack and heap at each execution step is not necessary. We give a proof of the sufficiency of this condition, much of which we have automatically verified using Dafny. We also discuss our experiences with Dafny and detail how some interesting parts of our Dafny proof work.