2015
Being and Change: Reasoning About Invariance
Publication
Publication
Presented at the
Correct System Design - Symposium in Honor of Ernst-Rudiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany
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.
| Additional Metadata | |
|---|---|
| Unspecified | |
| R. Meyer , A. Platzer , H. Wehrheim | |
| Correct System Design - Symposium in Honor of Ernst-Rudiger Olderog on the Occasion of His 60th Birthday | |
| Organisation | Computer Security |
|
de Boer, F., & de Gouw, S. (2015). Being and Change: Reasoning About Invariance. In R. Meyer, A. Platzer, & H. Wehrheim (Eds.), . |
|
