渐进精确逻辑：通过渐进验证统一霍尔逻辑与错误逻辑
计算机科学中的逻辑
2024-12-03 v1 编程语言
摘要
以前，渐进验证使用过逼近逻辑（如霍尔逻辑）进行开发。我们展示了渐进验证的静态验证组成部分也与过逼近逻辑（如错误逻辑）相关。为此，我们采用一种新颖的渐进验证定义和一种新颖的渐进化精确逻辑 [Maksimovic 等 2023]，称为渐进精确逻辑。进一步，我们展示了霍尔逻辑、错误逻辑和渐进验证都可以用渐进精确逻辑来定义。我们希望这一联系可以用于开发适用于渐进验证和错误查找的工具和技术。例如，我们设想，基于精确逻辑定义的技术可以直接应用于验证、错误查找和渐进验证，运用渐进类型原则 [Garcia 等 2016]。
引用
@article{arxiv.2412.00339,
title = {Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification},
author = {Conrad Zimmerman and Jenna DiVincenzo},
journal= {arXiv preprint arXiv:2412.00339},
year = {2024}
}
备注
For presentation at the 1st Workshop on the Theory and Practice of Static Analysis (TPSA 2025)