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.

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