001    /*
002     * Copyright (C) 2000-2006 Iowa State University
003     *
004     * This file is part of mjc, the MultiJava Compiler.
005     *
006     * This program is free software; you can redistribute it and/or modify
007     * it under the terms of the GNU General Public License as published by
008     * the Free Software Foundation; either version 2 of the License, or
009     * (at your option) any later version.
010     *
011     * This program is distributed in the hope that it will be useful,
012     * but WITHOUT ANY WARRANTY; without even the implied warranty of
013     * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
014     * GNU General Public License for more details.
015     *
016     * You should have received a copy of the GNU General Public License
017     * along with this program; if not, write to the Free Software
018     * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
019     *
020     * $Id: LineIterator.java,v 1.9 2006/08/13 02:36:41 chalin Exp $
021     */
022    package junitutils;
023    
024    import java.io.*;
025    import java.util.Iterator;
026    
027    /** This is a utility class that is an iterator over the lines produced
028        by reading a file.  It is used in particular by various
029        JUnit tests.
030    
031        @author David R. Cok
032    */
033    public class LineIterator implements Iterator {
034    
035        //@ public invariant elementType == \type(String);
036        //@ public invariant !returnsNull;
037    
038        //@ public represents moreElements <- nextLine != null;
039    
040        /** A reader that reads lines from the file. */
041        private /*@ non_null */ BufferedReader r;
042        
043        /** The next value to be returned by the iterator.  We read ahead one so
044            that we know the value of hasNext() when asked.
045        */
046        /*@ spec_public */ private /*@ nullable */ String nextLine; //@ in objectState;
047    
048        /** Starts an iterator reading from the given external process. 
049            @param filename The name of the file to be read
050         */
051        /*@ public behavior
052          @   modifies nextLine, elementType, returnsNull;
053          @   ensures (* file is readable *);
054          @   signals (java.io.IOException) (* file is not readable *);
055          @ also private behavior
056          @   modifies r;
057          @*/
058        public LineIterator(/*@ non_null */ String filename) throws java.io.IOException  {
059            r = new BufferedReader(new FileReader(filename)); 
060            nextLine = r.readLine();
061            //System.out.println("READ " + nextLine);
062            //@ set elementType = \type(String);
063            //@ set returnsNull = false;
064        }
065    
066        /** Per a standard iterator, returns true if there is another value waiting. */
067        public boolean hasNext() throws Error {
068            if (nextLine == null) {
069                try {
070                    r.close();
071                } catch (java.io.IOException e) {
072                    throw new Error("EXCEPTION in hasNext - " + e); 
073                }
074            }
075            return nextLine != null;
076        }
077    
078        /** Per a standard iterator, returns the next value - and throws 
079            java.util.NoSuchElementException if the list has been exhausted 
080            (hasNext() returns false).
081        */
082        public Object next() throws java.util.NoSuchElementException, Error {
083            //@ set remove_called_since = false;
084            if (nextLine == null) 
085                throw new java.util.NoSuchElementException();
086    
087            try {
088                String n = nextLine;
089                nextLine = r.readLine();
090                //System.out.println("READ " + nextLine);
091                return n;
092            } catch (java.io.IOException e) {
093                throw new Error("EXCEPTION in next - " + e); 
094            }
095        }
096    
097        /** This operation will throw an exception, as there is no need for 
098            remove in this context. */
099        //@ also
100        //@ requires \typeof(this)==\type(LineIterator);
101        //@ ensures false;
102        //@ signals (UnsupportedOperationException) true;
103        public void remove() throws UnsupportedOperationException {
104            throw new java.lang.UnsupportedOperationException();
105        }
106    
107    }
108    
109    
110