Practice: How to abstract messy details?


Determine high-level properties that describe the behavior of a routing protocol.

Define these properties in terms of rules (i.e., sufficient conditions) that are easier to reason about.

Show examples where the logic assists reasoning.

(This work is not about automatic theorem proving, model checking, etc.)