2021-10-31
Completeness and complexity of reasoning about call-by-value in Hoare logic
Publication
Publication
ACM Transactions on Programming Languages and Systems , Volume 43 - Issue 4 p. 17:1- 17:35
We provide a sound and relatively complete Hoare logic for reasoning about partial correctness of recursive procedures in presence of local variables and the call-by-value parameter mechanism and in which the correctness proofs support contracts and are linear in the length of the program. We argue that in spite of the fact that Hoare logics for recursive procedures were intensively studied, no such logic has been proposed in the literature.
| Additional Metadata | |
|---|---|
| , , , , | |
| doi.org/10.1145/3477143 | |
| ACM Transactions on Programming Languages and Systems | |
| Organisation | Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands |
|
de Boer, F., & Hiep, H.-D. (2021). Completeness and complexity of reasoning about call-by-value in Hoare logic. ACM Transactions on Programming Languages and Systems, 43(4), 17:1–17:35. doi:10.1145/3477143 |
|
