Gradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
Conrad Zimmerman, Jenna DiVincenzo
TL;DR
This work addresses unifying verification and bug-finding by introducing Gradual Verification (GV) and a novel Gradual Exact Logic (ẼL). It formalizes exact logic (EL) as the intersection of Hoare logic (HL) and incorrectness logic (IL), and shows how GV serves as a unifying framework that subsumes both OX and UX deductions. The authors establish precise correspondences: HL and IL can be recovered via ẼL, and GV corresponds to IL on imprecise specifications while also encompassing HL; ẼL provides the bridge among HL, IL, and GV. They also discuss practical implications for toolchains and outline caveats, such as language limitations and the static nature of the current GV model, with future work aimed at extending language features and incorporating runtime aspects. Overall, the paper provides a formal pathway to transfer techniques across static verification, gradual verification, and bug-finding techniques.
Abstract
Previously, gradual verification has been developed using overapproximating logics such as Hoare logic. We show that the static verification component of gradual verification is also connected to underapproximating logics like incorrectness logic. To do this, we use a novel definition of gradual verification and a novel gradualization of exact logic [Maksimovic et al. 2023] which we call gradual exact logic. Further, we show that Hoare logic, incorrectness logic, and gradual verification can be defined in terms of gradual exact logic. We hope that this connection can be used to develop tools and techniques that apply to both gradual verification and bug-finding. For example, we envision that techniques defined in terms of exact logic can be directly applied to verification, bug-finding, and gradual verification, using the principles of gradual typing [Garcia et al. 2016].