Mobile objects \`\` must” move safely.

*(English)*Zbl 1048.68026
Jacobs, Bart (ed.) et al., Formal methods for open object-based distributed systems V. IFIP TC6/ WG6.1 5th international conference, FMOODS 2002, Enschede, the Netherlands, March 20–22, 2002. Boston: Kluwer Academic Publishers (ISBN 0-7923-7683-8). IFIP, Int. Fed. Inf. Process. 81, 129-146 (2002).

Summary: Ø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 Øjeblik-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 Ø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.

For the entire collection see [Zbl 0989.00045].

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.

For the entire collection see [Zbl 0989.00045].