The thesis addresses the design of multiple-server implementations for services in distributed systems-a generalization of the replication management problem. A frequently used correctness criteria for replication management is that clients of a service not be able to distinguish a single-server implementation from on that involves multiple servers. Our approach formalizes this idea. It is based on viewing a single-server implementation of a service as a specification of that service. A multiple-server implementation is considered correct if it implements this single-server based specification. We show how program proof outlines can be viewed as specifications and, using refinement mappings, define what it means for one proof outline to implement another. The notion of a structural refinement, which formalizes the relationship between a program and the result of performing step-wise refinement, is defined. When one proof outline is a structural refinement of the other, simplified proof obligations can be used to show that the one implements the other. Finally, a methodology for designing a multiple-server implementation of a service is presented. The methodology is based on structural refinement and on viewing proof outlines as specifications. A designer defines a refinement mapping to express the relationship between the state space of a given single-server implementation of a service and the state space of the desired multiple-server implementation. Using this refinement mapping, a provably correct multiple-server implementation is derived from the single server one. Different refinement mappings as well as different single-server based specifications result in different implementations. Examples illustrate the concepts and the methodology.