Abstract
| 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 | |
| Publication status | Published - 2015 |
| Externally published | Yes |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 9360 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Fingerprint
Cite this
}
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 -