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

NameLecture Notes in Computer Science
PublisherSpringer
Volume9360
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Invariance
Sorting

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). (Lecture Notes in Computer Science; Vol. 9360). Cham: Springer. https://doi.org/10.1007/978-3-319-23506-6_13
Boer, Frank S. de ; Gouw, Stijn de. / Being and Change : Reasoning About Invariance. 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. editor / Roland Meyer ; André Platzer ; Heike Wehrheim. 1. ed. Cham : Springer, 2015. pp. 191-204 (Lecture Notes in Computer Science).
@inproceedings{86e6cc4919b4477c966aec4dfccfbfd7,
title = "Being and Change: Reasoning About Invariance",
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.",
author = "Boer, {Frank S. de} and Gouw, {Stijn de}",
year = "2015",
doi = "10.1007/978-3-319-23506-6_13",
language = "English",
isbn = "978-3-319-23505-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "191--204",
editor = "{Roland Meyer} and {Andr{\'e} Platzer} and {Heike Wehrheim}",
booktitle = "Correct System Design",
edition = "1",

}

Boer, FSD & Gouw, SD 2015, Being and Change: Reasoning About Invariance. in RM, AP & HW (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 edn, Lecture Notes in Computer Science, vol. 9360, Springer, Cham, pp. 191-204. https://doi.org/10.1007/978-3-319-23506-6_13

Being and Change : Reasoning About Invariance. / Boer, Frank S. de; Gouw, Stijn de.

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. ed. / Roland Meyer; André Platzer; Heike Wehrheim. 1. ed. Cham : Springer, 2015. p. 191-204 (Lecture Notes in Computer Science; Vol. 9360).

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

TY - GEN

T1 - Being and Change

T2 - Reasoning About Invariance

AU - Boer, Frank S. de

AU - Gouw, Stijn de

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

UR - https://link.springer.com/book/10.1007/978-3-319-23506-6

U2 - 10.1007/978-3-319-23506-6_13

DO - 10.1007/978-3-319-23506-6_13

M3 - Conference article in proceeding

SN - 978-3-319-23505-9

T3 - Lecture Notes in Computer Science

SP - 191

EP - 204

BT - Correct System Design

A2 - , Roland Meyer

A2 - , André Platzer

A2 - , Heike Wehrheim

PB - Springer

CY - Cham

ER -

Boer FSD, Gouw SD. Being and Change: Reasoning About Invariance. In RM, AP, HW, editors, 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. Cham: Springer. 2015. p. 191-204. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-23506-6_13