|
|
Topic |
Slides |
Introduction |
1 - 5 |
Hoare’s notation |
7 - 11 |
Formal proofs |
12 - 16 |
Partial and total correctness |
17 - 19 |
Example specification |
20 - 25 |
Review of predicate calculus |
26 - 34 |
Floyd-Hoare Logic |
35 - 59 |
How does one find an invariant |
60 - 62 |
Additional and derived rules |
63 - 72 |
Forwards and backwards proof |
73 - 79 |
Annotations |
80 - 82, 92 - 93 |
Mechanizing verification |
83 - 86 |
Verification conditions |
87 - 112 |
Weakest preconditions |
113 121 |
Strongest postconditions |
122 - 133 |
Total correctness |
134 - 154 |
Soundness and completeness |
155 - 179 |
Overview of additional topics |
180 - 181 |
Arrays |
182 - 190 |
Blocks and local variables |
191 - 194 |
FOR -commands |
196 - 213 |
Axiomatic semantics and Clarke’s theorem |
214 - 215 |
Refinement |
216 - 251 |
Separation logic |
252 - 293 |
Conclusion |
294 |