首页> 外文会议>Principles of programming languages >Modular Session Types for Distributed Object-Oriented Programming
【24h】

Modular Session Types for Distributed Object-Oriented Programming

机译:分布式面向对象编程的模块化会话类型

获取原文
获取原文并翻译 | 示例

摘要

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 be modularized, 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.
机译:会话类型允许从理论上指定通信协议的类型,以便可以通过静态类型检查来验证协议的实现。我们以三种方式扩展了有关分布式面向对象语言的会话类型的先前工作。 (1)我们将会话类型附加到类定义中,以指定方法调用的可能顺序。 (2)我们允许对会话类型(协议)实现进行模块化,即划分为可单独调用的方法。 (3)我们将会话类型的通信通道视为对象,将其会话类型与类的会话类型集成在一起。结果是通信通道及其会话类型,分布式面向对象的编程以及支持非统一对象(即动态更改可用方法集的对象)的一种类型状态的优雅统一。我们为基于分布式类的小型面向对象语言定义语法,操作语义,声音类型系统以及正确而完整的类型检查算法。静态类型保证通道上的消息序列和对象上的方法调用序列都符合类型理论规范,从而确保类型安全。该语言包括会话类型的预期功能(例如委派)和面向对象编程的预期功能(例如本地状态的封装)。我们还将原型实现描述为Java的扩展。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号