Modular verification of recursive programs
| Authors |
|
|---|---|
| Publication date | 2009 |
| Host editors |
|
| Book title | Languages: from formal to natural: Essays dedicated to Nissim Francez on the occasion of his 65th birthday |
| ISBN |
|
| Series | Lecture notes in computer science, 5533 |
| Pages (from-to) | 1-21 |
| Number of pages | 244 |
| Publisher | Berlin: Springer |
| Organisations |
|
| 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. |
| Document type | Chapter |
| Published at |
https://doi.org/10.1007/978-3-642-01748-3_1
(Final published version)
|
| Permalink to this page | |