In this paper we report progress in development of methods for reasoning about the equivalence of objects with memory and the use of these methods to describe sound operations on such objects, in terms of formal program transformations. We also formalize three different aspects of objects: their specification, their behavior, and their canonical representative. Formal connections among these aspects provide methods for optimization and reasoning about systems of objects. To illustrate these ideas we give a formal derivation of an optimized specialized window editor from generic specifications of its components. A new result in this paper enables one to make use of symbolic evaluation (with respect to a set of constraints) to establish the equivalence of objects. This form of evaluation is not only mechanizable, it is also generalizes the conditions under which partial evaluation usually takes place.