Aliasing Control in an Object-Oriented Programming Language with Typestate Annotations

使用类型状态注释的面向对象编程语言中的别名控制

• 批准号: 2469547
• 金额: --
• 依托单位: University of Glasgow
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2020
• 资助国家: 英国
• 起止时间: 2020 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2469547
• 关键词: Aliasing; Control; Object; Oriented; Programming

When writing stateful programs, an order of operation is often expected, even though the order itself is only informally denied, if denied at all. We call the order of operations a protocol. For small protocols, an informal specification may be manageable for the programmer to navigate. However, as the protocols become increasingly complex, it can become difficult for the programmer to ensure that operations are performed in the correct order. Multiple approaches have been proposed to integrate such protocols into programming languages, typestates being a key one. While a type describes all available operations allowed on data of that type, a typestate takes into consideration the context of the operations, hence only allows a subset of all operations, for a given point in the program. We can view the typestate of an object as a state machine for that particular object, where each state has a distinct set of operations available. A related problem to protocol checking is that of ensuring correct communication between processes. For this problem, which has been studied extensively, we employ session types to describe the types of data that will be sent through communication channels. Although session types were originally defined for small calculi, such as the pi-calculus, session types have also been applied to other settings. One such example is the introduction of channels and session types to an object oriented programming language, where a global session type is defined for a class, and the logic for conforming to the session type could be distributed over multiple methods. As a result of the relation between the two problems, the amalgamation of session types and typestate declarations for object oriented programming languages was studied by Dardha and co-authors and resulted in the tools Mungo and StMungo. In Mungo, a Java class is annotated with a typestate declaration, denoting the available set of method calls during the lifetime of the object. As Mungo employ typestate tracking, aliasing of objects must be controlled, to track where an object is updated. Mungo employs a linear typing approach, where only a single reference to an object is available at a given time. This is a common approach to typing communication and is often seen for session types and typestate based languages. The reasoning for enforcing linearity is that when we are working with behavioral types, we expect them to evolve during the lifetime of an object. In Mungo, for example, we expect the typestate of an object to be changed after performing a method call. If we allow unlimited aliasing of object references, changes performed by one alias are not reflected at the other aliases, even if the underlying object has changed. Linear typing sidesteps the issue, by not allowing these aliases to coexist. While such a restriction makes reasoning about types easier, it is very inflexible to program in an object-oriented language that disallows aliasing. During his PhD, Mathias will explore the linearity constraints in the Mungo formal framework and tool implementation, with the aim of relaxing these constraints for more expressive programming with typestates while still preserving the desired soundness and safety properties. The proposed methodology for loosening linearity constraints is alias control. To further the relevance and robustness of Mungo, his PhD also will focus on typestate inference (not present in Mungo so far) as well as the integration of Mungo with mainstream IDEs, making Mungo an applicable and industry-ready tool.

在编写有状态程序时，通常需要一个操作顺序，即使该顺序本身只是非正式地拒绝（如果根本拒绝的话）。我们将操作顺序称为协议。对于小型协议，程序员可以管理非正式的规范来导航。然而，随着协议变得越来越复杂，程序员可能很难确保以正确的顺序执行操作。人们已经提出了多种方法将此类协议集成到编程语言中，其中类型状态是关键之一。虽然类型描述了对该类型的数据允许的所有可用操作，但类型状态考虑了操作的上下文，因此对于程序中的给定点仅允许所有操作的子集。我们可以将对象的类型状态视为该特定对象的状态机，其中每个状态都有一组不同的可用操作。与协议检查相关的一个问题是确保进程之间的正确通信。对于这个已经被广泛研究的问题，我们使用会话类型来描述将通过通信通道发送的数据类型。尽管会话类型最初是为小型演算（例如 pi 演算）定义的，但会话类型也已应用于其他设置。一个这样的示例是将通道和会话类型引入面向对象的编程语言，其中为类定义全局会话类型，并且用于符合会话类型的逻辑可以分布在多个方法上。由于这两个问题之间的关系，Dardha 和合著者研究了面向对象编程语言的会话类型和类型状态声明的合并，并产生了工具 Mungo 和 StMungo。在 Mungo 中，Java 类用类型状态声明进行注释，表示对象生命周期内可用的方法调用集。由于 Mungo 采用类型状态跟踪，因此必须控制对象的别名，以跟踪对象的更新位置。 Mungo 采用线性类型方法，在给定时间只有一个对象引用可用。这是打字通信的常见方法，通常用于会话类型和基于类型状态的语言。强制线性的原因是，当我们处理行为类型时，我们期望它们在对象的生命周期中不断发展。例如，在 Mungo 中，我们期望在执行方法调用后更改对象的类型状态。如果我们允许对对象引用进行无限制的别名，则一个别名执行的更改不会反映在其他别名上，即使底层对象已更改。线性类型通过不允许这些别名共存来回避这个问题。虽然这样的限制使类型推理变得更容易，但使用不允许使用别名的面向对象语言进行编程非常不灵活。在攻读博士学位期间，Mathias 将探索 Mungo 形式框架和工具实现中的线性约束，目的是放宽这些约束，以便使用类型状态进行更具表现力的编程，同时仍然保留所需的健全性和安全属性。所提出的放松线性约束的方法是混叠控制。为了进一步提高 Mungo 的相关性和鲁棒性，他的博士学位还将专注于类型状态推断（Mungo 中尚未出现）以及 Mungo 与主流 IDE 的集成，使 Mungo 成为适用且适合行业的工具。