Copyright © 2014 Péter Battyányi
2014
Table of Contents
- Introduction
- 1. While programs
- The operational semantics of while programs
- Denotational semantics of while programs
- Partial correctness of while-programs
- The stepwise Floyd–Naur method
- Hoare logic from a semantical point of view
- Proof outlines
- Proof rules for the Hoare calculus
- The wlp-calculus
- Relative completeness of the Hoare partial correctness calculus
- The wp-calculus
- Total correctness
- Soundness of the Hoare total correctness calculus
- Relative completeness of the Hoare total correctness calculus
- 2. Recursive programs
- 3. Disjoint parallel programs
- 4. Shared variable parallelism
- 5. Synchronization
- A. Mathematical background
- B. Exercises
- Bibliography