Being and Change: Reasoning About Invariance

Frank S. de Boer; Stijn de Gouw

doi:10.1007/978-3-319-23506-6_13

Being and Change: Reasoning About Invariance

Research output: Chapter in Book/Report/Conference proceeding › Conference article in proceeding › Academic › peer-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 language	English
Title of host publication	Correct System Design
Subtitle of host publication	Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015, Proceedings
Editors	Roland Meyer , André Platzer , Heike Wehrheim
Place of Publication	Cham
Publisher	Springer
Pages	191-204
Number of pages	14
Edition	1
ISBN (Electronic)	978-3-319-23506-6
ISBN (Print)	978-3-319-23505-9
DOIs	https://doi.org/10.1007/978-3-319-23506-6_13
Publication status	Published - 2015
Externally published	Yes

Publication series

Series	Lecture Notes in Computer Science
Volume	9360
ISSN	0302-9743

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

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, Vol. 9360).

@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, Springer, Cham, Lecture Notes in Computer Science, vol. 9360, 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 proceeding › Conference article in proceeding › Academic › peer-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, Vol. 9360). https://doi.org/10.1007/978-3-319-23506-6_13

Access to Document

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

Link to proceedings