VeriFly：通过增量的动态断言检查
VeriFly: On-the-fly Assertion Checking via Incrementality
摘要：
断言检查是程序员的一个非常宝贵的工具，它可以在动态语言（如Prolog）中发现许多类错误或验证它们的存在。对于Prolog程序员来说，这意味着能够拥有相关的属性，如模式，类型，确定性，非故障，共享，约束，成本等，检查并标记错误，而无需实际运行程序。这样的全局静态分析工具在软件开发周期中越早使用就越有用，并且快速的响应时间对于交互式使用是必不可少的。每次进行更改时，都要对软件项目进行全面而精确的语义分析，这可能会非常昂贵。在我们的静态分析和验证框架中，通过模块化和增量（上下文和路径敏感）分析的组合来解决这一挑战，该分析响应于不同粒度级别的程序编辑。我们描述了如何在一个集成开发环境（IDE）中的框架的组合，利用这种增量，以实现高水平的反应时，反映分析和验证结果的着色和工具提示直接在程序文本-该工具的VeriFly模式。我们所描述的具体实现是基于Emacs的，并且部分地重用了现成的“动态”语法检查工具（flycheck）。我们相信，类似的扩展也可以在其他成熟的开发环境中以较低的工作量进行复制。我们使用该工具的初步经验显示出非常有希望的结果，具有低延迟时间，在开发过程中为程序员提供早期，连续和精确的断言检查和其他语义反馈。该工具支持Prolog本地，以及其他语言的语义转换成霍恩子句。本文件正在考虑被TPLP接受。
英文摘要：
Assertion checking is an invaluable programmer's tool for finding many classes of errors or verifying their absence in dynamic languages such as Prolog. For Prolog programmers this means being able to have relevant properties such as modes, types, determinacy, non-failure, sharing, constraints, cost, etc., checked and errors flagged without having to actually run the program. Such global static analysis tools are arguably most useful the earlier they are used in the software development cycle, and fast response times are essential for interactive use. Triggering a full and precise semantic analysis of a software project every time a change is made can be prohibitively expensive. In our static analysis and verification framework this challenge is addressed through a combination of modular and incremental (context- and path-sensitive) analysis that is responsive to program edits, at different levels of granularity. We describe how the combination of this framework within an integrated development environment (IDE) takes advantage of such incrementality to achieve a high level of reactivity when reflecting analysis and verification results back as colorings and tooltips directly on the program text -- the tool's VeriFly mode. The concrete implementation that we describe is Emacs-based and reuses in part off-the-shelf "on-the-fly" syntax checking facilities (flycheck). We believe that similar extensions are also reproducible with low effort in other mature development environments. Our initial experience with the tool shows quite promising results, with low latency times that provide early, continuous, and precise assertion checking and other semantic feedback to programmers during the development process. The tool supports Prolog natively, as well as other languages by semantic transformation into Horn clauses. This paper is under consideration for acceptance in TPLP.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
