结果逻辑：统一处理具有分支效应的程序逻辑元理论
计算机科学中的逻辑
2025-06-11 v3 编程语言
摘要
自50多年前的Hoare逻辑开始，人们设计了众多程序逻辑来推理现实世界中遇到的各种程序。这包括对计算效应的推理，特别是那些因非确定性或概率选择等原因导致程序执行分支为多条路径的效应。最近引入的结果逻辑（Outcome Logic）以分支为核心重新构想了Hoare逻辑，使用选择的代数表示来捕获分支为多个结果的程序。在本文中，我们扩展了先前的结果逻辑论文，以给出更权威和全面的元理论阐述。这包括一个相对完备的结果逻辑证明系统，能够推理通用循环。我们还展示了该证明系统适用于具有各种分支类型的程序，并且有助于在不同类型的规约之间复用证明片段。
引用
@article{arxiv.2401.04594,
title = {Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects},
author = {Noam Zilberstein},
journal= {arXiv preprint arXiv:2401.04594},
year = {2025}
}