This package contains samples of JML specifications relating to some abstractions of input and output. These samples were originally written by Arnd Poetzsch-Heffter, based on an example by K. Rustan M. Leino and Greg Nelson, that appears in their paper "Data abstraction and information hiding" (ACM Transactions on Programming Languages and Systems, volume 24, number 5, pp. 491-553, September 2002).