Contract-Based Software Development: Inheritance and Frame Rules

This lecture note explains how contract-based techniques interact with the classic object-oriented notion of inheritance, and how the subclass-superclass relationship presents some challenges to contract-based programming. We also investigate the concept of \emph{frame rules}, which express the parts of objects that do not change when a given command is executed.