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    }