Partial Incorrectness Logic
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913700737187840 |
|---|---|
| author | Verscht, Lena Wáng, Ānrán Kaminski, Benjamin Lucien |
| author_facet | Verscht, Lena Wáng, Ānrán Kaminski, Benjamin Lucien |
| contents | Reasoning about program correctness has been a central topic in static analysis for many years, with Hoare logic (HL) playing an important role. The key notions in HL are partial and total correctness. Both require that program executions starting in a specified set of initial states (the precondition) reach a designated set of final states (the postcondition). Partial correctness is more lenient in that it does not require termination, effectively deeming divergence acceptable. We explore partial incorrectness logic, which stands in relation to O'Hearn's "total" incorrectness logic as partial correctness does to total correctness: Partial correctness allows divergence, partial incorrectness allows unreachability. While the duality between divergence and unreachability may not be immediately apparent, we explore this relationship further. Our chosen formalism is predicate transformers à la Dijkstra. We focus here on deterministic and reversible programs, though the discussion extends to nondeterministic and irreversible computations, both of which introduce additional nondeterminism that must be addressed. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_14626 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Partial Incorrectness Logic Verscht, Lena Wáng, Ānrán Kaminski, Benjamin Lucien Logic in Computer Science Programming Languages Reasoning about program correctness has been a central topic in static analysis for many years, with Hoare logic (HL) playing an important role. The key notions in HL are partial and total correctness. Both require that program executions starting in a specified set of initial states (the precondition) reach a designated set of final states (the postcondition). Partial correctness is more lenient in that it does not require termination, effectively deeming divergence acceptable. We explore partial incorrectness logic, which stands in relation to O'Hearn's "total" incorrectness logic as partial correctness does to total correctness: Partial correctness allows divergence, partial incorrectness allows unreachability. While the duality between divergence and unreachability may not be immediately apparent, we explore this relationship further. Our chosen formalism is predicate transformers à la Dijkstra. We focus here on deterministic and reversible programs, though the discussion extends to nondeterministic and irreversible computations, both of which introduce additional nondeterminism that must be addressed. |
| title | Partial Incorrectness Logic |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2502.14626 |