This package contains samples of JML specifications that illustrate issues in component-based programming relating to callbacks and JML's model program feature. They are based on an example in Clemens Szyperski's book Component Software: Beyond Object-Oriented Programming (ACM Press and Addison-Wesley, NY, 1998).

The type Directory is the most interesting here, and illustrates the model program feature.