Correctness of Distributed Programs
Stub. Safety vs. liveness as the two correctness-property classes; correctness proofs via predicate logic; assertional reasoning for safety, well-founded sets for liveness; and programming/predicate-transformer logics for deriving correct programs.
How to state and prove that a distributed program does what it should. Splits correctness into safety (“nothing bad ever happens” — invariants) and liveness (“something good eventually happens” — termination, progress), proved by different techniques: assertional/invariant reasoning for safety, and well-founded orderings (ranking functions that can’t decrease forever) for liveness. Predicate logic underlies both, and predicate transformers give a way to derive a correct program from its specification rather than verify one after the fact.
Outline (TODO — flesh out each)
- Correctness criteria — safety properties, liveness properties
- Correctness proofs
- Predicate logic — propositional and predicate logic review
- Assertional reasoning: proving safety properties
- Proving liveness properties using well-founded sets
- Programming logic; predicate transformers