Being and Change: Reasoning About Invariance
The work
| Authors | Frank S. de Boer; Stijn de Gouw |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2015 |
| Citekey | boer2015being |
Where it appeared
| Published in | 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 |
|---|---|
| Pages | 191--204 |
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.
A copy is held
pdf, 241.1 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-16 15:38 UTC |
Filed under
Cite it as
@inproceedings{boer2015being,
title = {Being and Change: Reasoning About Invariance},
author = {Frank S. de Boer and Stijn de Gouw},
year = {2015},
booktitle = {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},
pages = {191--204},
}
This record lives at https://refs.drheap.org/boer2015being/ and will keep doing so.