Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Developer-Oriented Correctness Proofs
A Case Study of Cheney’s Algorithm
verfasst von : Holger Gast
Erschienen in: Formal Methods and Software Engineering
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
This paper examines the problem of structuring proofs in functional software verification from a novel perspective. By aligning the proofs with the operational behaviour of the program, we allow the formalization of the underlying concepts and their properties to reflect informal correctness arguments. By splitting the proof along the different aspects of the code, we achieve re-use of both theories and proof strategies across algorithms, thus enabling reasoning by analogy as employed in software construction. We demonstrate the viability and usefulness of the approach using a low-level C implementation of Cheney’s algorithm.