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

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

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.