    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.prover;
    004
    005    import java.io.OutputStream;
    006    import java.io.FilterOutputStream;
    007    import java.io.IOException;
    008
    009    /**
    010     * This class is a {@link FilterOutputStream} class that forwards its
    011     * given output to two given {@link OutputStream}s.
    012     *
    013     * @author Rustan Leino
    014     * @version 11 Aug 2000
    015     */
    016
    017    public class TeeOutputStream extends FilterOutputStream
    018    {
    019        /**
    020         * The other underlying output stream to be filtered (the first
    021         * being <code>out</code> in the superclass).
    022         */
    023        //@ spec_public
    024        protected /*@ non_null @*/ OutputStream out2;
    025
    026        /**
    027         * Creates an output stream filter built on top of two specified
    028         * underlying output streams.
    029         *
    030         * @param   out0  the first of the underlying output streams;
    031         *                will be assigned to <code>this.out</code>;
    032         *                should not be <code>null</code>
    033         * @param   out1  the second of the underlying output streams;
    034         *                will be assigned to <code>this.out2</code>;
    035         *                should not be <code>null</code>
    036         */
    037        //@ public normal_behavior
    038        //@   modifies this.out2;
    039        //@   ensures this.out2 == out1;
    040        public TeeOutputStream(/*@ non_null @*/ OutputStream out0,
    041                               /*@ non_null @*/ OutputStream out1) {
    042            super(out0);
    043            this.out2 = out1;
    044        }
    045
    046        /**
    047         * Writes the specified <code>byte</code> to this output stream.
    048         *
    049         * <p> The <code>write</code> method of
    050         * <code>TeeOutputStream</code> calls the <code>write</code>
    051         * method of its two underlying output streams, that is, it
    052         * performs <tt>out.write(b)</tt> and then
    053         * <tt>out2.write(b)</tt>. </p>
    054         *
    055         * <p> Implements the abstract <tt>write</tt> method of
    056         * <tt>OutputStream</tt>. </p>
    057         *
    058         * @param      b   the <code>byte</code>.
    059         * @exception  IOException  if an I/O error occurs.
    060         */
    061        public void write(int b) throws IOException {
    062            out.write(b);
    063            out2.write(b);
    064        }
    065
    066        /**
    067         * Writes <code>b.length</code> bytes to this output stream.
    068         *
    069         * <p>The <code>write</code> method of
    070         * <code>TeeOutputStream</code> calls the <code>write</code>
    071         * method of its two underlying output streams, that is, it
    072         * performs <tt>out.write(b)</tt> and then
    073         * <tt>out2.write(b)</tt>. </p>
    074         *
    075         * @param      b   the data to be written.
    076         * @exception  IOException  if an I/O error occurs.
    077         * @see        java.io.FilterOutputStream#write(byte[], int, int)
    078         */
    079        //@ also
    080        //@ public normal_behavior
    081        //@ requires b != null;
    082        //@   modifies \everything;
    083        public void write(byte b[]) throws IOException {
    084            out.write(b);
    085            out2.write(b);
    086        }
    087
    088        /**
    089         * Writes <code>len</code> bytes from the specified
    090         * <code>byte</code> array starting at offset <code>off</code> to
    091         * this output stream.
    092         *
    093         * <p>The <code>write</code> method of
    094         * <code>TeeOutputStream</code> calls the <code>write</code>
    095         * method of its two underlying output streams, that is, it
    096         * performs <tt>out.write(b)</tt> and then
    097         * <tt>out2.write(b)</tt>. </p>
    098         *
    099         * @param      b     the data.
    100         * @param      off   the start offset in the data.
    101         * @param      len   the number of bytes to write.
    102         * @exception  IOException  if an I/O error occurs.
    103         * @see        java.io.FilterOutputStream#write(int)
    104         */
    105        //@ also
    106        //@ public normal_behavior
    107        //@   requires b != null;
    108        //@   requires b.length >= off + len;
    109        //@   modifies \everything;
    110        public void write(byte b[], int off, int len) throws IOException {
    111            out.write(b, off, len);
    112            out2.write(b, off, len);
    113        }
    114
    115        /**
    116         * Flushes this output stream and forces any buffered output bytes
    117         * to be written out to the stream.
    118         *
    119         * <p> The <code>flush</code> method of
    120         * <code>FilterOutputStream</code> calls the <code>flush</code>
    121         * method of its two underlying output streams. </p>
    122         *
    123         * @exception  IOException  if an I/O error occurs.
    124         * @see        java.io.FilterOutputStream#flush
    125         */
    126        public void flush() throws IOException {
    127            out.flush();
    128            out2.flush();
    129        }
    130
    131        /**
    132         * Closes this output stream and releases any system resources
    133         * associated with the stream.
    134         *
    135         * <p> The <code>close</code> method of
    136         * <code>FilterOutputStream</code> calls its <code>flush</code>
    137         * method, and then calls the <code>close</code> method of its two
    138         * underlying output streams. </p>
    139         *
    140         * @exception  IOException  if an I/O error occurs.
    141         * @see        java.io.FilterOutputStream#flush()
    142         * @see        java.io.FilterOutputStream#close
    143         */
    144        public void close() throws IOException {
    145            try {
    146                flush();
    147            } catch (IOException ignored) {
    148                // ignored
    149            }
    150            out.close();
    151            out2.close();
    152        }
    153    }