Reasoning about call-by-value: a missing result in the history of Hoare's logic

2019/09/13 by Krzysztof R. Apt, Apt, Krzysztof R., Frank S. de Boer +1
Computer Science · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Formal Methods in Verification

paper · pdf · doi:10.48550/arxiv.1909.06215

Abstract

We provide a sound and relatively complete Hoare-like proof system 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 are linear in the length of the program. We argue that in spite of the fact that Hoare-like proof systems for recursive procedures were intensively studied, no such proof system has been proposed in the literature.

Cited by

• Fifty years of Hoare's Logic

Related

• Modular Verification of Recursive Programs
• Scope Logic with Local Reasoning and Pre/Post-State Properties
• Partial Incorrectness Logic
• Open Call-by-Value (Extended Version)
• Proof systems for partial incorrectness logic (partial reverse Hoare logic)