---

---

slide: Abstraction function and representation invariant

---