Mobile Objects “Must” Move Safely
Sébastien Briais, Uwe Nestmann · 2002
Øjeblik is a lexically-scoped, object-based calculus that represents a distribution-free subset of the LAN-based programming language Obliq. The surrogate operation on ojeblik-objects, which is the abstraction of migration on Øbliqobjects, is a combined operation derived from the more primitive operations cloning and aliasing . In short, surrogation on an object turns the object into an alias for a clone of itself; it amounts to migration when the original and the clone reside on different distribution sites. In previous work, we studied the conditions under which surrogation is safe, i.e., transparent to object clients. To this aim, we developed two complementary formal descriptions of Øjeblik’s semantics, one as an operational semantics on Øjeblik-configurations, and another one by translation into a process calculus. We used the former to explain typical (mis-)behaviors of Øjeblik programs, but only the latter to perform rigorous correctness proofs w.r.t. may-equivalence. In this paper, we offer new formal proofs, now based on the operational semantics of Øjeblik, making the results as well as the proofs accessible also to readers not familiar with process calculi. Furthermore, we strengthen our former results by using, in addition to may-equivalence, the much more distinguishing notion of must-equivalence. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.