Reasoning about call-by-value: a missing result in the history of Hoare's logic
Logic in Computer Science
2019-09-16 v1 Programming Languages
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.
Cite
@article{arxiv.1909.06215,
title = {Reasoning about call-by-value: a missing result in the history of Hoare's logic},
author = {Krzysztof R. Apt and Frank S. de Boer},
journal= {arXiv preprint arXiv:1909.06215},
year = {2019}
}
Comments
28 pages