Contractor Validation Tool

 

All the files necessary for replaying this case studies are available in the examples section of this web site.

  1. 1.PipedOutputStream

Class source: JDK 1.4 implementation (Java)
Behaviour requirements source: Javadoc documentation restrictions

The PipedOutputStream class is an implementation of an output stream that can be connected to a piped input stream to create a communications pipe. The piped output stream is the sending end of the pipe. More precisely, an instance of the PipedOutputStream class can engage in 4 different actions: connect, write, flush and close.

We produced a straightforward translation of the JDK 1.4 implementation of the PipedOutputStream to C. We also wrote the requires clauses for the class methods as the necessary conditions to avoid exceptions being thrown when executing methods of the class.

We then ran  Contractor and obtained the following abstraction:.

PipedOutputStream_files/PipedOutputStream.pdf

This abstraction shows to be an accurate representation of the Java official documentation. For instance, the documentation for the connect method says that “if this object is already connected to some other piped input stream, an IOException is thrown.”. This is captured by the abstraction by making the connect action unavailable once a connection is established.

The documentation for the close method reads that after closure the “stream may no longer be used for writing”. This is reflected in the transition from S14 to S12, since the latter does not allow to perform the write operation.

More interestingly, the abstraction shows a close loop transition on the initial state, which contradicts the Java documentation since it allows the following trace: close-connect-write, which exhibits the use of the writing operation after the pipe was closed. We analysed if this trace was legal in two ways: i) we first wrote an example program exercising this trace to see if it threw an exception; and ii) we analysed the JDK implementation to see if there was any additional condition which might make the closure of a non-connected buffer throw an exception. We found that, despite the documentation says otherwise, the closure of unconnected piped output streams is legal and it produces no changes in the class fields whatsoever.


 

ICSE 2011 Manuscript Case Studies