Formalizing class dynamic software updating

Dynamic software updating enables running programs to be updated while executing. In this paper, a simple formal system is established with the goal of understanding the underlying foundations of updating classes, for the purpose of understanding how to best build reliable updatable programs. The update calculus is built for O-O software with a precise mathematical semantics. It is formulated as an extension of a core calculus for Featherweight Java, and supports updating technology similar to that of the programming language Java and C++. The calculus also presents what kind of update can be made dynamically. At the end of the paper, we proof that these update is type safety.