|
|
|
| Friday (1/11) and Monday (1/14): |
||
| program
correctness |
||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| • | Basic
material on proving programs correct |
|||||||||||||
| – | Program
specifications |
|||||||||||||
| – | Semantics
of programming language constructs |
|||||||||||||
| – | Pre-
and post-conditions |
|||||||||||||
| – | Hoare
triples and Dijkstra weakest preconditions |
|||||||||||||
| – | Loop
invariants |
|||||||||||||
| – | Proving
correctness of data structures |
|||||||||||||
| • | Intent |
|||||||||||||
| – | Valuable
material on its own |
|||||||||||||
| – | Basis
for understanding software specification work |
|||||||||||||
| – | “Not
a mere matter of programming” |
|||||||||||||