抽象逻辑：上下文精化与分离逻辑的结合
编程语言
2021-09-08 v1
摘要
上下文精化与分离逻辑是性质迥异且均成功的验证技术。首先，前者保证具体程序与抽象程序间的行为精化，而后者在特定条件（以前置与后置条件表述）下保证具体程序的安全性。其次，前者在局部推理模块时不允许关于上下文的任何假设，而后者允许丰富的假设。本文提出一种称为抽象逻辑（AL）的新验证技术，它内在地结合了上下文精化与诸如 Iris 和 VST 的分离逻辑，从而兼取两者之长。具体而言，AL 允许我们在关于外部模块的分离逻辑式前后置条件下，针对抽象模块局部验证具体模块。AL 在 Coq 中完全形式化，并提供一种证明模式，支持使用我们自有策略的模拟式推理与使用 IPM（Iris Proof Mode）的 SL 式推理之结合。利用该证明模式，我们验证了多种示例以展示关于所有权（基于偏交换幺半群）与纯性（即无系统调用地终止）的推理、关于互递归与函数指针的循环与高阶推理，以及通过中间抽象的可复用与渐进式验证。此外，验证结果结合 CompCert，从而我们正式确立了从顶层抽象程序直至其汇编代码的行为精化。
引用
@article{arxiv.2109.02991,
title = {Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic},
author = {Youngju Song and Minki Cho and Dongjae Lee and Chung-Kil Hur},
journal= {arXiv preprint arXiv:2109.02991},
year = {2021}
}