In the present day, distributed systems are becoming more and more important. It can be difficult to stop such systems to perform an update, either because they are critical infrastructure, like air traffic control systems, or simply because we don't have direct control of the nodes. As a result of this, dynamic updates are of great interest, but so far no standard approach has emerged that strikes a good balance between the partly conflicting goals of safety, flexibility and performance. This thesis presents a specification of a dynamic update system in the Creol framework for distributed, object oriented programming. The system is designed to dynamically update classes, and includes a procedure for converting existing object instances to an updated version. A method is presented for controlling when and how an update is applied, and the necessary conditions for a correct update are discussed. The system presented is a low-overhead solution, lazily transferring state from one version to the next. It is very flexible, even allowing changes to the inheritance hierarchy. The system is given a formal specification in rewriting logic, extending Creol's semantics. Consequently, formal reasoning about the correctness of updates is possible.