Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Modular Verification of Recursive Programs
| |
|
Modular Verification of Recursive Programs
Krzysztof R. Apt20, 21, Frank S. de Boer20, 22 and Ernst-Rüdiger Olderog23
| (20) |
Centre for Mathematics and Computer Science (CWI), Amsterdam, The Netherlands |
| (21) |
Institute of Language, Logic and Computation, University of Amsterdam, Amsterdam, |
| (22) |
Leiden Institute of Advanced Computer Science, University of Leiden, The Netherlands |
| (23) |
Department of Computing Science, University of Oldenburg, Germany |
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.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|