Being and Change: Reasoning About Invariance

Frank S. de Boer, Stijn de Gouw

Research output: Chapter in Book/Report/Conference proceedingConference article in proceedingAcademicpeer-review

Abstract

We introduce a new way of reasoning about invariance in terms of foot-prints in a Hoare logic for recursive programs with (unbounded) arrays. A foot-print of a statement is a predicate that describes that part of the state that can be changed by the statement. We define invariance of an assertion with respect to a foot-print by means of a logical operation. This new Hoare logic is applied in a new simpler and modular proof of correctness of the well-known Quicksort sorting algorithm.
Original languageEnglish
Title of host publicationCorrect System Design
Subtitle of host publicationSymposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015, Proceedings
EditorsRoland Meyer , André Platzer , Heike Wehrheim
Place of PublicationCham
PublisherSpringer
Pages191-204
Number of pages14
Edition1
ISBN (Electronic)978-3-319-23506-6
ISBN (Print)978-3-319-23505-9
DOIs
Publication statusPublished - 2015
Externally publishedYes

Publication series

SeriesLecture Notes in Computer Science
Volume9360
ISSN0302-9743

Fingerprint Dive into the research topics of 'Being and Change: Reasoning About Invariance'. Together they form a unique fingerprint.

  • Cite this

    Boer, F. S. D., & Gouw, S. D. (2015). Being and Change: Reasoning About Invariance. In R. M., A. P., & H. W. (Eds.), Correct System Design: Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015, Proceedings (1 ed., pp. 191-204). Springer. Lecture Notes in Computer Science, Vol.. 9360 https://doi.org/10.1007/978-3-319-23506-6_13