Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915334051594240 |
|---|---|
| author | Zilberstein, Noam |
| author_facet | Zilberstein, Noam |
| contents | Starting with Hoare Logic over 50 years ago, numerous program logics have been devised to reason about the diverse programs encountered in the real world. This includes reasoning about computational effects, particularly those effects that cause the program execution to branch into multiple paths due to, e.g., nondeterministic or probabilistic choice.
The recently introduced Outcome Logic reimagines Hoare Logic with branching at its core, using an algebraic representation of choice to capture programs that branch into many outcomes. In this article, we expand on prior Outcome Logic papers in order to give a more authoritative and comprehensive account of the metatheory. This includes a relatively complete proof system for Outcome Logic with the ability to reason about general purpose looping. We also show that this proof system applies to programs with various types of branching and that it facilitates the reuse of proof fragments across different kinds of specifications. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_04594 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects Zilberstein, Noam Logic in Computer Science Programming Languages Starting with Hoare Logic over 50 years ago, numerous program logics have been devised to reason about the diverse programs encountered in the real world. This includes reasoning about computational effects, particularly those effects that cause the program execution to branch into multiple paths due to, e.g., nondeterministic or probabilistic choice. The recently introduced Outcome Logic reimagines Hoare Logic with branching at its core, using an algebraic representation of choice to capture programs that branch into many outcomes. In this article, we expand on prior Outcome Logic papers in order to give a more authoritative and comprehensive account of the metatheory. This includes a relatively complete proof system for Outcome Logic with the ability to reason about general purpose looping. We also show that this proof system applies to programs with various types of branching and that it facilitates the reuse of proof fragments across different kinds of specifications. |
| title | Outcome Logic: A Unified Approach to the Metatheory of Program Logics with Branching Effects |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2401.04594 |