Modular verification of recursive programs

Authors
Publication date 2009
Host editors
  • O. Grumberg
  • M. Kaminski
  • S. Katz
  • S. Wintner
Book title Languages: from formal to natural: Essays dedicated to Nissim Francez on the occasion of his 65th birthday
ISBN
  • 9783642017476
Series Lecture notes in computer science, 5533
Pages (from-to) 1-21
Number of pages 244
Publisher Berlin: Springer
Organisations
  • Interfacultary Research - Institute for Logic, Language and Computation (ILLC)
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
Permalink to this page
Back