Foundations of Typestate-Oriented Programming
Foundations of Typestate-Oriented Programming
复制标题
DOI：
10.1145/2629609
复制
发表时间：
2014-10-01
影响因子：
1.3
通讯作者：
Aldrich, Jonathan
中科院分区：
文献类型：
--
作者：
Garcia, Ronald;Tanter, Eric;Aldrich, Jonathan
Typestate反映了命令式对象上的法律的操作在运行时如何随着其内部状态的改变而改变。例如，一个类型状态检查器可以静态地确保一个对象方法只在对象处于一个操作定义良好的状态时被调用。先前的工作已经展示了如何通过访问权限和状态保证来实现模块化的类型状态检查。然而，typestate并没有被当作一个基本的语言概念：typestate检查器是现有语言之上的一个额外的验证层。相反，面向类型状态的编程（TSOP）语言直接支持表达类型状态。例如，在Plaid编程语言中，对象的类型状态直接对应于其类，并且该类可以动态更改。Plaid对象不仅具有依赖于类型状态的接口，而且具有依赖于类型状态的行为和运行时表示。本文通过形式化一个具有可变状态的名义型面向对象语言，将类型状态更改和类型状态检查作为基本概念集成，为TSOP奠定了基础。我们首先描述了一个静态类型的语言-Featherweight Typestate（FT）-对象引用的类型增加了访问权限和状态保证。我们描述了一种新的流量敏感的基于许可的类型系统的FT。由于静态类型状态检查对于某些应用程序来说仍然过于严格，我们将这种语言扩展为渐进类型化语言-渐进式轻量级类型状态（GFT）。这种语言扩展了渐进式类型的概念，以考虑类型状态：渐进式类型状态检查通过自动将运行时检查插入到程序中，无缝地结合了静态和动态检查。GFT的渐进类型系统允许程序员编写动态安全的代码，即使静态类型检查器只能部分验证它。3.1【编程语言】：形式定义和理论-语义学; D.3.3 [程序设计语言]：语言构造和语法-类型状态; D.2.10 [软件工程]：设计-表示
Typestate reflects how the legal operations on imperative objects can change at runtime as their internal state changes. A typestate checker can statically ensure, for instance, that an object method is only called when the object is in a state for which the operation is well defined. Prior work has shown how modular typestate checking can be achieved thanks to access permissions and state guarantees. However, typestate was not treated as a primitive language concept: typestate checkers are an additional verification layer on top of an existing language. In contrast, a typestate-oriented programming (TSOP) language directly supports expressing typestates. For example, in the Plaid programming language, the typestate of an object directly corresponds to its class, and that class can change dynamically. Plaid objects have not only typestate-dependent interfaces but also typestate-dependent behaviors and runtime representations.This article lays foundations for TSOP by formalizing a nominal object-oriented language with mutable state that integrates typestate change and typestate checking as primitive concepts. We first describe a statically typed language-Featherweight Typestate (FT)-where the types of object references are augmented with access permissions and state guarantees. We describe a novel flow-sensitive permission-based type system for FT. Because static typestate checking is still too rigid for some applications, we then extend this language into a gradually typed language-Gradual Featherweight Typestate (GFT). This language extends the notion of gradual typing to account for typestate: gradual typestate checking seamlessly combines static and dynamic checking by automatically inserting runtime checks into programs. The gradual type system of GFT allows programmers to write dynamically safe code even when the static type checker can only partly verify it.Categories and Subject Descriptors: D. 3.1 [Programming Languages]: Formal Definitions and Theory-Semantics; D.3.3 [Programming Languages]: Language Constructs and Features-Typestate; D.2.10 [Software Engineering]: Design-Representation