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.
|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|
|Number of pages||14|
|Publication status||Published - 2015|
|Series||Lecture Notes in Computer Science|