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 }