Reasoning about code mobility with mobile UNITY

Advancements in network technology have led to the emergence of new computi ng paradigms that challenge established programming practices by employing weak forms of consistency and dynamic forms of binding. Code mobility, for instance, allows for invocation-time binding between a code fragment and th e location where it executes. Similarly, mobile computing allows hosts (and the software they execute) to alter their physical location. Despite appar ent similarities, the two paradigms are distinct in their treatment of loca tion and movement. This paper seeks to uncover a common foundation for the two paradigms by exploring the manner in which stereotypical forms of code mobility can be expressed in a programming notation developed for mobile co mputing. Several solutions to a distributed simulation problem are used to illustrate the modeling strategy and the ability to construct assertional-s tyle proofs for programs that employ code mobility.