Modular Verification of Higher-Order Methods With Mandatory Calls Specified by Model Programs

No program exists in a vacuum. Instead, developers use components from libraries and frameworks. For example, a Java programmer may use Swing, Java's input/output framework, and Jakarta Commons. Such reuse improves productivity. It can also improve other attributes of software, such as its performance or maintainability. The importance of reusable OO components is both a challenge and opportunity for software engineering. It is an opportunity because better documentation of such components can payoff in productivity and quality.