Book contents
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- 2 Hoare logic
- 3 Separation logic
- 4 Soundness of Hoare logic
- 5 Mechanized Semantic Library
- 6 Separation algebras
- 7 Operators on separation algebras
- 8 First-order separation logic
- 9 A little case study
- 10 Covariant recursive predicates
- 11 Share accounting
- II Higher order separation logic
- III Separation logic for CompCert
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- VII Applications
- Bibliography
- Index
4 - Soundness of Hoare logic
from I - Generic separation logic
Published online by Cambridge University Press: 05 August 2014
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- 2 Hoare logic
- 3 Separation logic
- 4 Soundness of Hoare logic
- 5 Mechanized Semantic Library
- 6 Separation algebras
- 7 Operators on separation algebras
- 8 First-order separation logic
- 9 A little case study
- 10 Covariant recursive predicates
- 11 Share accounting
- II Higher order separation logic
- III Separation logic for CompCert
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- VII Applications
- Bibliography
- Index
Summary
A program logic is sound when, if you can prove some specification (such as a Hoare triple {P} c {Q}) about a program c, then when c actually executes it will obey that specification.
What does it mean to “actually execute”? If c is written in a source language L, then we can formally specify an operational semantics for L. Then we can give a formal model for the program logic in terms of the operational semantics, and formally prove the soundness of all the inference rules of the logic.
Then one is left trying to believe that the operational semantics accurately characterizes the execution of the language L. But many source languages do not directly execute; they are compiled into lower-level languages or machine language that executes it its own operational semantics. Fortunately, at this point in the 21st century we can rely on formal compiler correctness proofs, that execution in the operational semantics of the source language corresponds to execution in the operational semantics of the machine language. And the machine languages tend to be well specified; machine language is already a formal language, and it is even possible to formally prove that the logic gates of a computer chip correctly implement the instruction set architecure (ISA), that is, the machine language.
So, we prove the program correct using the program logic, we prove the program logic sound with respect to the source-language operational semantics, and prove the compiler correct with respect to the source- and machine-language semantics.
- Type
- Chapter
- Information
- Program Logics for Certified Compilers , pp. 25 - 32Publisher: Cambridge University PressPrint publication year: 2014