Modular Verification of Recursive Programs
Logic in Computer Science
2009-07-27 v1 Programming Languages
Abstract
We argue that verification of recursive programs by means of the assertional method of C.A.R. Hoare can be conceptually simplified using a modular reasoning. In this approach some properties of the program are established first and subsequently used to establish other program properties. We illustrate this approach by providing a modular correctness proof of the Quicksort program.
Keywords
Cite
@article{arxiv.0907.4316,
title = {Modular Verification of Recursive Programs},
author = {Krzysztof R. Apt and Frank S. de Boer and Ernst-Rüdiger Olderog},
journal= {arXiv preprint arXiv:0907.4316},
year = {2009}
}
Comments
21 pages. appeared in: Languages: From Formal to Natural, Essays Dedicated to Nissim Francez on the Occasion of His 65th Birthday. Lecture Notes in Computer Science 5533 Springer 2009