//# 19 errors, 747 messages
//#
/*
    //#responsemanager.java:1:1: class: net.sourceforge.pebble.domain.ResponseManager
    //#responsemanager.java:1:1: method: net.sourceforge.pebble.domain.ResponseManager.net.sourceforge.pebble.domain.ResponseManager__static_init
 * Copyright (c) 2003-2006, Simon Brown
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 *   - Redistributions of source code must retain the above copyright
 *     notice, this list of conditions and the following disclaimer.
 *
 *   - Redistributions in binary form must reproduce the above copyright
 *     notice, this list of conditions and the following disclaimer in
 *     the documentation and/or other materials provided with the
 *     distribution.
 *
 *   - Neither the name of Pebble nor the names of its contributors may
 *     be used to endorse or promote products derived from this software
 *     without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 */
package net.sourceforge.pebble.domain;

import net.sourceforge.pebble.comparator.ResponseByDateComparator;
import net.sourceforge.pebble.api.event.comment.CommentEvent;
import net.sourceforge.pebble.api.event.comment.CommentListener;
import net.sourceforge.pebble.api.event.trackback.TrackBackEvent;
import net.sourceforge.pebble.api.event.trackback.TrackBackListener;

import java.util.*;

/**
 * Internal comment and TrackBack listener used to manage the list of
 * responses for the associated blog.
 *
 * @author    Simon Brown
 */
public class ResponseManager implements CommentListener, TrackBackListener {

  /** the owning blog */
  private Blog blog;

  /** the set of recent comments */
  private SortedSet recentComments;

  /** the set of recent TrackBacks */
  private SortedSet recentTrackBacks;

  /** the set of recent responses (comments and TrackBacks) */
  private SortedSet approvedResponses;

  /** the set of pending responses (comments and TrackBacks) */
  private SortedSet pendingResponses;

  /** the set of rejected responses (comments and TrackBacks) */
  private SortedSet rejectedResponses;

  /**
   * Creates a new instance associated with the specified blog.
   *
   * @param blog    a Blog instance
   */
  public ResponseManager(Blog blog) {
    //#responsemanager.java:73: method: void net.sourceforge.pebble.domain.ResponseManager.net.sourceforge.pebble.domain.ResponseManager(Blog)
    //#input(void net.sourceforge.pebble.domain.ResponseManager(Blog)): blog
    //#input(void net.sourceforge.pebble.domain.ResponseManager(Blog)): this
    //#output(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#1) num objects
    //#output(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#3) num objects
    //#output(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#5) num objects
    //#output(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#7) num objects
    //#output(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#9) num objects
    //#output(void net.sourceforge.pebble.domain.ResponseManager(Blog)): this.approvedResponses
    //#output(void net.sourceforge.pebble.domain.ResponseManager(Blog)): this.blog
    //#output(void net.sourceforge.pebble.domain.ResponseManager(Blog)): this.pendingResponses
    //#output(void net.sourceforge.pebble.domain.ResponseManager(Blog)): this.recentComments
    //#output(void net.sourceforge.pebble.domain.ResponseManager(Blog)): this.recentTrackBacks
    //#output(void net.sourceforge.pebble.domain.ResponseManager(Blog)): this.rejectedResponses
    //#new obj(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#1)
    //#new obj(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#3)
    //#new obj(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#5)
    //#new obj(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#7)
    //#new obj(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#9)
    //#post(void net.sourceforge.pebble.domain.ResponseManager(Blog)): this.approvedResponses == &new TreeSet(ResponseManager#5)
    //#post(void net.sourceforge.pebble.domain.ResponseManager(Blog)): this.blog == blog
    //#post(void net.sourceforge.pebble.domain.ResponseManager(Blog)): init'ed(this.blog)
    //#post(void net.sourceforge.pebble.domain.ResponseManager(Blog)): this.pendingResponses == &new TreeSet(ResponseManager#7)
    //#post(void net.sourceforge.pebble.domain.ResponseManager(Blog)): this.recentComments == &new TreeSet(ResponseManager#1)
    //#post(void net.sourceforge.pebble.domain.ResponseManager(Blog)): this.recentTrackBacks == &new TreeSet(ResponseManager#3)
    //#post(void net.sourceforge.pebble.domain.ResponseManager(Blog)): this.rejectedResponses == &new TreeSet(ResponseManager#9)
    //#post(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#1) num objects == 1
    //#post(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#3) num objects == 1
    //#post(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#5) num objects == 1
    //#post(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#7) num objects == 1
    //#post(void net.sourceforge.pebble.domain.ResponseManager(Blog)): new TreeSet(ResponseManager#9) num objects == 1
    this.blog = blog;

    recentComments = new TreeSet(new ResponseByDateComparator());
    recentTrackBacks = new TreeSet(new ResponseByDateComparator());
    approvedResponses = new TreeSet(new ResponseByDateComparator());
    pendingResponses = new TreeSet(new ResponseByDateComparator());
    rejectedResponses = new TreeSet(new ResponseByDateComparator());
  }
    //#responsemanager.java:81: end of method: void net.sourceforge.pebble.domain.ResponseManager.net.sourceforge.pebble.domain.ResponseManager(Blog)

  /**
   * Gets recent comments.
   *
   * @return  a collection containing comments that have been left most recently
   */
  public Collection getRecentComments() {
    return this.recentComments;
    //#responsemanager.java:89: method: Collection net.sourceforge.pebble.domain.ResponseManager.getRecentComments()
    //#input(Collection getRecentComments()): this
    //#input(Collection getRecentComments()): this.recentComments
    //#output(Collection getRecentComments()): return_value
    //#pre[2] (Collection getRecentComments()): init'ed(this.recentComments)
    //#post(Collection getRecentComments()): return_value == this.recentComments
    //#post(Collection getRecentComments()): init'ed(return_value)
    //#responsemanager.java:89: end of method: Collection net.sourceforge.pebble.domain.ResponseManager.getRecentComments()
  }

  /**
   * Gets recent TrackBacks.
   *
   * @return  a collection containing TrackBacks that have been left most recently
   */
  public Collection getRecentTrackBacks() {
    return this.recentTrackBacks;
    //#responsemanager.java:98: method: Collection net.sourceforge.pebble.domain.ResponseManager.getRecentTrackBacks()
    //#input(Collection getRecentTrackBacks()): this
    //#input(Collection getRecentTrackBacks()): this.recentTrackBacks
    //#output(Collection getRecentTrackBacks()): return_value
    //#pre[2] (Collection getRecentTrackBacks()): init'ed(this.recentTrackBacks)
    //#post(Collection getRecentTrackBacks()): return_value == this.recentTrackBacks
    //#post(Collection getRecentTrackBacks()): init'ed(return_value)
    //#responsemanager.java:98: end of method: Collection net.sourceforge.pebble.domain.ResponseManager.getRecentTrackBacks()
  }

  /**
   * Gets recent responses (combined comments and TrackBacks).
   *
   * @return  a collection containing comments and TrackBacks that have been left
   *          most recently
   */
  public Collection getRecentResponses() {
    List list = new ArrayList();
    //#responsemanager.java:108: method: Collection net.sourceforge.pebble.domain.ResponseManager.getRecentResponses()
    //#input(Collection getRecentResponses()): this
    //#input(Collection getRecentResponses()): this.approvedResponses
    //#output(Collection getRecentResponses()): new ArrayList(getRecentResponses#1) num objects
    //#output(Collection getRecentResponses()): return_value
    //#new obj(Collection getRecentResponses()): new ArrayList(getRecentResponses#1)
    //#pre[2] (Collection getRecentResponses()): init'ed(this.approvedResponses)
    //#post(Collection getRecentResponses()): return_value == &new ArrayList(getRecentResponses#1)
    //#post(Collection getRecentResponses()): new ArrayList(getRecentResponses#1) num objects == 1
    list.addAll(approvedResponses);
    return list;
    //#responsemanager.java:110: end of method: Collection net.sourceforge.pebble.domain.ResponseManager.getRecentResponses()
  }

  /**
   * Gets the number of approved responses.
   *
   * @return  an int
   */
  public int getNumberOfApprovedResponses() {
    return approvedResponses.size();
    //#responsemanager.java:119: method: int net.sourceforge.pebble.domain.ResponseManager.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)
    //#responsemanager.java:119: end of method: int net.sourceforge.pebble.domain.ResponseManager.getNumberOfApprovedResponses()
  }

  /**
   * Gets pending responses (combined comments and TrackBacks).
   *
   * @return  a collection containing comments and TrackBacks that are pending
   */
  public Collection getPendingResponses() {
    List list = new ArrayList();
    //#responsemanager.java:128: method: Collection net.sourceforge.pebble.domain.ResponseManager.getPendingResponses()
    //#input(Collection getPendingResponses()): this
    //#input(Collection getPendingResponses()): this.pendingResponses
    //#output(Collection getPendingResponses()): new ArrayList(getPendingResponses#1) num objects
    //#output(Collection getPendingResponses()): return_value
    //#new obj(Collection getPendingResponses()): new ArrayList(getPendingResponses#1)
    //#pre[2] (Collection getPendingResponses()): init'ed(this.pendingResponses)
    //#post(Collection getPendingResponses()): return_value == &new ArrayList(getPendingResponses#1)
    //#post(Collection getPendingResponses()): new ArrayList(getPendingResponses#1) num objects == 1
    list.addAll(pendingResponses);
    return list;
    //#responsemanager.java:130: end of method: Collection net.sourceforge.pebble.domain.ResponseManager.getPendingResponses()
  }

  /**
   * Gets the number of pending responses.
   *
   * @return  an int
   */
  public int getNumberOfPendingResponses() {
    return pendingResponses.size();
    //#responsemanager.java:139: method: int net.sourceforge.pebble.domain.ResponseManager.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)
    //#responsemanager.java:139: end of method: int net.sourceforge.pebble.domain.ResponseManager.getNumberOfPendingResponses()
  }

  /**
   * Gets rejected responses (combined comments and TrackBacks).
   *
   * @return  a collection containing comments and TrackBacks that are rejected
   */
  public Collection getRejectedResponses() {
    List list = new ArrayList();
    //#responsemanager.java:148: method: Collection net.sourceforge.pebble.domain.ResponseManager.getRejectedResponses()
    //#input(Collection getRejectedResponses()): this
    //#input(Collection getRejectedResponses()): this.rejectedResponses
    //#output(Collection getRejectedResponses()): new ArrayList(getRejectedResponses#1) num objects
    //#output(Collection getRejectedResponses()): return_value
    //#new obj(Collection getRejectedResponses()): new ArrayList(getRejectedResponses#1)
    //#pre[2] (Collection getRejectedResponses()): init'ed(this.rejectedResponses)
    //#post(Collection getRejectedResponses()): return_value == &new ArrayList(getRejectedResponses#1)
    //#post(Collection getRejectedResponses()): new ArrayList(getRejectedResponses#1) num objects == 1
    list.addAll(rejectedResponses);
    return list;
    //#responsemanager.java:150: end of method: Collection net.sourceforge.pebble.domain.ResponseManager.getRejectedResponses()
  }

  /**
   * Gets the number of rejected responses.
   *
   * @return  an int
   */
  public int getNumberOfRejectedResponses() {
    return rejectedResponses.size();
    //#responsemanager.java:159: method: int net.sourceforge.pebble.domain.ResponseManager.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)
    //#responsemanager.java:159: end of method: int net.sourceforge.pebble.domain.ResponseManager.getNumberOfRejectedResponses()
  }

  /**
   * Called when a comment has been added.
   *
   * @param comment   a Comment instance
   */
  synchronized void addRecentComment(Comment comment) {
    if (comment.isApproved()) {
    //#responsemanager.java:168: method: void net.sourceforge.pebble.domain.ResponseManager.addRecentComment(Comment)
    //#input(void addRecentComment(Comment)): comment
    //#input(void addRecentComment(Comment)): comment.__Tag
    //#input(void addRecentComment(Comment)): comment.state
    //#input(void addRecentComment(Comment)): comment.state.__Tag
    //#input(void addRecentComment(Comment)): comment.state.name
    //#input(void addRecentComment(Comment)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).__Tag
    //#input(void addRecentComment(Comment)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name
    //#input(void addRecentComment(Comment)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).__Tag
    //#input(void addRecentComment(Comment)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name
    //#input(void addRecentComment(Comment)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).__Tag
    //#input(void addRecentComment(Comment)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[others]
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isApproved()Z
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isPending()Z
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isRejected()Z
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Response]
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/Response.__Descendant_Table[others]
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/State.PENDING
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/State.__Descendant_Table[net/sourceforge/pebble/domain/State]
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/State.__Descendant_Table[others]
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/State.__Dispatch_Table.equals(Ljava/lang/Object;)Z
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/State.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void addRecentComment(Comment)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void addRecentComment(Comment)): this
    //#input(void addRecentComment(Comment)): this.approvedResponses
    //#input(void addRecentComment(Comment)): this.pendingResponses
    //#input(void addRecentComment(Comment)): this.recentComments
    //#input(void addRecentComment(Comment)): this.rejectedResponses
    //#pre[1] (void addRecentComment(Comment)): comment != null
    //#pre[2] (void addRecentComment(Comment)): comment.__Tag == net/sourceforge/pebble/domain/Comment
    //#pre[3] (void addRecentComment(Comment)): comment.state != null
    //#pre[4] (void addRecentComment(Comment)): comment.state.__Tag == net/sourceforge/pebble/domain/State
    //#pre[5] (void addRecentComment(Comment)): (soft) init'ed(comment.state.name)
    //#pre[6] (void addRecentComment(Comment)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name != null
    //#pre[7] (void addRecentComment(Comment)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name != null
    //#pre[8] (void addRecentComment(Comment)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name != null
    //#pre[10] (void addRecentComment(Comment)): (soft) this.approvedResponses != null
    //#pre[11] (void addRecentComment(Comment)): (soft) this.pendingResponses != null
    //#pre[12] (void addRecentComment(Comment)): (soft) this.recentComments != null
    //#pre[13] (void addRecentComment(Comment)): (soft) this.rejectedResponses != null
    //#unanalyzed(void addRecentComment(Comment)): Effects-of-calling:getState
    //#unanalyzed(void addRecentComment(Comment)): Effects-of-calling:java.lang.String:equals
      recentComments.add(comment);
      approvedResponses.add(comment);
    } else if (comment.isPending()) {
      pendingResponses.add(comment);
    } else if (comment.isRejected()) {
      rejectedResponses.add(comment);
    }
  }
    //#responsemanager.java:176: end of method: void net.sourceforge.pebble.domain.ResponseManager.addRecentComment(Comment)

  /**
   * Called when a comment has been removed.
   *
   * @param comment   a Comment instance
   */
  synchronized void removeRecentComment(Comment comment) {
    recentComments.remove(comment);
    //#responsemanager.java:184: method: void net.sourceforge.pebble.domain.ResponseManager.removeRecentComment(Comment)
    //#input(void removeRecentComment(Comment)): comment
    //#input(void removeRecentComment(Comment)): this
    //#input(void removeRecentComment(Comment)): this.approvedResponses
    //#input(void removeRecentComment(Comment)): this.pendingResponses
    //#input(void removeRecentComment(Comment)): this.recentComments
    //#input(void removeRecentComment(Comment)): this.rejectedResponses
    //#pre[3] (void removeRecentComment(Comment)): this.approvedResponses != null
    //#pre[4] (void removeRecentComment(Comment)): this.pendingResponses != null
    //#pre[5] (void removeRecentComment(Comment)): this.recentComments != null
    //#pre[6] (void removeRecentComment(Comment)): this.rejectedResponses != null
    approvedResponses.remove(comment);
    pendingResponses.remove(comment);
    rejectedResponses.remove(comment);
  }
    //#responsemanager.java:188: end of method: void net.sourceforge.pebble.domain.ResponseManager.removeRecentComment(Comment)

  /**
   * Called when a TrackBack has been added.
   *
   * @param trackBack   a TrackBack instance
   */
  synchronized void addRecentTrackBack(TrackBack trackBack) {
    if (trackBack.isApproved()) {
    //#responsemanager.java:196: method: void net.sourceforge.pebble.domain.ResponseManager.addRecentTrackBack(TrackBack)
    //#input(void addRecentTrackBack(TrackBack)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).__Tag
    //#input(void addRecentTrackBack(TrackBack)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name
    //#input(void addRecentTrackBack(TrackBack)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).__Tag
    //#input(void addRecentTrackBack(TrackBack)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name
    //#input(void addRecentTrackBack(TrackBack)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).__Tag
    //#input(void addRecentTrackBack(TrackBack)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Response]
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/Response.__Descendant_Table[others]
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/State.PENDING
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/State.__Descendant_Table[net/sourceforge/pebble/domain/State]
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/State.__Descendant_Table[others]
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/State.__Dispatch_Table.equals(Ljava/lang/Object;)Z
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/State.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[others]
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isApproved()Z
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isPending()Z
    //#input(void addRecentTrackBack(TrackBack)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isRejected()Z
    //#input(void addRecentTrackBack(TrackBack)): this
    //#input(void addRecentTrackBack(TrackBack)): this.approvedResponses
    //#input(void addRecentTrackBack(TrackBack)): this.pendingResponses
    //#input(void addRecentTrackBack(TrackBack)): this.recentTrackBacks
    //#input(void addRecentTrackBack(TrackBack)): this.rejectedResponses
    //#input(void addRecentTrackBack(TrackBack)): trackBack
    //#input(void addRecentTrackBack(TrackBack)): trackBack.__Tag
    //#input(void addRecentTrackBack(TrackBack)): trackBack.state
    //#input(void addRecentTrackBack(TrackBack)): trackBack.state.__Tag
    //#input(void addRecentTrackBack(TrackBack)): trackBack.state.name
    //#pre[9] (void addRecentTrackBack(TrackBack)): trackBack != null
    //#pre[10] (void addRecentTrackBack(TrackBack)): trackBack.__Tag == net/sourceforge/pebble/domain/TrackBack
    //#pre[11] (void addRecentTrackBack(TrackBack)): trackBack.state != null
    //#pre[12] (void addRecentTrackBack(TrackBack)): trackBack.state.__Tag == net/sourceforge/pebble/domain/State
    //#pre[1] (void addRecentTrackBack(TrackBack)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name != null
    //#pre[2] (void addRecentTrackBack(TrackBack)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name != null
    //#pre[3] (void addRecentTrackBack(TrackBack)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name != null
    //#pre[5] (void addRecentTrackBack(TrackBack)): (soft) this.approvedResponses != null
    //#pre[6] (void addRecentTrackBack(TrackBack)): (soft) this.pendingResponses != null
    //#pre[7] (void addRecentTrackBack(TrackBack)): (soft) this.recentTrackBacks != null
    //#pre[8] (void addRecentTrackBack(TrackBack)): (soft) this.rejectedResponses != null
    //#pre[13] (void addRecentTrackBack(TrackBack)): (soft) init'ed(trackBack.state.name)
    //#unanalyzed(void addRecentTrackBack(TrackBack)): Effects-of-calling:getState
    //#unanalyzed(void addRecentTrackBack(TrackBack)): Effects-of-calling:java.lang.String:equals
      recentTrackBacks.add(trackBack);
      approvedResponses.add(trackBack);
    } else if (trackBack.isPending()) {
      pendingResponses.add(trackBack);
    } else if (trackBack.isRejected()) {
      rejectedResponses.add(trackBack);
    }
  }
    //#responsemanager.java:204: end of method: void net.sourceforge.pebble.domain.ResponseManager.addRecentTrackBack(TrackBack)

  /**
   * Called when a TrackBack has been removed.
   *
   * @param trackBack   a TrackBack instance
   */
  synchronized void removeRecentTrackBack(TrackBack trackBack) {
    recentTrackBacks.remove(trackBack);
    //#responsemanager.java:212: method: void net.sourceforge.pebble.domain.ResponseManager.removeRecentTrackBack(TrackBack)
    //#input(void removeRecentTrackBack(TrackBack)): this
    //#input(void removeRecentTrackBack(TrackBack)): this.approvedResponses
    //#input(void removeRecentTrackBack(TrackBack)): this.pendingResponses
    //#input(void removeRecentTrackBack(TrackBack)): this.recentTrackBacks
    //#input(void removeRecentTrackBack(TrackBack)): this.rejectedResponses
    //#input(void removeRecentTrackBack(TrackBack)): trackBack
    //#pre[2] (void removeRecentTrackBack(TrackBack)): this.approvedResponses != null
    //#pre[3] (void removeRecentTrackBack(TrackBack)): this.pendingResponses != null
    //#pre[4] (void removeRecentTrackBack(TrackBack)): this.recentTrackBacks != null
    //#pre[5] (void removeRecentTrackBack(TrackBack)): this.rejectedResponses != null
    approvedResponses.remove(trackBack);
    pendingResponses.remove(trackBack);
    rejectedResponses.remove(trackBack);
  }
    //#responsemanager.java:216: end of method: void net.sourceforge.pebble.domain.ResponseManager.removeRecentTrackBack(TrackBack)

  /**
   * Called when a comment has been added.
   *
   * @param event a CommentEvent instance
   */
  public void commentAdded(CommentEvent event) {
    addRecentComment(event.getComment());
    //#responsemanager.java:224: method: void net.sourceforge.pebble.domain.ResponseManager.commentAdded(CommentEvent)
    //#responsemanager.java:224: ?null dereference
    //#    __Descendant_Table[this.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void commentAdded(CommentEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: __Descendant_Table[this.__Tag] != null
    //#    VN: __Descendant_Table[this.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#responsemanager.java:224: ?precondition failure
    //#    net/sourceforge/pebble/domain/ResponseManager.addRecentComment: comment.__Tag == net/sourceforge/pebble/domain/Comment
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void commentAdded(CommentEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72.__Tag == net/sourceforge/pebble/domain/Comment
    //#    callee: void net/sourceforge/pebble/domain/ResponseManager.addRecentComment(Comment)
    //#    callee assertion: comment.__Tag == net/sourceforge/pebble/domain/Comment
    //#    callee file: responsemanager.java
    //#    callee precondition index: [2]
    //#    callee srcpos: 168
    //#    VN: net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72.__Tag
    //#    Expected: {793_344}
    //#    Bad: {801_280}
    //#    Attribs:  Int  Exp singleton  Bad singleton  Bad > Exp
    //#input(void commentAdded(CommentEvent)): __Descendant_Table[net/sourceforge/pebble/domain/ResponseManager]
    //#input(void commentAdded(CommentEvent)): __Descendant_Table[others]
    //#input(void commentAdded(CommentEvent)): __Dispatch_Table.addRecentComment(Lnet/sourceforge/pebble/domain/Comment;)V
    //#input(void commentAdded(CommentEvent)): event
    //#input(void commentAdded(CommentEvent)): event.__Tag
    //#input(void commentAdded(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).__Tag
    //#input(void commentAdded(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name
    //#input(void commentAdded(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).__Tag
    //#input(void commentAdded(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name
    //#input(void commentAdded(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).__Tag
    //#input(void commentAdded(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[net/sourceforge/pebble/api/event/comment/CommentEvent]
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[others]
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/api/event/comment/CommentEvent.__Dispatch_Table.getComment()Lnet/sourceforge/pebble/domain/Comment;
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[others]
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isApproved()Z
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isPending()Z
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isRejected()Z
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Response]
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[others]
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/State.PENDING
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/State.__Descendant_Table[net/sourceforge/pebble/domain/State]
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/State.__Descendant_Table[others]
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/State.__Dispatch_Table.equals(Ljava/lang/Object;)Z
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/State.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void commentAdded(CommentEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void commentAdded(CommentEvent)): this
    //#input(void commentAdded(CommentEvent)): this.__Tag
    //#input(void commentAdded(CommentEvent)): this.approvedResponses
    //#input(void commentAdded(CommentEvent)): this.pendingResponses
    //#input(void commentAdded(CommentEvent)): this.recentComments
    //#input(void commentAdded(CommentEvent)): this.rejectedResponses
    //#pre[1] (void commentAdded(CommentEvent)): event != null
    //#pre[2] (void commentAdded(CommentEvent)): event.__Tag == net/sourceforge/pebble/api/event/comment/CommentEvent
    //#pre[7] (void commentAdded(CommentEvent)): this.__Tag == net/sourceforge/pebble/domain/ResponseManager
    //#pre[3] (void commentAdded(CommentEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name != null
    //#pre[4] (void commentAdded(CommentEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name != null
    //#pre[5] (void commentAdded(CommentEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name != null
    //#pre[8] (void commentAdded(CommentEvent)): (soft) this.approvedResponses != null
    //#pre[9] (void commentAdded(CommentEvent)): (soft) this.pendingResponses != null
    //#pre[10] (void commentAdded(CommentEvent)): (soft) this.recentComments != null
    //#pre[11] (void commentAdded(CommentEvent)): (soft) this.rejectedResponses != null
    //#presumption(void commentAdded(CommentEvent)): getComment(...).state.__Tag@224 == net/sourceforge/pebble/domain/State
    //#presumption(void commentAdded(CommentEvent)): getComment(...).state@224 != null
    //#presumption(void commentAdded(CommentEvent)): net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72 != null
    //#presumption(void commentAdded(CommentEvent)): net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72.__Tag is init'ed
    //#unanalyzed(void commentAdded(CommentEvent)): Effects-of-calling:isApproved
    //#unanalyzed(void commentAdded(CommentEvent)): Effects-of-calling:java.util.SortedSet:add
    //#unanalyzed(void commentAdded(CommentEvent)): Effects-of-calling:isPending
    //#unanalyzed(void commentAdded(CommentEvent)): Effects-of-calling:isRejected
    //#unanalyzed(void commentAdded(CommentEvent)): Effects-of-calling:net.sourceforge.pebble.api.event.comment.CommentEvent:getSource
    //#unanalyzed(void commentAdded(CommentEvent)): Effects-of-calling:getState
    //#unanalyzed(void commentAdded(CommentEvent)): Effects-of-calling:java.lang.String:equals
  }
    //#responsemanager.java:225: end of method: void net.sourceforge.pebble.domain.ResponseManager.commentAdded(CommentEvent)

  /**
   * Called when a comment has been removed.
   *
   * @param event a CommentEvent instance
   */
  public void commentRemoved(CommentEvent event) {
    removeRecentComment(event.getComment());
    //#responsemanager.java:233: method: void net.sourceforge.pebble.domain.ResponseManager.commentRemoved(CommentEvent)
    //#input(void commentRemoved(CommentEvent)): __Descendant_Table[net/sourceforge/pebble/domain/ResponseManager]
    //#input(void commentRemoved(CommentEvent)): __Descendant_Table[others]
    //#input(void commentRemoved(CommentEvent)): __Dispatch_Table.removeRecentComment(Lnet/sourceforge/pebble/domain/Comment;)V
    //#input(void commentRemoved(CommentEvent)): event
    //#input(void commentRemoved(CommentEvent)): event.__Tag
    //#input(void commentRemoved(CommentEvent)): net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[net/sourceforge/pebble/api/event/comment/CommentEvent]
    //#input(void commentRemoved(CommentEvent)): net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[others]
    //#input(void commentRemoved(CommentEvent)): net/sourceforge/pebble/api/event/comment/CommentEvent.__Dispatch_Table.getComment()Lnet/sourceforge/pebble/domain/Comment;
    //#input(void commentRemoved(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void commentRemoved(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[others]
    //#input(void commentRemoved(CommentEvent)): this
    //#input(void commentRemoved(CommentEvent)): this.__Tag
    //#input(void commentRemoved(CommentEvent)): this.approvedResponses
    //#input(void commentRemoved(CommentEvent)): this.pendingResponses
    //#input(void commentRemoved(CommentEvent)): this.recentComments
    //#input(void commentRemoved(CommentEvent)): this.rejectedResponses
    //#pre[1] (void commentRemoved(CommentEvent)): event != null
    //#pre[2] (void commentRemoved(CommentEvent)): event.__Tag == net/sourceforge/pebble/api/event/comment/CommentEvent
    //#pre[4] (void commentRemoved(CommentEvent)): this.__Tag == net/sourceforge/pebble/domain/ResponseManager
    //#pre[5] (void commentRemoved(CommentEvent)): this.approvedResponses != null
    //#pre[6] (void commentRemoved(CommentEvent)): this.pendingResponses != null
    //#pre[7] (void commentRemoved(CommentEvent)): this.recentComments != null
    //#pre[8] (void commentRemoved(CommentEvent)): this.rejectedResponses != null
    //#unanalyzed(void commentRemoved(CommentEvent)): Effects-of-calling:java.util.SortedSet:remove
    //#unanalyzed(void commentRemoved(CommentEvent)): Effects-of-calling:net.sourceforge.pebble.api.event.comment.CommentEvent:getSource
  }
    //#responsemanager.java:234: end of method: void net.sourceforge.pebble.domain.ResponseManager.commentRemoved(CommentEvent)

  /**
   * Called when a comment has been approved.
   *
   * @param event a CommentEvent instance
   */
  public void commentApproved(CommentEvent event) {
    removeRecentComment(event.getComment());
    //#responsemanager.java:242: method: void net.sourceforge.pebble.domain.ResponseManager.commentApproved(CommentEvent)
    //#responsemanager.java:242: ?null dereference
    //#    __Descendant_Table[this.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void commentApproved(CommentEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: __Descendant_Table[this.__Tag] != null
    //#    VN: __Descendant_Table[this.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#input(void commentApproved(CommentEvent)): __Descendant_Table[net/sourceforge/pebble/domain/ResponseManager]
    //#input(void commentApproved(CommentEvent)): __Descendant_Table[others]
    //#input(void commentApproved(CommentEvent)): __Dispatch_Table.addRecentComment(Lnet/sourceforge/pebble/domain/Comment;)V
    //#input(void commentApproved(CommentEvent)): __Dispatch_Table.removeRecentComment(Lnet/sourceforge/pebble/domain/Comment;)V
    //#input(void commentApproved(CommentEvent)): event
    //#input(void commentApproved(CommentEvent)): event.__Tag
    //#input(void commentApproved(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).__Tag
    //#input(void commentApproved(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name
    //#input(void commentApproved(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).__Tag
    //#input(void commentApproved(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name
    //#input(void commentApproved(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).__Tag
    //#input(void commentApproved(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[net/sourceforge/pebble/api/event/comment/CommentEvent]
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[others]
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/api/event/comment/CommentEvent.__Dispatch_Table.getComment()Lnet/sourceforge/pebble/domain/Comment;
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[others]
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isApproved()Z
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isPending()Z
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isRejected()Z
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Response]
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[others]
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/State.PENDING
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/State.__Descendant_Table[net/sourceforge/pebble/domain/State]
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/State.__Descendant_Table[others]
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/State.__Dispatch_Table.equals(Ljava/lang/Object;)Z
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/State.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void commentApproved(CommentEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void commentApproved(CommentEvent)): this
    //#input(void commentApproved(CommentEvent)): this.__Tag
    //#input(void commentApproved(CommentEvent)): this.approvedResponses
    //#input(void commentApproved(CommentEvent)): this.pendingResponses
    //#input(void commentApproved(CommentEvent)): this.recentComments
    //#input(void commentApproved(CommentEvent)): this.rejectedResponses
    //#pre[1] (void commentApproved(CommentEvent)): event != null
    //#pre[2] (void commentApproved(CommentEvent)): event.__Tag == net/sourceforge/pebble/api/event/comment/CommentEvent
    //#pre[7] (void commentApproved(CommentEvent)): this.__Tag == net/sourceforge/pebble/domain/ResponseManager
    //#pre[8] (void commentApproved(CommentEvent)): this.approvedResponses != null
    //#pre[9] (void commentApproved(CommentEvent)): this.pendingResponses != null
    //#pre[10] (void commentApproved(CommentEvent)): this.recentComments != null
    //#pre[11] (void commentApproved(CommentEvent)): this.rejectedResponses != null
    //#pre[3] (void commentApproved(CommentEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name != null
    //#pre[4] (void commentApproved(CommentEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name != null
    //#pre[5] (void commentApproved(CommentEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name != null
    //#presumption(void commentApproved(CommentEvent)): getComment(...).state.__Tag@243 == net/sourceforge/pebble/domain/State
    //#presumption(void commentApproved(CommentEvent)): getComment(...).state@243 != null
    //#presumption(void commentApproved(CommentEvent)): net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72 != null
    //#presumption(void commentApproved(CommentEvent)): net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72.__Tag != net/sourceforge/pebble/domain/ResponseManager
    //#presumption(void commentApproved(CommentEvent)): net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72.__Tag is init'ed
    //#unanalyzed(void commentApproved(CommentEvent)): Effects-of-calling:java.util.SortedSet:remove
    //#unanalyzed(void commentApproved(CommentEvent)): Effects-of-calling:isApproved
    //#unanalyzed(void commentApproved(CommentEvent)): Effects-of-calling:java.util.SortedSet:add
    //#unanalyzed(void commentApproved(CommentEvent)): Effects-of-calling:isPending
    //#unanalyzed(void commentApproved(CommentEvent)): Effects-of-calling:isRejected
    //#unanalyzed(void commentApproved(CommentEvent)): Effects-of-calling:net.sourceforge.pebble.api.event.comment.CommentEvent:getSource
    //#unanalyzed(void commentApproved(CommentEvent)): Effects-of-calling:getState
    //#unanalyzed(void commentApproved(CommentEvent)): Effects-of-calling:java.lang.String:equals
    addRecentComment(event.getComment());
    //#responsemanager.java:243: ?null dereference
    //#    net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[event.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void commentApproved(CommentEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[event.__Tag] != null
    //#    VN: net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[event.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#responsemanager.java:243: ?null dereference
    //#    __Descendant_Table[this.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void commentApproved(CommentEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: __Descendant_Table[this.__Tag] != null
    //#    VN: __Descendant_Table[this.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#responsemanager.java:243: ?precondition failure
    //#    net/sourceforge/pebble/domain/ResponseManager.addRecentComment: comment.__Tag == net/sourceforge/pebble/domain/Comment
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void commentApproved(CommentEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72.__Tag == net/sourceforge/pebble/domain/Comment
    //#    callee: void net/sourceforge/pebble/domain/ResponseManager.addRecentComment(Comment)
    //#    callee assertion: comment.__Tag == net/sourceforge/pebble/domain/Comment
    //#    callee file: responsemanager.java
    //#    callee precondition index: [2]
    //#    callee srcpos: 168
    //#    VN: net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72.__Tag
    //#    Expected: {793_344}
    //#    Bad: {801_280}
    //#    Attribs:  Int  Exp singleton  Bad singleton  Bad > Exp
  }
    //#responsemanager.java:244: end of method: void net.sourceforge.pebble.domain.ResponseManager.commentApproved(CommentEvent)

  /**
   * Called when a comment has been rejected.
   *
   * @param event a CommentEvent instance
   */
  public void commentRejected(CommentEvent event) {
    removeRecentComment(event.getComment());
    //#responsemanager.java:252: method: void net.sourceforge.pebble.domain.ResponseManager.commentRejected(CommentEvent)
    //#responsemanager.java:252: ?null dereference
    //#    __Descendant_Table[this.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void commentRejected(CommentEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: __Descendant_Table[this.__Tag] != null
    //#    VN: __Descendant_Table[this.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#input(void commentRejected(CommentEvent)): __Descendant_Table[net/sourceforge/pebble/domain/ResponseManager]
    //#input(void commentRejected(CommentEvent)): __Descendant_Table[others]
    //#input(void commentRejected(CommentEvent)): __Dispatch_Table.addRecentComment(Lnet/sourceforge/pebble/domain/Comment;)V
    //#input(void commentRejected(CommentEvent)): __Dispatch_Table.removeRecentComment(Lnet/sourceforge/pebble/domain/Comment;)V
    //#input(void commentRejected(CommentEvent)): event
    //#input(void commentRejected(CommentEvent)): event.__Tag
    //#input(void commentRejected(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).__Tag
    //#input(void commentRejected(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name
    //#input(void commentRejected(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).__Tag
    //#input(void commentRejected(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name
    //#input(void commentRejected(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).__Tag
    //#input(void commentRejected(CommentEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[net/sourceforge/pebble/api/event/comment/CommentEvent]
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[others]
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/api/event/comment/CommentEvent.__Dispatch_Table.getComment()Lnet/sourceforge/pebble/domain/Comment;
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Descendant_Table[others]
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isApproved()Z
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isPending()Z
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.isRejected()Z
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Response]
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[others]
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/State.PENDING
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/State.__Descendant_Table[net/sourceforge/pebble/domain/State]
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/State.__Descendant_Table[others]
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/State.__Dispatch_Table.equals(Ljava/lang/Object;)Z
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/State.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void commentRejected(CommentEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void commentRejected(CommentEvent)): this
    //#input(void commentRejected(CommentEvent)): this.__Tag
    //#input(void commentRejected(CommentEvent)): this.approvedResponses
    //#input(void commentRejected(CommentEvent)): this.pendingResponses
    //#input(void commentRejected(CommentEvent)): this.recentComments
    //#input(void commentRejected(CommentEvent)): this.rejectedResponses
    //#pre[1] (void commentRejected(CommentEvent)): event != null
    //#pre[2] (void commentRejected(CommentEvent)): event.__Tag == net/sourceforge/pebble/api/event/comment/CommentEvent
    //#pre[7] (void commentRejected(CommentEvent)): this.__Tag == net/sourceforge/pebble/domain/ResponseManager
    //#pre[8] (void commentRejected(CommentEvent)): this.approvedResponses != null
    //#pre[9] (void commentRejected(CommentEvent)): this.pendingResponses != null
    //#pre[10] (void commentRejected(CommentEvent)): this.recentComments != null
    //#pre[11] (void commentRejected(CommentEvent)): this.rejectedResponses != null
    //#pre[3] (void commentRejected(CommentEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name != null
    //#pre[4] (void commentRejected(CommentEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name != null
    //#pre[5] (void commentRejected(CommentEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name != null
    //#presumption(void commentRejected(CommentEvent)): getComment(...).state.__Tag@253 == net/sourceforge/pebble/domain/State
    //#presumption(void commentRejected(CommentEvent)): getComment(...).state@253 != null
    //#presumption(void commentRejected(CommentEvent)): net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72 != null
    //#presumption(void commentRejected(CommentEvent)): net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72.__Tag != net/sourceforge/pebble/domain/ResponseManager
    //#presumption(void commentRejected(CommentEvent)): net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72.__Tag is init'ed
    //#unanalyzed(void commentRejected(CommentEvent)): Effects-of-calling:java.util.SortedSet:remove
    //#unanalyzed(void commentRejected(CommentEvent)): Effects-of-calling:isApproved
    //#unanalyzed(void commentRejected(CommentEvent)): Effects-of-calling:java.util.SortedSet:add
    //#unanalyzed(void commentRejected(CommentEvent)): Effects-of-calling:isPending
    //#unanalyzed(void commentRejected(CommentEvent)): Effects-of-calling:isRejected
    //#unanalyzed(void commentRejected(CommentEvent)): Effects-of-calling:net.sourceforge.pebble.api.event.comment.CommentEvent:getSource
    //#unanalyzed(void commentRejected(CommentEvent)): Effects-of-calling:getState
    //#unanalyzed(void commentRejected(CommentEvent)): Effects-of-calling:java.lang.String:equals
    addRecentComment(event.getComment());
    //#responsemanager.java:253: ?null dereference
    //#    net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[event.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void commentRejected(CommentEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[event.__Tag] != null
    //#    VN: net/sourceforge/pebble/api/event/comment/CommentEvent.__Descendant_Table[event.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#responsemanager.java:253: ?null dereference
    //#    __Descendant_Table[this.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void commentRejected(CommentEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: __Descendant_Table[this.__Tag] != null
    //#    VN: __Descendant_Table[this.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#responsemanager.java:253: ?precondition failure
    //#    net/sourceforge/pebble/domain/ResponseManager.addRecentComment: comment.__Tag == net/sourceforge/pebble/domain/Comment
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void commentRejected(CommentEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72.__Tag == net/sourceforge/pebble/domain/Comment
    //#    callee: void net/sourceforge/pebble/domain/ResponseManager.addRecentComment(Comment)
    //#    callee assertion: comment.__Tag == net/sourceforge/pebble/domain/Comment
    //#    callee file: responsemanager.java
    //#    callee precondition index: [2]
    //#    callee srcpos: 168
    //#    VN: net.sourceforge.pebble.api.event.comment.CommentEvent:getSource(...)@72.__Tag
    //#    Expected: {793_344}
    //#    Bad: {801_280}
    //#    Attribs:  Int  Exp singleton  Bad singleton  Bad > Exp
  }
    //#responsemanager.java:254: end of method: void net.sourceforge.pebble.domain.ResponseManager.commentRejected(CommentEvent)

  /**
   * Called when a TrackBack has been added.
   *
   * @param event a TrackBackEvent instance
   */
  public void trackBackAdded(TrackBackEvent event) {
    addRecentTrackBack(event.getTrackBack());
    //#responsemanager.java:262: method: void net.sourceforge.pebble.domain.ResponseManager.trackBackAdded(TrackBackEvent)
    //#responsemanager.java:262: ?null dereference
    //#    __Descendant_Table[this.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void trackBackAdded(TrackBackEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: __Descendant_Table[this.__Tag] != null
    //#    VN: __Descendant_Table[this.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#input(void trackBackAdded(TrackBackEvent)): __Descendant_Table[net/sourceforge/pebble/domain/ResponseManager]
    //#input(void trackBackAdded(TrackBackEvent)): __Descendant_Table[others]
    //#input(void trackBackAdded(TrackBackEvent)): __Dispatch_Table.addRecentTrackBack(Lnet/sourceforge/pebble/domain/TrackBack;)V
    //#input(void trackBackAdded(TrackBackEvent)): event
    //#input(void trackBackAdded(TrackBackEvent)): event.__Tag
    //#input(void trackBackAdded(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).__Tag
    //#input(void trackBackAdded(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name
    //#input(void trackBackAdded(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).__Tag
    //#input(void trackBackAdded(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name
    //#input(void trackBackAdded(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).__Tag
    //#input(void trackBackAdded(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[net/sourceforge/pebble/api/event/trackback/TrackBackEvent]
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[others]
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Dispatch_Table.getTrackBack()Lnet/sourceforge/pebble/domain/TrackBack;
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Response]
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[others]
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/State.PENDING
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/State.__Descendant_Table[net/sourceforge/pebble/domain/State]
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/State.__Descendant_Table[others]
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/State.__Dispatch_Table.equals(Ljava/lang/Object;)Z
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/State.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[others]
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isApproved()Z
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isPending()Z
    //#input(void trackBackAdded(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isRejected()Z
    //#input(void trackBackAdded(TrackBackEvent)): this
    //#input(void trackBackAdded(TrackBackEvent)): this.__Tag
    //#input(void trackBackAdded(TrackBackEvent)): this.approvedResponses
    //#input(void trackBackAdded(TrackBackEvent)): this.pendingResponses
    //#input(void trackBackAdded(TrackBackEvent)): this.recentTrackBacks
    //#input(void trackBackAdded(TrackBackEvent)): this.rejectedResponses
    //#pre[1] (void trackBackAdded(TrackBackEvent)): event != null
    //#pre[2] (void trackBackAdded(TrackBackEvent)): event.__Tag == net/sourceforge/pebble/api/event/trackback/TrackBackEvent
    //#pre[7] (void trackBackAdded(TrackBackEvent)): this.__Tag == net/sourceforge/pebble/domain/ResponseManager
    //#pre[3] (void trackBackAdded(TrackBackEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name != null
    //#pre[4] (void trackBackAdded(TrackBackEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name != null
    //#pre[5] (void trackBackAdded(TrackBackEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name != null
    //#pre[8] (void trackBackAdded(TrackBackEvent)): (soft) this.approvedResponses != null
    //#pre[9] (void trackBackAdded(TrackBackEvent)): (soft) this.pendingResponses != null
    //#pre[10] (void trackBackAdded(TrackBackEvent)): (soft) this.recentTrackBacks != null
    //#pre[11] (void trackBackAdded(TrackBackEvent)): (soft) this.rejectedResponses != null
    //#presumption(void trackBackAdded(TrackBackEvent)): getTrackBack(...).state.__Tag@262 == net/sourceforge/pebble/domain/State
    //#presumption(void trackBackAdded(TrackBackEvent)): getTrackBack(...).state@262 != null
    //#presumption(void trackBackAdded(TrackBackEvent)): net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource(...)@72 != null
    //#presumption(void trackBackAdded(TrackBackEvent)): net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource(...)@72.__Tag == net/sourceforge/pebble/domain/TrackBack
    //#unanalyzed(void trackBackAdded(TrackBackEvent)): Effects-of-calling:isApproved
    //#unanalyzed(void trackBackAdded(TrackBackEvent)): Effects-of-calling:java.util.SortedSet:add
    //#unanalyzed(void trackBackAdded(TrackBackEvent)): Effects-of-calling:isPending
    //#unanalyzed(void trackBackAdded(TrackBackEvent)): Effects-of-calling:isRejected
    //#unanalyzed(void trackBackAdded(TrackBackEvent)): Effects-of-calling:getState
    //#unanalyzed(void trackBackAdded(TrackBackEvent)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(void trackBackAdded(TrackBackEvent)): Effects-of-calling:net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource
  }
    //#responsemanager.java:263: end of method: void net.sourceforge.pebble.domain.ResponseManager.trackBackAdded(TrackBackEvent)

  /**
   * Called when a TrackBack has been removed.
   *
   * @param event a TrackBackEvent instance
   */
  public void trackBackRemoved(TrackBackEvent event) {
    removeRecentTrackBack(event.getTrackBack());
    //#responsemanager.java:271: method: void net.sourceforge.pebble.domain.ResponseManager.trackBackRemoved(TrackBackEvent)
    //#input(void trackBackRemoved(TrackBackEvent)): __Descendant_Table[net/sourceforge/pebble/domain/ResponseManager]
    //#input(void trackBackRemoved(TrackBackEvent)): __Descendant_Table[others]
    //#input(void trackBackRemoved(TrackBackEvent)): __Dispatch_Table.removeRecentTrackBack(Lnet/sourceforge/pebble/domain/TrackBack;)V
    //#input(void trackBackRemoved(TrackBackEvent)): event
    //#input(void trackBackRemoved(TrackBackEvent)): event.__Tag
    //#input(void trackBackRemoved(TrackBackEvent)): net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[net/sourceforge/pebble/api/event/trackback/TrackBackEvent]
    //#input(void trackBackRemoved(TrackBackEvent)): net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[others]
    //#input(void trackBackRemoved(TrackBackEvent)): net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Dispatch_Table.getTrackBack()Lnet/sourceforge/pebble/domain/TrackBack;
    //#input(void trackBackRemoved(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void trackBackRemoved(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[others]
    //#input(void trackBackRemoved(TrackBackEvent)): this
    //#input(void trackBackRemoved(TrackBackEvent)): this.__Tag
    //#input(void trackBackRemoved(TrackBackEvent)): this.approvedResponses
    //#input(void trackBackRemoved(TrackBackEvent)): this.pendingResponses
    //#input(void trackBackRemoved(TrackBackEvent)): this.recentTrackBacks
    //#input(void trackBackRemoved(TrackBackEvent)): this.rejectedResponses
    //#pre[1] (void trackBackRemoved(TrackBackEvent)): event != null
    //#pre[2] (void trackBackRemoved(TrackBackEvent)): event.__Tag == net/sourceforge/pebble/api/event/trackback/TrackBackEvent
    //#pre[4] (void trackBackRemoved(TrackBackEvent)): this.__Tag == net/sourceforge/pebble/domain/ResponseManager
    //#pre[5] (void trackBackRemoved(TrackBackEvent)): this.approvedResponses != null
    //#pre[6] (void trackBackRemoved(TrackBackEvent)): this.pendingResponses != null
    //#pre[7] (void trackBackRemoved(TrackBackEvent)): this.recentTrackBacks != null
    //#pre[8] (void trackBackRemoved(TrackBackEvent)): this.rejectedResponses != null
    //#unanalyzed(void trackBackRemoved(TrackBackEvent)): Effects-of-calling:java.util.SortedSet:remove
    //#unanalyzed(void trackBackRemoved(TrackBackEvent)): Effects-of-calling:net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource
  }
    //#responsemanager.java:272: end of method: void net.sourceforge.pebble.domain.ResponseManager.trackBackRemoved(TrackBackEvent)

  /**
   * Called when a TrackBack has been approved.
   *
   * @param event a TrackBackEvent instance
   */
  public void trackBackApproved(TrackBackEvent event) {
    removeRecentTrackBack(event.getTrackBack());
    //#responsemanager.java:280: method: void net.sourceforge.pebble.domain.ResponseManager.trackBackApproved(TrackBackEvent)
    //#responsemanager.java:280: ?null dereference
    //#    __Descendant_Table[this.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void trackBackApproved(TrackBackEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: __Descendant_Table[this.__Tag] != null
    //#    VN: __Descendant_Table[this.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#input(void trackBackApproved(TrackBackEvent)): __Descendant_Table[net/sourceforge/pebble/domain/ResponseManager]
    //#input(void trackBackApproved(TrackBackEvent)): __Descendant_Table[others]
    //#input(void trackBackApproved(TrackBackEvent)): __Dispatch_Table.addRecentTrackBack(Lnet/sourceforge/pebble/domain/TrackBack;)V
    //#input(void trackBackApproved(TrackBackEvent)): __Dispatch_Table.removeRecentTrackBack(Lnet/sourceforge/pebble/domain/TrackBack;)V
    //#input(void trackBackApproved(TrackBackEvent)): event
    //#input(void trackBackApproved(TrackBackEvent)): event.__Tag
    //#input(void trackBackApproved(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).__Tag
    //#input(void trackBackApproved(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name
    //#input(void trackBackApproved(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).__Tag
    //#input(void trackBackApproved(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name
    //#input(void trackBackApproved(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).__Tag
    //#input(void trackBackApproved(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[net/sourceforge/pebble/api/event/trackback/TrackBackEvent]
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[others]
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Dispatch_Table.getTrackBack()Lnet/sourceforge/pebble/domain/TrackBack;
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Response]
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[others]
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/State.PENDING
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/State.__Descendant_Table[net/sourceforge/pebble/domain/State]
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/State.__Descendant_Table[others]
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/State.__Dispatch_Table.equals(Ljava/lang/Object;)Z
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/State.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[others]
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isApproved()Z
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isPending()Z
    //#input(void trackBackApproved(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isRejected()Z
    //#input(void trackBackApproved(TrackBackEvent)): this
    //#input(void trackBackApproved(TrackBackEvent)): this.__Tag
    //#input(void trackBackApproved(TrackBackEvent)): this.approvedResponses
    //#input(void trackBackApproved(TrackBackEvent)): this.pendingResponses
    //#input(void trackBackApproved(TrackBackEvent)): this.recentTrackBacks
    //#input(void trackBackApproved(TrackBackEvent)): this.rejectedResponses
    //#pre[1] (void trackBackApproved(TrackBackEvent)): event != null
    //#pre[2] (void trackBackApproved(TrackBackEvent)): event.__Tag == net/sourceforge/pebble/api/event/trackback/TrackBackEvent
    //#pre[7] (void trackBackApproved(TrackBackEvent)): this.__Tag == net/sourceforge/pebble/domain/ResponseManager
    //#pre[8] (void trackBackApproved(TrackBackEvent)): this.approvedResponses != null
    //#pre[9] (void trackBackApproved(TrackBackEvent)): this.pendingResponses != null
    //#pre[10] (void trackBackApproved(TrackBackEvent)): this.recentTrackBacks != null
    //#pre[11] (void trackBackApproved(TrackBackEvent)): this.rejectedResponses != null
    //#pre[3] (void trackBackApproved(TrackBackEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name != null
    //#pre[4] (void trackBackApproved(TrackBackEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name != null
    //#pre[5] (void trackBackApproved(TrackBackEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name != null
    //#presumption(void trackBackApproved(TrackBackEvent)): getTrackBack(...).state.__Tag@281 == net/sourceforge/pebble/domain/State
    //#presumption(void trackBackApproved(TrackBackEvent)): getTrackBack(...).state@281 != null
    //#presumption(void trackBackApproved(TrackBackEvent)): net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource(...)@72 != null
    //#presumption(void trackBackApproved(TrackBackEvent)): net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource(...)@72.__Tag != net/sourceforge/pebble/domain/ResponseManager
    //#presumption(void trackBackApproved(TrackBackEvent)): net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource(...)@72.__Tag is init'ed
    //#unanalyzed(void trackBackApproved(TrackBackEvent)): Effects-of-calling:java.util.SortedSet:remove
    //#unanalyzed(void trackBackApproved(TrackBackEvent)): Effects-of-calling:isApproved
    //#unanalyzed(void trackBackApproved(TrackBackEvent)): Effects-of-calling:java.util.SortedSet:add
    //#unanalyzed(void trackBackApproved(TrackBackEvent)): Effects-of-calling:isPending
    //#unanalyzed(void trackBackApproved(TrackBackEvent)): Effects-of-calling:isRejected
    //#unanalyzed(void trackBackApproved(TrackBackEvent)): Effects-of-calling:getState
    //#unanalyzed(void trackBackApproved(TrackBackEvent)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(void trackBackApproved(TrackBackEvent)): Effects-of-calling:net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource
    addRecentTrackBack(event.getTrackBack());
    //#responsemanager.java:281: ?null dereference
    //#    net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[event.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void trackBackApproved(TrackBackEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[event.__Tag] != null
    //#    VN: net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[event.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#responsemanager.java:281: ?null dereference
    //#    __Descendant_Table[this.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void trackBackApproved(TrackBackEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: __Descendant_Table[this.__Tag] != null
    //#    VN: __Descendant_Table[this.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#responsemanager.java:281: ?precondition failure
    //#    net/sourceforge/pebble/domain/ResponseManager.addRecentTrackBack: trackBack.__Tag == net/sourceforge/pebble/domain/TrackBack
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void trackBackApproved(TrackBackEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource(...)@72.__Tag == net/sourceforge/pebble/domain/TrackBack
    //#    callee: void net/sourceforge/pebble/domain/ResponseManager.addRecentTrackBack(TrackBack)
    //#    callee assertion: trackBack.__Tag == net/sourceforge/pebble/domain/TrackBack
    //#    callee file: responsemanager.java
    //#    callee precondition index: [10]
    //#    callee srcpos: 196
    //#    VN: net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource(...)@72.__Tag
    //#    Expected: {804_352}
    //#    Bad: {801_280}
    //#    Attribs:  Int  Exp singleton  Bad singleton  Bad < Exp
  }
    //#responsemanager.java:282: end of method: void net.sourceforge.pebble.domain.ResponseManager.trackBackApproved(TrackBackEvent)

  /**
   * Called when a TrackBack has been rejected.
   *
   * @param event a TrackBackEvent instance
   */
  public void trackBackRejected(TrackBackEvent event) {
    removeRecentTrackBack(event.getTrackBack());
    //#responsemanager.java:290: method: void net.sourceforge.pebble.domain.ResponseManager.trackBackRejected(TrackBackEvent)
    //#responsemanager.java:290: ?null dereference
    //#    __Descendant_Table[this.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void trackBackRejected(TrackBackEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: __Descendant_Table[this.__Tag] != null
    //#    VN: __Descendant_Table[this.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#input(void trackBackRejected(TrackBackEvent)): __Descendant_Table[net/sourceforge/pebble/domain/ResponseManager]
    //#input(void trackBackRejected(TrackBackEvent)): __Descendant_Table[others]
    //#input(void trackBackRejected(TrackBackEvent)): __Dispatch_Table.addRecentTrackBack(Lnet/sourceforge/pebble/domain/TrackBack;)V
    //#input(void trackBackRejected(TrackBackEvent)): __Dispatch_Table.removeRecentTrackBack(Lnet/sourceforge/pebble/domain/TrackBack;)V
    //#input(void trackBackRejected(TrackBackEvent)): event
    //#input(void trackBackRejected(TrackBackEvent)): event.__Tag
    //#input(void trackBackRejected(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).__Tag
    //#input(void trackBackRejected(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name
    //#input(void trackBackRejected(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).__Tag
    //#input(void trackBackRejected(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name
    //#input(void trackBackRejected(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).__Tag
    //#input(void trackBackRejected(TrackBackEvent)): net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[net/sourceforge/pebble/api/event/trackback/TrackBackEvent]
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[others]
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Dispatch_Table.getTrackBack()Lnet/sourceforge/pebble/domain/TrackBack;
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/Comment.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Comment]
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/Response]
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Descendant_Table[others]
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/Response.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/State.APPROVED
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/State.PENDING
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/State.REJECTED
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/State.__Descendant_Table[net/sourceforge/pebble/domain/State]
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/State.__Descendant_Table[others]
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/State.__Dispatch_Table.equals(Ljava/lang/Object;)Z
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/State.__Dispatch_Table.getName()Ljava/lang/String;
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[net/sourceforge/pebble/domain/TrackBack]
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Descendant_Table[others]
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.getState()Lnet/sourceforge/pebble/domain/State;
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isApproved()Z
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isPending()Z
    //#input(void trackBackRejected(TrackBackEvent)): net/sourceforge/pebble/domain/TrackBack.__Dispatch_Table.isRejected()Z
    //#input(void trackBackRejected(TrackBackEvent)): this
    //#input(void trackBackRejected(TrackBackEvent)): this.__Tag
    //#input(void trackBackRejected(TrackBackEvent)): this.approvedResponses
    //#input(void trackBackRejected(TrackBackEvent)): this.pendingResponses
    //#input(void trackBackRejected(TrackBackEvent)): this.recentTrackBacks
    //#input(void trackBackRejected(TrackBackEvent)): this.rejectedResponses
    //#pre[1] (void trackBackRejected(TrackBackEvent)): event != null
    //#pre[2] (void trackBackRejected(TrackBackEvent)): event.__Tag == net/sourceforge/pebble/api/event/trackback/TrackBackEvent
    //#pre[7] (void trackBackRejected(TrackBackEvent)): this.__Tag == net/sourceforge/pebble/domain/ResponseManager
    //#pre[8] (void trackBackRejected(TrackBackEvent)): this.approvedResponses != null
    //#pre[9] (void trackBackRejected(TrackBackEvent)): this.pendingResponses != null
    //#pre[10] (void trackBackRejected(TrackBackEvent)): this.recentTrackBacks != null
    //#pre[11] (void trackBackRejected(TrackBackEvent)): this.rejectedResponses != null
    //#pre[3] (void trackBackRejected(TrackBackEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#1).name != null
    //#pre[4] (void trackBackRejected(TrackBackEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#2).name != null
    //#pre[5] (void trackBackRejected(TrackBackEvent)): (soft) net.sourceforge.pebble.domain.State__static_init.new State(State__static_init#3).name != null
    //#presumption(void trackBackRejected(TrackBackEvent)): getTrackBack(...).state.__Tag@291 == net/sourceforge/pebble/domain/State
    //#presumption(void trackBackRejected(TrackBackEvent)): getTrackBack(...).state@291 != null
    //#presumption(void trackBackRejected(TrackBackEvent)): net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource(...)@72 != null
    //#presumption(void trackBackRejected(TrackBackEvent)): net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource(...)@72.__Tag != net/sourceforge/pebble/domain/ResponseManager
    //#presumption(void trackBackRejected(TrackBackEvent)): net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource(...)@72.__Tag is init'ed
    //#unanalyzed(void trackBackRejected(TrackBackEvent)): Effects-of-calling:java.util.SortedSet:remove
    //#unanalyzed(void trackBackRejected(TrackBackEvent)): Effects-of-calling:isApproved
    //#unanalyzed(void trackBackRejected(TrackBackEvent)): Effects-of-calling:java.util.SortedSet:add
    //#unanalyzed(void trackBackRejected(TrackBackEvent)): Effects-of-calling:isPending
    //#unanalyzed(void trackBackRejected(TrackBackEvent)): Effects-of-calling:isRejected
    //#unanalyzed(void trackBackRejected(TrackBackEvent)): Effects-of-calling:getState
    //#unanalyzed(void trackBackRejected(TrackBackEvent)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(void trackBackRejected(TrackBackEvent)): Effects-of-calling:net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource
    addRecentTrackBack(event.getTrackBack());
    //#responsemanager.java:291: ?null dereference
    //#    net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[event.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void trackBackRejected(TrackBackEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[event.__Tag] != null
    //#    VN: net/sourceforge/pebble/api/event/trackback/TrackBackEvent.__Descendant_Table[event.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#responsemanager.java:291: ?null dereference
    //#    __Descendant_Table[this.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void trackBackRejected(TrackBackEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: __Descendant_Table[this.__Tag] != null
    //#    VN: __Descendant_Table[this.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#responsemanager.java:291: ?precondition failure
    //#    net/sourceforge/pebble/domain/ResponseManager.addRecentTrackBack: trackBack.__Tag == net/sourceforge/pebble/domain/TrackBack
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.ResponseManager
    //#    method: void trackBackRejected(TrackBackEvent)
    //#    basic block: Entry_BB_1
    //#    assertion: net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource(...)@72.__Tag == net/sourceforge/pebble/domain/TrackBack
    //#    callee: void net/sourceforge/pebble/domain/ResponseManager.addRecentTrackBack(TrackBack)
    //#    callee assertion: trackBack.__Tag == net/sourceforge/pebble/domain/TrackBack
    //#    callee file: responsemanager.java
    //#    callee precondition index: [10]
    //#    callee srcpos: 196
    //#    VN: net.sourceforge.pebble.api.event.trackback.TrackBackEvent:getSource(...)@72.__Tag
    //#    Expected: {804_352}
    //#    Bad: {801_280}
    //#    Attribs:  Int  Exp singleton  Bad singleton  Bad < Exp
  }
    //#responsemanager.java:292: end of method: void net.sourceforge.pebble.domain.ResponseManager.trackBackRejected(TrackBackEvent)

  /**
   * Gets the number of responses.
   */
  public int getNumberOfResponses() {
    return approvedResponses.size() + pendingResponses.size() + rejectedResponses.size();
    //#responsemanager.java:298: method: int net.sourceforge.pebble.domain.ResponseManager.getNumberOfResponses()
    //#input(int getNumberOfResponses()): this
    //#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.approvedResponses != null
    //#pre[3] (int getNumberOfResponses()): this.pendingResponses != null
    //#pre[4] (int getNumberOfResponses()): this.rejectedResponses != null
    //#presumption(int getNumberOfResponses()): java.util.SortedSet:size(...)@298 + java.util.SortedSet:size(...)@298 in -4_294_967_296..6_442_450_943
    //#presumption(int getNumberOfResponses()): java.util.SortedSet:size(...)@298 + java.util.SortedSet:size(...)@298 + java.util.SortedSet:size(...)@298 in -2_147_483_648..4_294_967_295
    //#post(int getNumberOfResponses()): (soft) init'ed(return_value)
    //#responsemanager.java:298: end of method: int net.sourceforge.pebble.domain.ResponseManager.getNumberOfResponses()
  }

}
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Descendant_Table[net/sourceforge/pebble/domain/ResponseManager]
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.addRecentComment(Lnet/sourceforge/pebble/domain/Comment;)V
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.addRecentTrackBack(Lnet/sourceforge/pebble/domain/TrackBack;)V
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.commentAdded(Lnet/sourceforge/pebble/api/event/comment/CommentEvent;)V
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.commentApproved(Lnet/sourceforge/pebble/api/event/comment/CommentEvent;)V
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.commentRejected(Lnet/sourceforge/pebble/api/event/comment/CommentEvent;)V
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.commentRemoved(Lnet/sourceforge/pebble/api/event/comment/CommentEvent;)V
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getNumberOfApprovedResponses()I
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getNumberOfPendingResponses()I
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getNumberOfRejectedResponses()I
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getNumberOfResponses()I
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getPendingResponses()Ljava/util/Collection;
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getRecentComments()Ljava/util/Collection;
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getRecentResponses()Ljava/util/Collection;
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getRecentTrackBacks()Ljava/util/Collection;
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getRejectedResponses()Ljava/util/Collection;
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.removeRecentComment(Lnet/sourceforge/pebble/domain/Comment;)V
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.removeRecentTrackBack(Lnet/sourceforge/pebble/domain/TrackBack;)V
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.trackBackAdded(Lnet/sourceforge/pebble/api/event/trackback/TrackBackEvent;)V
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.trackBackApproved(Lnet/sourceforge/pebble/api/event/trackback/TrackBackEvent;)V
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.trackBackRejected(Lnet/sourceforge/pebble/api/event/trackback/TrackBackEvent;)V
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.trackBackRemoved(Lnet/sourceforge/pebble/api/event/trackback/TrackBackEvent;)V
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): net/sourceforge/pebble/api/event/comment/CommentListener.__Descendant_Table[net/sourceforge/pebble/domain/ResponseManager]
    //#output(net.sourceforge.pebble.domain.ResponseManager__static_init): net/sourceforge/pebble/api/event/trackback/TrackBackListener.__Descendant_Table[net/sourceforge/pebble/domain/ResponseManager]
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Descendant_Table[net/sourceforge/pebble/domain/ResponseManager] == &__Dispatch_Table
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): net/sourceforge/pebble/api/event/comment/CommentListener.__Descendant_Table[net/sourceforge/pebble/domain/ResponseManager] == &__Dispatch_Table
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): net/sourceforge/pebble/api/event/trackback/TrackBackListener.__Descendant_Table[net/sourceforge/pebble/domain/ResponseManager] == &__Dispatch_Table
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.addRecentComment(Lnet/sourceforge/pebble/domain/Comment;)V == &addRecentComment
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.addRecentTrackBack(Lnet/sourceforge/pebble/domain/TrackBack;)V == &addRecentTrackBack
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.commentAdded(Lnet/sourceforge/pebble/api/event/comment/CommentEvent;)V == &commentAdded
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.commentApproved(Lnet/sourceforge/pebble/api/event/comment/CommentEvent;)V == &commentApproved
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.commentRejected(Lnet/sourceforge/pebble/api/event/comment/CommentEvent;)V == &commentRejected
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.commentRemoved(Lnet/sourceforge/pebble/api/event/comment/CommentEvent;)V == &commentRemoved
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getNumberOfApprovedResponses()I == &getNumberOfApprovedResponses
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getNumberOfPendingResponses()I == &getNumberOfPendingResponses
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getNumberOfRejectedResponses()I == &getNumberOfRejectedResponses
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getNumberOfResponses()I == &getNumberOfResponses
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getPendingResponses()Ljava/util/Collection; == &getPendingResponses
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getRecentComments()Ljava/util/Collection; == &getRecentComments
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getRecentResponses()Ljava/util/Collection; == &getRecentResponses
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getRecentTrackBacks()Ljava/util/Collection; == &getRecentTrackBacks
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.getRejectedResponses()Ljava/util/Collection; == &getRejectedResponses
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.removeRecentComment(Lnet/sourceforge/pebble/domain/Comment;)V == &removeRecentComment
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.removeRecentTrackBack(Lnet/sourceforge/pebble/domain/TrackBack;)V == &removeRecentTrackBack
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.trackBackAdded(Lnet/sourceforge/pebble/api/event/trackback/TrackBackEvent;)V == &trackBackAdded
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.trackBackApproved(Lnet/sourceforge/pebble/api/event/trackback/TrackBackEvent;)V == &trackBackApproved
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.trackBackRejected(Lnet/sourceforge/pebble/api/event/trackback/TrackBackEvent;)V == &trackBackRejected
    //#post(net.sourceforge.pebble.domain.ResponseManager__static_init): __Dispatch_Table.trackBackRemoved(Lnet/sourceforge/pebble/api/event/trackback/TrackBackEvent;)V == &trackBackRemoved
    //#responsemanager.java:: end of method: net.sourceforge.pebble.domain.ResponseManager.net.sourceforge.pebble.domain.ResponseManager__static_init
    //#responsemanager.java:: end of class: net.sourceforge.pebble.domain.ResponseManager
