Proof systems for partial incorrectness logic (partial reverse Hoare logic)
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866916635307147264 |
|---|---|
| author | Oda, Yukihiro |
| author_facet | Oda, Yukihiro |
| contents | Partial incorrectness logic (partial reverse Hoare logic) has recently been introduced as a new Hoare-style logic that over-approximates the weakest pre-conditions of a program and a post-condition. It is expected to verify systems where the final state must guarantee its initial state, such as authentication, secure communication tools and digital signatures. However, the logic has only been given semantics. This paper defines two proof systems for partial incorrectness logic (partial reverse Hoare logic): ordinary and cyclic proof systems. They are sound and relatively complete. The relative completeness of our ordinary proof system is proved by showing that the weakest pre-condition of a while loop and a post-condition is its loop invariant. The relative completeness of our cyclic proof system is also proved by providing a way to transform any cyclic proof into an ordinary proof. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_21053 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Proof systems for partial incorrectness logic (partial reverse Hoare logic) Oda, Yukihiro Logic in Computer Science Programming Languages Partial incorrectness logic (partial reverse Hoare logic) has recently been introduced as a new Hoare-style logic that over-approximates the weakest pre-conditions of a program and a post-condition. It is expected to verify systems where the final state must guarantee its initial state, such as authentication, secure communication tools and digital signatures. However, the logic has only been given semantics. This paper defines two proof systems for partial incorrectness logic (partial reverse Hoare logic): ordinary and cyclic proof systems. They are sound and relatively complete. The relative completeness of our ordinary proof system is proved by showing that the weakest pre-condition of a while loop and a post-condition is its loop invariant. The relative completeness of our cyclic proof system is also proved by providing a way to transform any cyclic proof into an ordinary proof. |
| title | Proof systems for partial incorrectness logic (partial reverse Hoare logic) |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2502.21053 |