Book contents
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- II Higher order separation logic
- III Separation logic for CompCert
- 22 Verifiable C
- 23 Expressions, values, and assertions
- 24 The VST separation logic for C light
- 25 Typechecking for Verifiable C
- 26 Derived rules and proof automation for C light
- 27 Proof of a program
- 28 More C programs
- 29 Dependently typed C programs
- 30 Concurrent separation logic
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- VII Applications
- Bibliography
- Index
27 - Proof of a program
from III - Separation logic for CompCert
Published online by Cambridge University Press: 05 August 2014
- Frontmatter
- Dedication
- Contents
- Road map
- Acknowledgments
- 1 Introduction
- I Generic separation logic
- II Higher order separation logic
- III Separation logic for CompCert
- 22 Verifiable C
- 23 Expressions, values, and assertions
- 24 The VST separation logic for C light
- 25 Typechecking for Verifiable C
- 26 Derived rules and proof automation for C light
- 27 Proof of a program
- 28 More C programs
- 29 Dependently typed C programs
- 30 Concurrent separation logic
- IV Operational semantics of CompCert
- V Higher-order semantic models
- VI Semantic model and soundness of Verifiable C
- VII Applications
- Bibliography
- Index
Summary
We illustrate the use of tactical proof (semi)automation on the program shown in Figure 27.1. We compile this source program reverse.c into a C-light abstract-syntax data structure using the front end of CompCert, the clightgen utility. This produces a Coq file reverse.v with a sequence of definitions in the CompCert abstract-syntax tree structures (Figure 27.2).
Clightgen comprises CompCert's (unverified) parser into CompCert C, followed by CompCert's (verified) translation into C light. The fact that one or another of these front-end phases is unverified does not concern us, because we apply the program logic to the output of these translations. If we specify correctness properties of reverse.v and prove them, then the C light program will have those properties, regardless of whether it matches the source program reverse.c. Of course, it is very desirable for reverse.v to match reverse.c, so the programmer may reason informally about unverified properties of reverse.c such as timing, information flow, or resource consumption.
This program uses linked lists of 32-bit integers. Before proceeding with the verification, we should develop the theory of list segments (a “theory” is just what we call a collection of definitions, lemmas, and tactics useful for reasoning about the subject matter). Chapter 19 explained the theory of list segments; in the file list.v we build an lseg theory parameterized by a C structure definition.
- Type
- Chapter
- Information
- Program Logics for Certified Compilers , pp. 195 - 207Publisher: Cambridge University PressPrint publication year: 2014