| 1 | /* |
|---|
| 2 | * This program is free software; you can redistribute it and/or modify |
|---|
| 3 | * it under the terms of the GNU General Public License as published by |
|---|
| 4 | * the Free Software Foundation; either version 2 of the License, or |
|---|
| 5 | * (at your option) any later version. |
|---|
| 6 | * |
|---|
| 7 | * This program is distributed in the hope that it will be useful, |
|---|
| 8 | * but WITHOUT ANY WARRANTY; without even the implied warranty of |
|---|
| 9 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
|---|
| 10 | * GNU General Public License for more details. |
|---|
| 11 | * |
|---|
| 12 | * You should have received a copy of the GNU General Public License |
|---|
| 13 | * along with this program; if not, write to the Free Software |
|---|
| 14 | * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. |
|---|
| 15 | */ |
|---|
| 16 | |
|---|
| 17 | /* |
|---|
| 18 | * WekaEnumeration.java |
|---|
| 19 | * Copyright (C) 2009 University of Waikato, Hamilton, New Zealand |
|---|
| 20 | * |
|---|
| 21 | */ |
|---|
| 22 | package weka.core; |
|---|
| 23 | |
|---|
| 24 | import java.util.Enumeration; |
|---|
| 25 | import java.util.List; |
|---|
| 26 | import weka.core.RevisionHandler; |
|---|
| 27 | |
|---|
| 28 | /** |
|---|
| 29 | * Class for enumerating an array list's elements. |
|---|
| 30 | */ |
|---|
| 31 | public class WekaEnumeration |
|---|
| 32 | implements Enumeration, RevisionHandler { |
|---|
| 33 | |
|---|
| 34 | /** The counter. */ |
|---|
| 35 | private int m_Counter; |
|---|
| 36 | // These JML commands say how m_Counter implements Enumeration |
|---|
| 37 | //@ in moreElements; |
|---|
| 38 | //@ private represents moreElements = m_Counter < m_Vector.size(); |
|---|
| 39 | //@ private invariant 0 <= m_Counter && m_Counter <= m_Vector.size(); |
|---|
| 40 | |
|---|
| 41 | /** The vector. */ |
|---|
| 42 | private /*@non_null@*/ List m_Vector; |
|---|
| 43 | |
|---|
| 44 | /** Special element. Skipped during enumeration. */ |
|---|
| 45 | private int m_SpecialElement; |
|---|
| 46 | //@ private invariant -1 <= m_SpecialElement; |
|---|
| 47 | //@ private invariant m_SpecialElement < m_Vector.size(); |
|---|
| 48 | //@ private invariant m_SpecialElement>=0 ==> m_Counter!=m_SpecialElement; |
|---|
| 49 | |
|---|
| 50 | /** |
|---|
| 51 | * Constructs an enumeration. |
|---|
| 52 | * |
|---|
| 53 | * @param vector the vector which is to be enumerated |
|---|
| 54 | */ |
|---|
| 55 | public WekaEnumeration(/*@non_null@*/List vector) { |
|---|
| 56 | |
|---|
| 57 | m_Counter = 0; |
|---|
| 58 | m_Vector = vector; |
|---|
| 59 | m_SpecialElement = -1; |
|---|
| 60 | } |
|---|
| 61 | |
|---|
| 62 | /** |
|---|
| 63 | * Constructs an enumeration with a special element. |
|---|
| 64 | * The special element is skipped during the enumeration. |
|---|
| 65 | * |
|---|
| 66 | * @param vector the vector which is to be enumerated |
|---|
| 67 | * @param special the index of the special element |
|---|
| 68 | */ |
|---|
| 69 | //@ requires 0 <= special && special < vector.size(); |
|---|
| 70 | public WekaEnumeration(/*@non_null@*/List vector, int special){ |
|---|
| 71 | |
|---|
| 72 | m_Vector = vector; |
|---|
| 73 | m_SpecialElement = special; |
|---|
| 74 | if (special == 0) { |
|---|
| 75 | m_Counter = 1; |
|---|
| 76 | } else { |
|---|
| 77 | m_Counter = 0; |
|---|
| 78 | } |
|---|
| 79 | } |
|---|
| 80 | |
|---|
| 81 | |
|---|
| 82 | /** |
|---|
| 83 | * Tests if there are any more elements to enumerate. |
|---|
| 84 | * |
|---|
| 85 | * @return true if there are some elements left |
|---|
| 86 | */ |
|---|
| 87 | public final /*@pure@*/ boolean hasMoreElements() { |
|---|
| 88 | |
|---|
| 89 | if (m_Counter < m_Vector.size()) { |
|---|
| 90 | return true; |
|---|
| 91 | } |
|---|
| 92 | return false; |
|---|
| 93 | } |
|---|
| 94 | |
|---|
| 95 | /** |
|---|
| 96 | * Returns the next element. |
|---|
| 97 | * |
|---|
| 98 | * @return the next element to be enumerated |
|---|
| 99 | */ |
|---|
| 100 | //@ also requires hasMoreElements(); |
|---|
| 101 | public final Object nextElement() { |
|---|
| 102 | |
|---|
| 103 | Object result = m_Vector.get(m_Counter); |
|---|
| 104 | |
|---|
| 105 | m_Counter++; |
|---|
| 106 | if (m_Counter == m_SpecialElement) { |
|---|
| 107 | m_Counter++; |
|---|
| 108 | } |
|---|
| 109 | return result; |
|---|
| 110 | } |
|---|
| 111 | |
|---|
| 112 | /** |
|---|
| 113 | * Returns the revision string. |
|---|
| 114 | * |
|---|
| 115 | * @return the revision |
|---|
| 116 | */ |
|---|
| 117 | public String getRevision() { |
|---|
| 118 | return RevisionUtils.extract("$Revision: 5955 $"); |
|---|
| 119 | } |
|---|
| 120 | } |
|---|