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.

, , , ,
doi.org/10.1145/3477143
ACM Transactions on Programming Languages and Systems
Centrum Wiskunde & Informatica, Amsterdam, The Netherlands

de Boer, F.S, & Hiep, H.A. (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