Java 无穷迹属性的类型强制执行
计算机科学中的逻辑
2022-09-09 v1 编程语言
摘要
提高软件质量的一种常见方法是使用编程指南来避免常见类型的错误。在本文中，我们考虑了针对 Featherweight Java (FJ) 强制执行指南的问题。我们将指南形式化为有限或无限执行迹的集合，并为 FJ 开发了一个基于区域的类型与效应系统，该系统可以强制执行此类指南。我们建立在 Erbatur、Hofmann 和 Z\u{a}linescu 的工作之上，他们提出了一个类型系统，用于验证终止 FJ 程序的有限事件迹。我们改进了该类型系统，将区域类型与 FJ 类型分离，并使用 Hofmann 和 Chen 的思想将其扩展，以捕获由非终止程序产生的无限迹。我们的类型与效应系统可以表达有限和无限迹的属性，并能计算关于 FJ 程序可能的无限迹的信息。具体而言，方法的无限迹集合被构造为计算方法体可能迹的算子的最大不动点。我们的类型推断算法通过使用基于 B"uchi 自动机的系统有限抽象来实现。
引用
@article{arxiv.2107.11280,
title = {Type-based Enforcement of Infinitary Trace Properties for Java},
author = {Serdar Erbatur and Ulrich Schöpp and Chuangjie Xu},
journal= {arXiv preprint arXiv:2107.11280},
year = {2022}
}
备注
main part (14 pages) published at PPDP'21; arXiv version contains an appendix on the FJ operational semantics and the extension to support exception handling (15 pages total)