//# 1 errors, 518 messages
//#
package net.sourceforge.pebble.index;
    //#responseindex.java:1:1: class: net.sourceforge.pebble.index.ResponseIndex

import net.sourceforge.pebble.comparator.ReverseResponseIdComparator;
import net.sourceforge.pebble.domain.Blog;
import net.sourceforge.pebble.domain.BlogEntry;
import net.sourceforge.pebble.domain.Response;
import net.sourceforge.pebble.domain.State;
import org.apache.commons.logging.Log;
import org.apache.commons.logging.LogFactory;

import java.io.*;
import java.util.ArrayList;
import java.util.Collections;
import java.util.List;
import java.util.Collection;

/**
 * Keeps an index of all responses.
 *
 * @author    Simon Brown
 */
public class ResponseIndex {

  private static final Log log = LogFactory.getLog(ResponseIndex.class);
    //#responseindex.java:24: method: net.sourceforge.pebble.index.ResponseIndex.net.sourceforge.pebble.index.ResponseIndex__static_init
    //#responseindex.java:24: Warning: method not available
    //#    -- call on Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.index.ResponseIndex
    //#    method: net.sourceforge.pebble.index.ResponseIndex__static_init
    //#    unanalyzed callee: Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Descendant_Table[net/sourceforge/pebble/index/ResponseIndex]
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.clear()V
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getApprovedResponses()Ljava/util/List;
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getNumberOfApprovedResponses()I
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getNumberOfPendingResponses()I
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getNumberOfRejectedResponses()I
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getNumberOfResponses()I
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getPendingResponses()Ljava/util/List;
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getRecentApprovedResponses(I)Ljava/util/List;
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getRecentResponses(I)Ljava/util/List;
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getRejectedResponses()Ljava/util/List;
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.index(Ljava/util/Collection;)V
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.index(Lnet/sourceforge/pebble/domain/Response;)V
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.readIndex(Lnet/sourceforge/pebble/domain/State;)Ljava/util/List;
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.unindex(Lnet/sourceforge/pebble/domain/Response;)V
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.writeIndex(Lnet/sourceforge/pebble/domain/State;)V
    //#output(net.sourceforge.pebble.index.ResponseIndex__static_init): log
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Descendant_Table[net/sourceforge/pebble/index/ResponseIndex] == &__Dispatch_Table
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.clear()V == &clear
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getApprovedResponses()Ljava/util/List; == &getApprovedResponses
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getNumberOfApprovedResponses()I == &getNumberOfApprovedResponses
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getNumberOfPendingResponses()I == &getNumberOfPendingResponses
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getNumberOfRejectedResponses()I == &getNumberOfRejectedResponses
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getNumberOfResponses()I == &getNumberOfResponses
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getPendingResponses()Ljava/util/List; == &getPendingResponses
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getRecentApprovedResponses(I)Ljava/util/List; == &getRecentApprovedResponses
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getRecentResponses(I)Ljava/util/List; == &getRecentResponses
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.getRejectedResponses()Ljava/util/List; == &getRejectedResponses
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.index(Ljava/util/Collection;)V == &index
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.index(Lnet/sourceforge/pebble/domain/Response;)V == &index
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.readIndex(Lnet/sourceforge/pebble/domain/State;)Ljava/util/List; == &readIndex
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.unindex(Lnet/sourceforge/pebble/domain/Response;)V == &unindex
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): __Dispatch_Table.writeIndex(Lnet/sourceforge/pebble/domain/State;)V == &writeIndex
    //#post(net.sourceforge.pebble.index.ResponseIndex__static_init): init'ed(log)
    //#responseindex.java:24: end of method: net.sourceforge.pebble.index.ResponseIndex.net.sourceforge.pebble.index.ResponseIndex__static_init

  private Blog blog;

  private List<String> approvedResponses = new ArrayList<String>();
  private List<String> pendingResponses = new ArrayList<String>();
  private List<String> rejectedResponses = new ArrayList<String>();

  public ResponseIndex(Blog blog) {
    //#responseindex.java:32: method: void net.sourceforge.pebble.index.ResponseIndex.net.sourceforge.pebble.index.ResponseIndex(Blog)
    //#input(void net.sourceforge.pebble.index.ResponseIndex(Blog)): blog
    //#input(void net.sourceforge.pebble.index.ResponseIndex(Blog)): log
    //#input(void net.sourceforge.pebble.index.ResponseIndex(Blog)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void net.sourceforge.pebble.index.ResponseIndex(Blog)): net/sourceforge/pebble/domain/State.PENDING
    //#input(void net.sourceforge.pebble.index.ResponseIndex(Blog)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void net.sourceforge.pebble.index.ResponseIndex(Blog)): this
    //#output(void net.sourceforge.pebble.index.ResponseIndex(Blog)): new ArrayList(ResponseIndex#1) num objects
    //#output(void net.sourceforge.pebble.index.ResponseIndex(Blog)): new ArrayList(ResponseIndex#2) num objects
    //#output(void net.sourceforge.pebble.index.ResponseIndex(Blog)): new ArrayList(ResponseIndex#3) num objects
    //#output(void net.sourceforge.pebble.index.ResponseIndex(Blog)): new ArrayList(readIndex#1) num objects
    //#output(void net.sourceforge.pebble.index.ResponseIndex(Blog)): this.approvedResponses
    //#output(void net.sourceforge.pebble.index.ResponseIndex(Blog)): this.blog
    //#output(void net.sourceforge.pebble.index.ResponseIndex(Blog)): this.pendingResponses
    //#output(void net.sourceforge.pebble.index.ResponseIndex(Blog)): this.rejectedResponses
    //#new obj(void net.sourceforge.pebble.index.ResponseIndex(Blog)): new ArrayList(ResponseIndex#1)
    //#new obj(void net.sourceforge.pebble.index.ResponseIndex(Blog)): new ArrayList(ResponseIndex#2)
    //#new obj(void net.sourceforge.pebble.index.ResponseIndex(Blog)): new ArrayList(ResponseIndex#3)
    //#new obj(void net.sourceforge.pebble.index.ResponseIndex(Blog)): new ArrayList(readIndex#1)
    //#pre[1] (void net.sourceforge.pebble.index.ResponseIndex(Blog)): blog != null
    //#post(void net.sourceforge.pebble.index.ResponseIndex(Blog)): this.approvedResponses == &new ArrayList(readIndex#1)
    //#post(void net.sourceforge.pebble.index.ResponseIndex(Blog)): this.blog == blog
    //#post(void net.sourceforge.pebble.index.ResponseIndex(Blog)): this.blog != null
    //#post(void net.sourceforge.pebble.index.ResponseIndex(Blog)): this.pendingResponses == &new ArrayList(readIndex#1)
    //#post(void net.sourceforge.pebble.index.ResponseIndex(Blog)): this.rejectedResponses == &new ArrayList(readIndex#1)
    //#post(void net.sourceforge.pebble.index.ResponseIndex(Blog)): new ArrayList(ResponseIndex#1) num objects == 1
    //#post(void net.sourceforge.pebble.index.ResponseIndex(Blog)): new ArrayList(ResponseIndex#2) num objects == 1
    //#post(void net.sourceforge.pebble.index.ResponseIndex(Blog)): new ArrayList(ResponseIndex#3) num objects == 1
    //#post(void net.sourceforge.pebble.index.ResponseIndex(Blog)): new ArrayList(readIndex#1) num objects == 3
    //#unanalyzed(void net.sourceforge.pebble.index.ResponseIndex(Blog)): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(void net.sourceforge.pebble.index.ResponseIndex(Blog)): Effects-of-calling:net.sourceforge.pebble.domain.Blog:getIndexesDirectory
    //#unanalyzed(void net.sourceforge.pebble.index.ResponseIndex(Blog)): Effects-of-calling:java.io.File
    //#unanalyzed(void net.sourceforge.pebble.index.ResponseIndex(Blog)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void net.sourceforge.pebble.index.ResponseIndex(Blog)): Effects-of-calling:java.io.FileReader
    //#unanalyzed(void net.sourceforge.pebble.index.ResponseIndex(Blog)): Effects-of-calling:java.io.BufferedReader
    //#unanalyzed(void net.sourceforge.pebble.index.ResponseIndex(Blog)): Effects-of-calling:java.io.BufferedReader:readLine
    //#unanalyzed(void net.sourceforge.pebble.index.ResponseIndex(Blog)): Effects-of-calling:java.util.List:add
    //#unanalyzed(void net.sourceforge.pebble.index.ResponseIndex(Blog)): Effects-of-calling:java.io.BufferedReader:close
    //#unanalyzed(void net.sourceforge.pebble.index.ResponseIndex(Blog)): Effects-of-calling:org.apache.commons.logging.Log:error
    //#unanalyzed(void net.sourceforge.pebble.index.ResponseIndex(Blog)): Effects-of-calling:java.util.Collections:sort
    this.blog = blog;

    approvedResponses = readIndex(State.APPROVED);
    pendingResponses = readIndex(State.PENDING);
    rejectedResponses = readIndex(State.REJECTED);
  }
    //#responseindex.java:38: end of method: void net.sourceforge.pebble.index.ResponseIndex.net.sourceforge.pebble.index.ResponseIndex(Blog)

  /**
   * Clears the index.
   */
  public void clear() {
    approvedResponses = new ArrayList<String>();
    //#responseindex.java:44: method: void net.sourceforge.pebble.index.ResponseIndex.clear()
    //#input(void clear()): log
    //#input(void clear()): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void clear()): net/sourceforge/pebble/domain/State.PENDING
    //#input(void clear()): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void clear()): this
    //#input(void clear()): this.blog
    //#input(void clear()): this.pendingResponses
    //#input(void clear()): this.rejectedResponses
    //#output(void clear()): new ArrayList(clear#1) num objects
    //#output(void clear()): new ArrayList(clear#2) num objects
    //#output(void clear()): new ArrayList(clear#3) num objects
    //#output(void clear()): this.approvedResponses
    //#output(void clear()): this.pendingResponses
    //#output(void clear()): this.rejectedResponses
    //#new obj(void clear()): new ArrayList(clear#1)
    //#new obj(void clear()): new ArrayList(clear#2)
    //#new obj(void clear()): new ArrayList(clear#3)
    //#pre[1] (void clear()): (soft) this.pendingResponses != null
    //#pre[2] (void clear()): (soft) this.rejectedResponses != null
    //#pre[4] (void clear()): (soft) this.blog != null
    //#post(void clear()): this.approvedResponses == &new ArrayList(clear#1)
    //#post(void clear()): this.pendingResponses == &new ArrayList(clear#2)
    //#post(void clear()): this.rejectedResponses == &new ArrayList(clear#3)
    //#post(void clear()): new ArrayList(clear#1) num objects == 1
    //#post(void clear()): new ArrayList(clear#2) num objects == 1
    //#post(void clear()): new ArrayList(clear#3) num objects == 1
    //#unanalyzed(void clear()): Effects-of-calling:net.sourceforge.pebble.domain.Blog:getIndexesDirectory
    //#unanalyzed(void clear()): Effects-of-calling:java.io.File
    //#unanalyzed(void clear()): Effects-of-calling:org.apache.commons.logging.Log:error
    //#unanalyzed(void clear()): Effects-of-calling:java.io.FileWriter
    //#unanalyzed(void clear()): Effects-of-calling:java.io.BufferedWriter
    //#unanalyzed(void clear()): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(void clear()): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void clear()): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void clear()): Effects-of-calling:java.io.BufferedWriter:write
    //#unanalyzed(void clear()): Effects-of-calling:java.io.BufferedWriter:newLine
    //#unanalyzed(void clear()): Effects-of-calling:java.io.BufferedWriter:flush
    //#unanalyzed(void clear()): Effects-of-calling:java.io.BufferedWriter:close
    writeIndex(State.APPROVED);

    pendingResponses = new ArrayList<String>();
    writeIndex(State.PENDING);

    rejectedResponses = new ArrayList<String>();
    writeIndex(State.REJECTED);
  }
    //#responseindex.java:52: end of method: void net.sourceforge.pebble.index.ResponseIndex.clear()

  /**
   * Indexes one or more blog entries.
   *
   * @param blogEntries   a List of BlogEntry instances
   */
  public synchronized void index(Collection<BlogEntry> blogEntries) {
    for (BlogEntry blogEntry : blogEntries) {
    //#responseindex.java:60: method: void net.sourceforge.pebble.index.ResponseIndex.index(Collection)
    //#input(void index(Collection)): blogEntries
    //#input(void index(Collection)): log
    //#input(void index(Collection)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).__Tag
    //#input(void index(Collection)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name
    //#input(void index(Collection)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).__Tag
    //#input(void index(Collection)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name
    //#input(void index(Collection)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).__Tag
    //#input(void index(Collection)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name
    //#input(void index(Collection)): net/sourceforge/pebble/domain/BlogEntry.__Descendant_Table[net/sourceforge/pebble/domain/BlogEntry]
    //#input(void index(Collection)): net/sourceforge/pebble/domain/BlogEntry.__Descendant_Table[others]
    //#input(void index(Collection)): net/sourceforge/pebble/domain/BlogEntry.__Dispatch_Table.getComments()Ljava/util/List;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/BlogEntry.__Dispatch_Table.getResponses()Ljava/util/List;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/BlogEntry.__Dispatch_Table.getTrackBacks()Ljava/util/List;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[others]
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getBlogEntry()Lnet/sourceforge/pebble/domain/BlogEntry;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getComments()Ljava/util/List;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getGuid()Ljava/lang/String;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getId()J
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isApproved()Z
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isPending()Z
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isRejected()Z
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Response]
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Response.__Descendant_Table[others]
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getBlogEntry()Lnet/sourceforge/pebble/domain/BlogEntry;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getGuid()Ljava/lang/String;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getId()J
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.isApproved()Z
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.isPending()Z
    //#input(void index(Collection)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.isRejected()Z
    //#input(void index(Collection)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void index(Collection)): net/sourceforge/pebble/domain/State.PENDING
    //#input(void index(Collection)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void index(Collection)): net/sourceforge/pebble/domain/State.__Descendant_Table[net/sourceforge/pebble/domain/State]
    //#input(void index(Collection)): net/sourceforge/pebble/domain/State.__Descendant_Table[others]
    //#input(void index(Collection)): net/sourceforge/pebble/domain/State.__Dispatch_Table.equals(Ljava/lang/Object;)Z
    //#input(void index(Collection)): net/sourceforge/pebble/domain/State.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void index(Collection)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[others]
    //#input(void index(Collection)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getBlogEntry()Lnet/sourceforge/pebble/domain/BlogEntry;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getGuid()Ljava/lang/String;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getId()J
    //#input(void index(Collection)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void index(Collection)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isApproved()Z
    //#input(void index(Collection)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isPending()Z
    //#input(void index(Collection)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isRejected()Z
    //#input(void index(Collection)): this
    //#input(void index(Collection)): this.approvedResponses
    //#input(void index(Collection)): this.blog
    //#input(void index(Collection)): this.pendingResponses
    //#input(void index(Collection)): this.rejectedResponses
    //#pre[1] (void index(Collection)): blogEntries != null
    //#pre[2] (void index(Collection)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name != null
    //#pre[3] (void index(Collection)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name != null
    //#pre[4] (void index(Collection)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name != null
    //#pre[6] (void index(Collection)): (soft) this.approvedResponses != null
    //#pre[7] (void index(Collection)): (soft) this.blog != null
    //#pre[8] (void index(Collection)): (soft) this.pendingResponses != null
    //#pre[9] (void index(Collection)): (soft) this.rejectedResponses != null
    //#presumption(void index(Collection)): blogEntry.comments@60 != null
    //#presumption(void index(Collection)): java.util.Iterator:next(...).__Tag@60 == net/sourceforge/pebble/domain/BlogEntry
    //#presumption(void index(Collection)): java.util.Iterator:next(...).__Tag@61 in {net/sourceforge/pebble/domain/Comment, net/sourceforge/pebble/domain/Response, net/sourceforge/pebble/domain/TrackBack}
    //#presumption(void index(Collection)): java.util.Iterator:next(...)@60 != null
    //#presumption(void index(Collection)): java.util.Iterator:next(...)@61 != null
    //#presumption(void index(Collection)): response.blogEntry@62 != null
    //#presumption(void index(Collection)): response.blogEntry@64 != null
    //#presumption(void index(Collection)): response.blogEntry@66 != null
    //#presumption(void index(Collection)): response.date@62 != null
    //#presumption(void index(Collection)): response.date@64 != null
    //#presumption(void index(Collection)): response.date@66 != null
    //#presumption(void index(Collection)): response.state.__Tag@61 == net/sourceforge/pebble/domain/State
    //#presumption(void index(Collection)): response.state.__Tag@62 == net/sourceforge/pebble/domain/State
    //#presumption(void index(Collection)): response.state.__Tag@64 == net/sourceforge/pebble/domain/State
    //#presumption(void index(Collection)): response.state@61 != null
    //#presumption(void index(Collection)): response.state@62 != null
    //#presumption(void index(Collection)): response.state@64 != null
    //#unanalyzed(void index(Collection)): Effects-of-calling:net.sourceforge.pebble.domain.Blog:getIndexesDirectory
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.io.File
    //#unanalyzed(void index(Collection)): Effects-of-calling:org.apache.commons.logging.Log:error
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.io.FileWriter
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.io.BufferedWriter
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.io.BufferedWriter:write
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.io.BufferedWriter:newLine
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.io.BufferedWriter:flush
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.io.BufferedWriter:close
    //#unanalyzed(void index(Collection)): Effects-of-calling:getState
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.util.Date:getTime
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.lang.String:valueOf
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void index(Collection)): Effects-of-calling:net.sourceforge.pebble.domain.BlogEntry:getId
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.util.List:add
    //#unanalyzed(void index(Collection)): Effects-of-calling:getComments
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.util.List:addAll
    //#unanalyzed(void index(Collection)): Effects-of-calling:java.util.Collections:sort
    //#test_vector(void index(Collection)): java.util.Iterator:hasNext(...)@60: {1}, {0}
    //#test_vector(void index(Collection)): java.util.Iterator:hasNext(...)@61: {1}, {0}
      for (Response response : blogEntry.getResponses()) {
        if (response.isApproved()) {
          approvedResponses.add(response.getGuid());
        } else if (response.isPending()) {
          pendingResponses.add(response.getGuid());
        } else if (response.isRejected()) {
          rejectedResponses.add(response.getGuid());
        }
      }
    }

    Collections.sort(approvedResponses, new ReverseResponseIdComparator());
    Collections.sort(pendingResponses, new ReverseResponseIdComparator());
    Collections.sort(rejectedResponses, new ReverseResponseIdComparator());
    writeIndex(State.APPROVED);
    writeIndex(State.PENDING);
    writeIndex(State.REJECTED);
  }
    //#responseindex.java:78: end of method: void net.sourceforge.pebble.index.ResponseIndex.index(Collection)

  /**
   * Indexes a single response.
   *
   * @param response    a Response instance
   */
  public synchronized void index(Response response) {
    if (response.isApproved()) {
    //#responseindex.java:86: method: void net.sourceforge.pebble.index.ResponseIndex.index(Response)
    //#responseindex.java:86: Warning: suspicious precondition
    //#    the precondition for response.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.index.ResponseIndex
    //#    method: void index(Response)
    //#    suspicious precondition index: [5]
    //#input(void index(Response)): log
    //#input(void index(Response)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).__Tag
    //#input(void index(Response)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name
    //#input(void index(Response)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).__Tag
    //#input(void index(Response)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name
    //#input(void index(Response)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).__Tag
    //#input(void index(Response)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name
    //#input(void index(Response)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void index(Response)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[others]
    //#input(void index(Response)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getBlogEntry()Lnet/sourceforge/pebble/domain/BlogEntry;
    //#input(void index(Response)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getGuid()Ljava/lang/String;
    //#input(void index(Response)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getId()J
    //#input(void index(Response)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void index(Response)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isApproved()Z
    //#input(void index(Response)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isPending()Z
    //#input(void index(Response)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isRejected()Z
    //#input(void index(Response)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void index(Response)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Response]
    //#input(void index(Response)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void index(Response)): net/sourceforge/pebble/domain/Response.__Descendant_Table[others]
    //#input(void index(Response)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getBlogEntry()Lnet/sourceforge/pebble/domain/BlogEntry;
    //#input(void index(Response)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getGuid()Ljava/lang/String;
    //#input(void index(Response)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getId()J
    //#input(void index(Response)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void index(Response)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.isApproved()Z
    //#input(void index(Response)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.isPending()Z
    //#input(void index(Response)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.isRejected()Z
    //#input(void index(Response)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void index(Response)): net/sourceforge/pebble/domain/State.PENDING
    //#input(void index(Response)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void index(Response)): net/sourceforge/pebble/domain/State.__Descendant_Table[net/sourceforge/pebble/domain/State]
    //#input(void index(Response)): net/sourceforge/pebble/domain/State.__Descendant_Table[others]
    //#input(void index(Response)): net/sourceforge/pebble/domain/State.__Dispatch_Table.equals(Ljava/lang/Object;)Z
    //#input(void index(Response)): net/sourceforge/pebble/domain/State.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void index(Response)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void index(Response)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[others]
    //#input(void index(Response)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getBlogEntry()Lnet/sourceforge/pebble/domain/BlogEntry;
    //#input(void index(Response)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getGuid()Ljava/lang/String;
    //#input(void index(Response)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getId()J
    //#input(void index(Response)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void index(Response)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isApproved()Z
    //#input(void index(Response)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isPending()Z
    //#input(void index(Response)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isRejected()Z
    //#input(void index(Response)): response
    //#input(void index(Response)): response.__Tag
    //#input(void index(Response)): response.blogEntry
    //#input(void index(Response)): response.date
    //#input(void index(Response)): response.state
    //#input(void index(Response)): response.state.__Tag
    //#input(void index(Response)): response.state.name
    //#input(void index(Response)): this
    //#input(void index(Response)): this.approvedResponses
    //#input(void index(Response)): this.blog
    //#input(void index(Response)): this.pendingResponses
    //#input(void index(Response)): this.rejectedResponses
    //#pre[4] (void index(Response)): response != null
    //#pre[5] (void index(Response)): response.__Tag in {net/sourceforge/pebble/domain/Comment, net/sourceforge/pebble/domain/Response, net/sourceforge/pebble/domain/TrackBack}
    //#pre[8] (void index(Response)): response.state != null
    //#pre[9] (void index(Response)): response.state.__Tag == net/sourceforge/pebble/domain/State
    //#pre[1] (void index(Response)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name != null
    //#pre[2] (void index(Response)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name != null
    //#pre[3] (void index(Response)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name != null
    //#pre[6] (void index(Response)): (soft) response.blogEntry != null
    //#pre[7] (void index(Response)): (soft) response.date != null
    //#pre[10] (void index(Response)): (soft) init'ed(response.state.name)
    //#pre[12] (void index(Response)): (soft) this.approvedResponses != null
    //#pre[13] (void index(Response)): (soft) this.blog != null
    //#pre[14] (void index(Response)): (soft) this.pendingResponses != null
    //#pre[15] (void index(Response)): (soft) this.rejectedResponses != null
    //#unanalyzed(void index(Response)): Effects-of-calling:net.sourceforge.pebble.domain.Blog:getIndexesDirectory
    //#unanalyzed(void index(Response)): Effects-of-calling:java.io.File
    //#unanalyzed(void index(Response)): Effects-of-calling:org.apache.commons.logging.Log:error
    //#unanalyzed(void index(Response)): Effects-of-calling:java.io.FileWriter
    //#unanalyzed(void index(Response)): Effects-of-calling:java.io.BufferedWriter
    //#unanalyzed(void index(Response)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(void index(Response)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void index(Response)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void index(Response)): Effects-of-calling:java.io.BufferedWriter:write
    //#unanalyzed(void index(Response)): Effects-of-calling:java.io.BufferedWriter:newLine
    //#unanalyzed(void index(Response)): Effects-of-calling:java.io.BufferedWriter:flush
    //#unanalyzed(void index(Response)): Effects-of-calling:java.io.BufferedWriter:close
    //#unanalyzed(void index(Response)): Effects-of-calling:getState
    //#unanalyzed(void index(Response)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(void index(Response)): Effects-of-calling:java.util.Date:getTime
    //#unanalyzed(void index(Response)): Effects-of-calling:java.lang.String:valueOf
    //#unanalyzed(void index(Response)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void index(Response)): Effects-of-calling:net.sourceforge.pebble.domain.BlogEntry:getId
    //#unanalyzed(void index(Response)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void index(Response)): Effects-of-calling:java.lang.StringBuilder:toString
      approvedResponses.add(response.getGuid());
      Collections.sort(approvedResponses, new ReverseResponseIdComparator());
      writeIndex(State.APPROVED);
    } else if (response.isPending()) {
      pendingResponses.add(response.getGuid());
      Collections.sort(pendingResponses, new ReverseResponseIdComparator());
      writeIndex(State.PENDING);
    } else if (response.isRejected()) {
      rejectedResponses.add(response.getGuid());
      Collections.sort(rejectedResponses, new ReverseResponseIdComparator());
      writeIndex(State.REJECTED);
    }
  }
    //#responseindex.java:99: end of method: void net.sourceforge.pebble.index.ResponseIndex.index(Response)

  /**
   * Unindexes a single response.
   *
   * @param response    a Response instance
   */
  public synchronized void unindex(Response response) {
    if (approvedResponses.contains(response.getGuid())) {
    //#responseindex.java:107: method: void net.sourceforge.pebble.index.ResponseIndex.unindex(Response)
    //#responseindex.java:107: Warning: suspicious precondition
    //#    the precondition for response.__Tag is not a contiguous range of values
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.index.ResponseIndex
    //#    method: void unindex(Response)
    //#    suspicious precondition index: [2]
    //#input(void unindex(Response)): log
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[others]
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getBlogEntry()Lnet/sourceforge/pebble/domain/BlogEntry;
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getGuid()Ljava/lang/String;
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getId()J
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Response]
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/Response.__Descendant_Table[others]
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getBlogEntry()Lnet/sourceforge/pebble/domain/BlogEntry;
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getGuid()Ljava/lang/String;
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getId()J
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/State.PENDING
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[others]
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getBlogEntry()Lnet/sourceforge/pebble/domain/BlogEntry;
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getGuid()Ljava/lang/String;
    //#input(void unindex(Response)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getId()J
    //#input(void unindex(Response)): response
    //#input(void unindex(Response)): response.__Tag
    //#input(void unindex(Response)): response.blogEntry
    //#input(void unindex(Response)): response.date
    //#input(void unindex(Response)): this
    //#input(void unindex(Response)): this.approvedResponses
    //#input(void unindex(Response)): this.blog
    //#input(void unindex(Response)): this.pendingResponses
    //#input(void unindex(Response)): this.rejectedResponses
    //#pre[1] (void unindex(Response)): response != null
    //#pre[2] (void unindex(Response)): response.__Tag in {net/sourceforge/pebble/domain/Comment, net/sourceforge/pebble/domain/Response, net/sourceforge/pebble/domain/TrackBack}
    //#pre[3] (void unindex(Response)): response.blogEntry != null
    //#pre[4] (void unindex(Response)): response.date != null
    //#pre[6] (void unindex(Response)): this.approvedResponses != null
    //#pre[7] (void unindex(Response)): (soft) this.blog != null
    //#pre[8] (void unindex(Response)): (soft) this.pendingResponses != null
    //#pre[9] (void unindex(Response)): (soft) this.rejectedResponses != null
    //#unanalyzed(void unindex(Response)): Effects-of-calling:net.sourceforge.pebble.domain.Blog:getIndexesDirectory
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.io.File
    //#unanalyzed(void unindex(Response)): Effects-of-calling:org.apache.commons.logging.Log:error
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.io.FileWriter
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.io.BufferedWriter
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.io.BufferedWriter:write
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.io.BufferedWriter:newLine
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.io.BufferedWriter:flush
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.io.BufferedWriter:close
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.util.Date:getTime
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.lang.String:valueOf
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void unindex(Response)): Effects-of-calling:net.sourceforge.pebble.domain.BlogEntry:getId
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void unindex(Response)): Effects-of-calling:java.lang.StringBuilder:toString
    //#test_vector(void unindex(Response)): java.util.List:contains(...)@107: {0}, {1}
    //#test_vector(void unindex(Response)): java.util.List:contains(...)@110: {0}, {1}
    //#test_vector(void unindex(Response)): java.util.List:contains(...)@113: {0}, {1}
      approvedResponses.remove(response.getGuid());
      writeIndex(State.APPROVED);
    } else if (pendingResponses.contains(response.getGuid())) {
      pendingResponses.remove(response.getGuid());
      writeIndex(State.PENDING);
    } else if (rejectedResponses.contains(response.getGuid())) {
      rejectedResponses.remove(response.getGuid());
      writeIndex(State.REJECTED);
    }
  }
    //#responseindex.java:117: end of method: void net.sourceforge.pebble.index.ResponseIndex.unindex(Response)

  /**
   * Helper method to load the index.
   */
  private List<String> readIndex(State state) {
    String filename = null;
    //#responseindex.java:123: method: List net.sourceforge.pebble.index.ResponseIndex.readIndex(State)
    //#input(List readIndex(State)): log
    //#input(List readIndex(State)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(List readIndex(State)): net/sourceforge/pebble/domain/State.PENDING
    //#input(List readIndex(State)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(List readIndex(State)): state
    //#input(List readIndex(State)): this
    //#input(List readIndex(State)): this.blog
    //#output(List readIndex(State)): new ArrayList(readIndex#1) num objects
    //#output(List readIndex(State)): return_value
    //#new obj(List readIndex(State)): new ArrayList(readIndex#1)
    //#pre[3] (List readIndex(State)): this.blog != null
    //#presumption(List readIndex(State)): org.apache.commons.logging.LogFactory:getLog(...)@24 != null
    //#post(List readIndex(State)): return_value == &new ArrayList(readIndex#1)
    //#post(List readIndex(State)): new ArrayList(readIndex#1) num objects == 1
    //#test_vector(List readIndex(State)): java.io.File:exists(...)@134: {0}, {1}
    List<String> responses = new ArrayList<String>();
    if (state == State.APPROVED) {
        filename = "responses-approved.index";
    } else if (state == State.PENDING) {
      filename = "responses-pending.index";
    } else if (state == State.REJECTED) {
      filename = "responses-rejected.index";
    }

    File indexFile = new File(blog.getIndexesDirectory(), filename);
    //#responseindex.java:133: Warning: method not available
    //#    -- call on String net.sourceforge.pebble.domain.Blog:getIndexesDirectory()
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.index.ResponseIndex
    //#    method: List readIndex(State)
    //#    unanalyzed callee: String net.sourceforge.pebble.domain.Blog:getIndexesDirectory()
    if (indexFile.exists()) {
      try {
        BufferedReader reader = new BufferedReader(new FileReader(indexFile));
        String response = reader.readLine();
        while (response != null) {
          responses.add(response);
          response = reader.readLine();
        }

        reader.close();
      } catch (Exception e) {
        log.error("Error while reading index", e);
    //#responseindex.java:145: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:error(Object, Throwable)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.index.ResponseIndex
    //#    method: List readIndex(State)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:error(Object, Throwable)
      }
    }

    Collections.sort(responses, new ReverseResponseIdComparator());

    return responses;
    //#responseindex.java:151: end of method: List net.sourceforge.pebble.index.ResponseIndex.readIndex(State)
  }

  /**
   * Helper method to write out the index to disk.
   */
  private void writeIndex(State state) {
    String filename = null;
    //#responseindex.java:158: method: void net.sourceforge.pebble.index.ResponseIndex.writeIndex(State)
    //#input(void writeIndex(State)): log
    //#input(void writeIndex(State)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void writeIndex(State)): net/sourceforge/pebble/domain/State.PENDING
    //#input(void writeIndex(State)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void writeIndex(State)): state
    //#input(void writeIndex(State)): this
    //#input(void writeIndex(State)): this.approvedResponses
    //#input(void writeIndex(State)): this.blog
    //#input(void writeIndex(State)): this.pendingResponses
    //#input(void writeIndex(State)): this.rejectedResponses
    //#pre[3] (void writeIndex(State)): (soft) this.approvedResponses != null
    //#pre[4] (void writeIndex(State)): (soft) this.blog != null
    //#pre[5] (void writeIndex(State)): (soft) this.pendingResponses != null
    //#pre[6] (void writeIndex(State)): (soft) this.rejectedResponses != null
    //#presumption(void writeIndex(State)): org.apache.commons.logging.LogFactory:getLog(...)@24 != null
    //#test_vector(void writeIndex(State)): java.util.Iterator:hasNext(...)@175: {1}, {0}
    List<String> responses = null;
    if (state == State.APPROVED) {
        filename = "responses-approved.index";
        responses = approvedResponses;
    } else if (state == State.PENDING) {
      filename = "responses-pending.index";
      responses = pendingResponses;
    } else if (state == State.REJECTED) {
      filename = "responses-rejected.index";
      responses = rejectedResponses;
    }

    try {
      File indexFile = new File(blog.getIndexesDirectory(), filename);
    //#responseindex.java:172: Warning: method not available
    //#    -- call on String net.sourceforge.pebble.domain.Blog:getIndexesDirectory()
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.index.ResponseIndex
    //#    method: void writeIndex(State)
    //#    unanalyzed callee: String net.sourceforge.pebble.domain.Blog:getIndexesDirectory()
      BufferedWriter writer = new BufferedWriter(new FileWriter(indexFile));

      for (String response : responses) {
    //#responseindex.java:175: ?null dereference
    //#    responses != null
    //#    severity: MEDIUM
    //#    class: net.sourceforge.pebble.index.ResponseIndex
    //#    method: void writeIndex(State)
    //#    basic block: bb_8
    //#    assertion: responses != null
    //#    VN: responses
    //#    Expected: Inverse{null} or Invalid
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
        writer.write(response);
        writer.newLine();
      }

      writer.flush();
      writer.close();
    } catch (Exception e) {
      log.error("Error while writing index", e);
    //#responseindex.java:183: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:error(Object, Throwable)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.index.ResponseIndex
    //#    method: void writeIndex(State)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:error(Object, Throwable)
    }
  }
    //#responseindex.java:185: end of method: void net.sourceforge.pebble.index.ResponseIndex.writeIndex(State)

  /**
   * Gets the number of approved responses for this blog.
   *
   * @return  an int
   */
  public int getNumberOfApprovedResponses() {
    return approvedResponses.size();
    //#responseindex.java:193: method: int net.sourceforge.pebble.index.ResponseIndex.getNumberOfApprovedResponses()
    //#input(int getNumberOfApprovedResponses()): this
    //#input(int getNumberOfApprovedResponses()): this.approvedResponses
    //#output(int getNumberOfApprovedResponses()): return_value
    //#pre[2] (int getNumberOfApprovedResponses()): this.approvedResponses != null
    //#post(int getNumberOfApprovedResponses()): init'ed(return_value)
    //#responseindex.java:193: end of method: int net.sourceforge.pebble.index.ResponseIndex.getNumberOfApprovedResponses()
  }

  /**
   * Gets the number of pending responses for this blog.
   *
   * @return  an int
   */
  public int getNumberOfPendingResponses() {
    return pendingResponses.size();
    //#responseindex.java:202: method: int net.sourceforge.pebble.index.ResponseIndex.getNumberOfPendingResponses()
    //#input(int getNumberOfPendingResponses()): this
    //#input(int getNumberOfPendingResponses()): this.pendingResponses
    //#output(int getNumberOfPendingResponses()): return_value
    //#pre[2] (int getNumberOfPendingResponses()): this.pendingResponses != null
    //#post(int getNumberOfPendingResponses()): init'ed(return_value)
    //#responseindex.java:202: end of method: int net.sourceforge.pebble.index.ResponseIndex.getNumberOfPendingResponses()
  }

  /**
   * Gets the number of rejected responses for this blog.
   *
   * @return  an int
   */
  public int getNumberOfRejectedResponses() {
    return rejectedResponses.size();
    //#responseindex.java:211: method: int net.sourceforge.pebble.index.ResponseIndex.getNumberOfRejectedResponses()
    //#input(int getNumberOfRejectedResponses()): this
    //#input(int getNumberOfRejectedResponses()): this.rejectedResponses
    //#output(int getNumberOfRejectedResponses()): return_value
    //#pre[2] (int getNumberOfRejectedResponses()): this.rejectedResponses != null
    //#post(int getNumberOfRejectedResponses()): init'ed(return_value)
    //#responseindex.java:211: end of method: int net.sourceforge.pebble.index.ResponseIndex.getNumberOfRejectedResponses()
  }

  /**
   * Gets the number of responses for this blog.
   *
   * @return  an int
   */
  public int getNumberOfResponses() {
    return getNumberOfApprovedResponses() + getNumberOfPendingResponses() + getNumberOfRejectedResponses();
    //#responseindex.java:220: method: int net.sourceforge.pebble.index.ResponseIndex.getNumberOfResponses()
    //#input(int getNumberOfResponses()): __Descendant_Table[net/sourceforge/pebble/index/ResponseIndex]
    //#input(int getNumberOfResponses()): __Descendant_Table[others]
    //#input(int getNumberOfResponses()): __Dispatch_Table.getNumberOfApprovedResponses()I
    //#input(int getNumberOfResponses()): __Dispatch_Table.getNumberOfPendingResponses()I
    //#input(int getNumberOfResponses()): __Dispatch_Table.getNumberOfRejectedResponses()I
    //#input(int getNumberOfResponses()): this
    //#input(int getNumberOfResponses()): this.__Tag
    //#input(int getNumberOfResponses()): this.approvedResponses
    //#input(int getNumberOfResponses()): this.pendingResponses
    //#input(int getNumberOfResponses()): this.rejectedResponses
    //#output(int getNumberOfResponses()): return_value
    //#pre[2] (int getNumberOfResponses()): this.__Tag == net/sourceforge/pebble/index/ResponseIndex
    //#pre[3] (int getNumberOfResponses()): this.approvedResponses != null
    //#pre[4] (int getNumberOfResponses()): this.pendingResponses != null
    //#pre[5] (int getNumberOfResponses()): this.rejectedResponses != null
    //#presumption(int getNumberOfResponses()): java.util.List:size(...)@202 + java.util.List:size(...)@193 in -4_294_967_296..6_442_450_943
    //#presumption(int getNumberOfResponses()): java.util.List:size(...)@202 + java.util.List:size(...)@193 + java.util.List:size(...)@211 in -2_147_483_648..4_294_967_295
    //#post(int getNumberOfResponses()): (soft) init'ed(return_value)
    //#unanalyzed(int getNumberOfResponses()): Effects-of-calling:java.util.List:size
    //#responseindex.java:220: end of method: int net.sourceforge.pebble.index.ResponseIndex.getNumberOfResponses()
  }

  /**
   * Gets the most recent N approved responses.
   *
   * @return  a List of response IDs
   */
  public List<String> getRecentResponses(int number) {
    return getRecentApprovedResponses(number);
    //#responseindex.java:229: method: List net.sourceforge.pebble.index.ResponseIndex.getRecentResponses(int)
    //#input(List getRecentResponses(int)): __Descendant_Table[net/sourceforge/pebble/index/ResponseIndex]
    //#input(List getRecentResponses(int)): __Descendant_Table[others]
    //#input(List getRecentResponses(int)): __Dispatch_Table.getRecentApprovedResponses(I)Ljava/util/List;
    //#input(List getRecentResponses(int)): number
    //#input(List getRecentResponses(int)): this
    //#input(List getRecentResponses(int)): this.__Tag
    //#input(List getRecentResponses(int)): this.approvedResponses
    //#output(List getRecentResponses(int)): return_value
    //#pre[3] (List getRecentResponses(int)): this.__Tag == net/sourceforge/pebble/index/ResponseIndex
    //#pre[4] (List getRecentResponses(int)): this.approvedResponses != null
    //#post(List getRecentResponses(int)): init'ed(return_value)
    //#unanalyzed(List getRecentResponses(int)): Effects-of-calling:java.util.List:size
    //#unanalyzed(List getRecentResponses(int)): Effects-of-calling:java.util.List:subList
    //#responseindex.java:229: end of method: List net.sourceforge.pebble.index.ResponseIndex.getRecentResponses(int)
  }

  /**
   * Gets the most recent N approved responses.
   *
   * @return  a List of response IDs
   */
  public List<String> getRecentApprovedResponses(int number) {
    if (approvedResponses.size() >= number) {
    //#responseindex.java:238: method: List net.sourceforge.pebble.index.ResponseIndex.getRecentApprovedResponses(int)
    //#input(List getRecentApprovedResponses(int)): number
    //#input(List getRecentApprovedResponses(int)): this
    //#input(List getRecentApprovedResponses(int)): this.approvedResponses
    //#output(List getRecentApprovedResponses(int)): return_value
    //#pre[3] (List getRecentApprovedResponses(int)): this.approvedResponses != null
    //#post(List getRecentApprovedResponses(int)): init'ed(return_value)
      return approvedResponses.subList(0, number);
    } else {
      return approvedResponses;
    //#responseindex.java:241: end of method: List net.sourceforge.pebble.index.ResponseIndex.getRecentApprovedResponses(int)
    }
  }

  /**
   * Gets the list of approved responses.
   *
   * @return  a List of response IDs
   */
  public List<String> getApprovedResponses() {
    return new ArrayList<String>(approvedResponses);
    //#responseindex.java:251: method: List net.sourceforge.pebble.index.ResponseIndex.getApprovedResponses()
    //#input(List getApprovedResponses()): this
    //#input(List getApprovedResponses()): this.approvedResponses
    //#output(List getApprovedResponses()): new ArrayList(getApprovedResponses#1) num objects
    //#output(List getApprovedResponses()): return_value
    //#new obj(List getApprovedResponses()): new ArrayList(getApprovedResponses#1)
    //#pre[2] (List getApprovedResponses()): init'ed(this.approvedResponses)
    //#post(List getApprovedResponses()): return_value == &new ArrayList(getApprovedResponses#1)
    //#post(List getApprovedResponses()): new ArrayList(getApprovedResponses#1) num objects == 1
    //#responseindex.java:251: end of method: List net.sourceforge.pebble.index.ResponseIndex.getApprovedResponses()
  }

  /**
   * Gets the list of pending responses.
   *
   * @return  a List of response IDs
   */
  public List<String> getPendingResponses() {
    return new ArrayList<String>(pendingResponses);
    //#responseindex.java:260: method: List net.sourceforge.pebble.index.ResponseIndex.getPendingResponses()
    //#input(List getPendingResponses()): this
    //#input(List getPendingResponses()): this.pendingResponses
    //#output(List getPendingResponses()): new ArrayList(getPendingResponses#1) num objects
    //#output(List getPendingResponses()): return_value
    //#new obj(List getPendingResponses()): new ArrayList(getPendingResponses#1)
    //#pre[2] (List getPendingResponses()): init'ed(this.pendingResponses)
    //#post(List getPendingResponses()): return_value == &new ArrayList(getPendingResponses#1)
    //#post(List getPendingResponses()): new ArrayList(getPendingResponses#1) num objects == 1
    //#responseindex.java:260: end of method: List net.sourceforge.pebble.index.ResponseIndex.getPendingResponses()
  }

  /**
   * Gets the list of rejected responses.
   *
   * @return  a List of response IDs
   */
  public List<String> getRejectedResponses() {
    return new ArrayList<String>(rejectedResponses);
    //#responseindex.java:269: method: List net.sourceforge.pebble.index.ResponseIndex.getRejectedResponses()
    //#input(List getRejectedResponses()): this
    //#input(List getRejectedResponses()): this.rejectedResponses
    //#output(List getRejectedResponses()): new ArrayList(getRejectedResponses#1) num objects
    //#output(List getRejectedResponses()): return_value
    //#new obj(List getRejectedResponses()): new ArrayList(getRejectedResponses#1)
    //#pre[2] (List getRejectedResponses()): init'ed(this.rejectedResponses)
    //#post(List getRejectedResponses()): return_value == &new ArrayList(getRejectedResponses#1)
    //#post(List getRejectedResponses()): new ArrayList(getRejectedResponses#1) num objects == 1
    //#responseindex.java:269: end of method: List net.sourceforge.pebble.index.ResponseIndex.getRejectedResponses()
  }

}    //#responseindex.java:: end of class: net.sourceforge.pebble.index.ResponseIndex
