Encapsulation (2)
Within set methods of original variables, we can imbed methods to update ghost replicas.
Within get methods we can assert pre- conditions that reveal unexpected errors (failure to maintain consistent ghost copies, due to incomplete static analysis or refactoring omissions.
We can also imbed trace statements that log all variable update events at runtime.