鲁棒环境演算类型演化系统的扩充 |
| |
引用本文: | 陈韬略,冯扬悦,吕建,韩婷婷.鲁棒环境演算类型演化系统的扩充[J].南京大学学报(自然科学版),2004,40(5):531-539. |
| |
作者姓名: | 陈韬略 冯扬悦 吕建 韩婷婷 |
| |
作者单位: | 南京大学计算机软件新技术国家重点实验室,南京,210093 |
| |
基金项目: | 国家自然科学基金,国家高技术研究发展计划(863计划),国家重点基础研究发展计划(973计划) |
| |
摘 要: | 移动计算是在网络技术发展过程中涌现出来的一种新的分布计算范型,移动环境演算是一种广为使用的描述移动计算的形式化模型,鲁棒环境演算1]是针对这种演算的一种改进.文献2]提出了类型演化问题,然而其研究只是针对不含有通信原语的纯演算进行.在2]的基础上,进一步讨论了此问题.通过引入消息类型和消息体类型,并将之与原有的进程类型和环境类型相结合,提出了一个支持类型演化的能够对带有消息传递的进程项类型化的类型系统,从而将2]的工作扩充到整个鲁棒环境演算中.证明了类型系统的正确性.同时给出了一个最小类型算法,在给定类型上下文的条件下,算法能够计算出任意进程项的类型;并证明了算法的可靠性和完备性.
|
关 键 词: | 进程代数 环境演算 类型演化 类型系统 |
Extension of Type Evolution System for Robust Mobile Ambients |
| |
Abstract: | Computation with mobility becomes a novel distributed computation paradigm with the
development of network technology. The calculus of mobile ambients is a widely studied formal
mechanism for describing both mobile computing and mobile computation. This paper deals with the
type evolution problem for a variant of this calculus, the robust mobile ambient(ROAM) provided by
1]. In detail, the message type and message body type are introduced, and a type system that can
type process terms with message passing and support type evolution is provided, thus the results of
2] can be extended to the full ROAM. Furthermore, this paper gives the proof of the correctness of
the type system and introduces a minimal type-checking algorithm. The soundness and completeness
of the algorithm are also shown. |
| |
Keywords: | process algebra mobile ambient type evolution type system |
本文献已被 CNKI 维普 万方数据 等数据库收录! |
|