Modular session types for distributed object-oriented programming
Modular session types for distributed object-oriented programming
复制标题
用于分布式面向对象编程的模块化会话类型
DOI：
10.1145/1706299.1706335
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
Gay S
中科院分区：
文献类型：
--
作者：
Gay S
会话类型允许将通信协议指定为类型--理论上讲，这样就可以通过静态类型检查来验证协议实现。我们从三个方面扩展了以前关于分布式面向对象语言的会话类型的工作。(1)我们将会话类型附加到类定义，以指定可能的方法调用序列。(2)我们允许会话类型(协议)实现双模，即划分成可单独调用的方法。(3)将会话类型的通信通道视为对象，将其会话类型与类的会话类型相结合。其结果是完美地统一了通信通道及其会话类型、分布式面向对象编程以及支持非统一对象的类型状态的形式，即动态更改可用方法集的对象。我们定义了一种小型分布式基于类的面向对象语言的语法、操作语义、完善的类型系统和正确而完整的类型检查算法。静态类型确保通道上的消息序列和对象上的方法调用序列都符合类型理论规范，从而确保类型安全。该语言包括会话类型的预期功能(如委托)和面向对象编程的预期功能(如本地状态的封装)。我们还将原型实现描述为Java的扩展。
Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type-checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class definition, to specify the possible sequences of method calls. (2) We allow a session type (protocol) implementation to bemodularized, i.e. partitioned into separately-callable methods. (3) We treat session-typed communication channels as objects, integrating their session types with the session types of classes. The result is an elegant unification of communication channels and their session types, distributed object-oriented programming, and a form of typestates supporting non-uniform objects, i.e. objects that dynamically change the set of available methods. We define syntax, operational semantics, a sound type system, and a correct and complete type checking algorithm for a small distributed class-based object-oriented language. Static typing guarantees that both sequences of messages on channels, and sequences of method calls on objects, conform to type-theoretic specifications, thus ensuring type-safety. The language includes expected features of session types, such as delegation, and expected features of object-oriented programming, such as encapsulation of local state. We also describe a prototype implementation as an extension of Java.
登录
查看更多内容
DOI：
10.1016/j.tcs.2006.06.028
发表时间：
2006-12
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
V. Vasconcelos;S. Gay;A. Ravara
通讯作者：
V. Vasconcelos;S. Gay;A. Ravara
用于协调类 Java 语言的类型安全状态抽象
影响因子：
0.6
作者：
Ferruccio Damiani;Elena Giachino;P. Giannini;S. Drossopoulou
通讯作者：
S. Drossopoulou
DOI：
10.1145/1328438.1328472
发表时间：
2008-01
期刊：
--
影响因子：
--
作者：
Kohei Honda;N. Yoshida;Marco Carbone
通讯作者：
Kohei Honda;N. Yoshida;Marco Carbone
气球类型：控制数据类型中的状态共享
DOI：
10.1007/bfb0053373
发表时间：
1997
期刊：
Software: Practice and Experience
影响因子：
--
作者：
Paulo Sérgio Almeida
通讯作者：
Paulo Sérgio Almeida
所有权、唯一性和不变性
DOI：
--
发表时间：
2008
期刊：
International Conference on Software Technology: Methods and Tools
影响因子：
--
作者：
Johan Östlund;Tobias Wrigstad;D. Clarke;Beatrice Åkerblom
通讯作者：
Beatrice Åkerblom