Mobile Objects as Mobile Processes
| Autor: | Uwe Nestmann, Josva Kleist, Massimo Merro |
|---|---|
| Rok vydání: | 2002 |
| Předmět: |
Object-oriented programming
Object migration Correctness Distributed Objects Programming language Semantics (computer science) pi-calculus Concurrency Distributed object Semantics computer.software_genre Object (computer science) Proofs Operational semantics Pi-calculus Computer Science Applications Theoretical Computer Science Computational Theory and Mathematics Objects computer Migration Abstraction (linguistics) Mathematics Information Systems |
| Zdroj: | Massimo, M, Nestmann, U & Kleist, J 2002, ' Mobile Objects as Mobile Processes ', Information and Computation, no. 177, pp. 1-47 . Aalborg University |
| ISSN: | 0890-5401 |
| Popis: | Obliq is a lexically scoped, distributed, object-based programming language. In Obliq, the migration of an object is proposed as creating a clone of the object at the target site, whereafter the original object is turned into an alias for the clone. Obliq has only an informal semantics, so there is no proof that this style of migration is safe, i.e., transparent to object clients. In previous work, we introduced ojeblik, an abstraction of Obliq, where, by lexical scoping, sites have been abstracted away. We used ojeblik in order to exhibit how the semantics behind Obliq's implementation renders migration unsafe. We also suggested a modified semantics that we conjectured instead to be safe. In this paper, we rewrite our modified semantics of ojeblik in terms of the π-calculus, and we use it to formally prove the correctness of object surrogation, the abstraction of object migration in Ojeblik. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect