Ojeblik 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 Obliq-objects, 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 Ojeblik's semantics, one as an operational semantics on Ojeblik-configurations, and another one by translation into a process calculus. We used the former to explain typical (mis-)behaviors of Ojeblik 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 Ojeblik, 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.
展开▼
