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 }