An Expressive Trace Logic for Recursive Programs
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916489152430080 |
|---|---|
| author | Gurov, Dilian Hähnle, Reiner |
| author_facet | Gurov, Dilian Hähnle, Reiner |
| contents | We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed-points, for precise specification of programs with recursive procedures. Both, programs and trace formulas, are equipped with a direct-style, fully compositional, denotational semantics that on programs coincides with the standard SOS of recursive programs. We design a compositional proof calculus for proving finite-trace program properties, and prove soundness as well as (relative) completeness. We show that each program can be mapped to a semantics-preserving trace formula and, vice versa, each trace formula can be mapped to a canonical program over slightly extended programs, resulting in a Galois connection between programs and formulas. Our results shed light on the correspondence between programming constructs and logical connectives. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_13125 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | An Expressive Trace Logic for Recursive Programs Gurov, Dilian Hähnle, Reiner Logic in Computer Science Software Engineering 68Q55 (Primary) 03B45 (Secondary) F.3.2; F.3.1; F.4.1 We present an expressive logic over trace formulas, based on binary state predicates, chop, and least fixed-points, for precise specification of programs with recursive procedures. Both, programs and trace formulas, are equipped with a direct-style, fully compositional, denotational semantics that on programs coincides with the standard SOS of recursive programs. We design a compositional proof calculus for proving finite-trace program properties, and prove soundness as well as (relative) completeness. We show that each program can be mapped to a semantics-preserving trace formula and, vice versa, each trace formula can be mapped to a canonical program over slightly extended programs, resulting in a Galois connection between programs and formulas. Our results shed light on the correspondence between programming constructs and logical connectives. |
| title | An Expressive Trace Logic for Recursive Programs |
| topic | Logic in Computer Science Software Engineering 68Q55 (Primary) 03B45 (Secondary) F.3.2; F.3.1; F.4.1 |
| url | https://arxiv.org/abs/2411.13125 |