一个 HAT 技巧：使用符号有限自动机自动验证表示不变式
A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata
AI总结：
本文提出使用符号有限自动机（SFA）结合精化类型系统，实现 Hoare Automata Types (HATs) 以自动验证依赖有状态库的数据结构表示不变式，并开发了双向类型检查算法将其转化为 SMT 可验证形式。
摘要：
函数式程序通常与将状态隐藏在类型抽象背后的有状态库进行交互。一类特别重要的应用是数据结构实现，它们依赖此类库来提供原本可能难以实现的效率和可扩展性。然而，由于这些库提供的方法规范必然是通用的，且很少专门针对任何特定客户端的需求进行定制，因此任何必需的应用级不变式通常必须表示为对库所维护的（通常）不透明状态的附加约束。在本文中，我们考虑使用符号有限自动机（SFA）来规范和验证此类表示不变式。我们表明，SFA 可用于简洁且精确地捕获函数式客户端与有状态库之间交互的细粒度时间与数据依赖历史。为了促进模块化和组合式推理，我们将 SFA 集成到精化类型系统中，以限定由此类交互产生的有状态计算。我们考虑的特定实例化是 Hoare Automata Types (HATs)，它允许我们规范并自动类型检查数据类型的表示不变式，即使其实现依赖于操作隐藏状态的有状态库方法。我们还开发了一种新的双向类型检查算法，该算法实现了对 HAT 的高效子类型包含检查，从而使其能够转换为适合基于 SMT 的自动验证的形式。我们展示了该算法实现的广泛实验结果，证明了类型检查复杂且高级的 HAT 规范的 OCaml 数据结构实现的可行性。
英文摘要：
Functional programs typically interact with stateful libraries that hide state behind typed abstractions. One particularly important class of applications are data structure implementations that rely on such libraries to provide a level of efficiency and scalability that may be otherwise difficult to achieve. However, because the specifications of the methods provided by these libraries are necessarily general and rarely specialized to the needs of any specific client, any required application-level invariants must often be expressed in terms of additional constraints on the (often) opaque state maintained by the library. In this paper, we consider the specification and verification of such representation invariants using symbolic finite automata (SFA). We show that SFAs can be used to succinctly and precisely capture fine-grained temporal and data-dependent histories of interactions between functional clients and stateful libraries. To facilitate modular and compositional reasoning, we integrate SFAs into a refinement type system to qualify stateful computations resulting from such interactions. The particular instantiation we consider, Hoare Automata Types (HATs), allows us to both specify and automatically type-check the representation invariants of a datatype, even when its implementation depends on stateful library methods that operate over hidden state. We also develop a new bidirectional type checking algorithm that implements an efficient subtyping inclusion check over HATs, enabling their translation into a form amenable for SMT-based automated verification. We present extensive experimental results on an implementation of this algorithm that demonstrates the feasibility of type-checking complex and sophisticated HAT-specified OCaml data structure implementations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
