//# 13 errors, 984 messages
//#
/*
    //#categorybuilder.java:1:1: class: net.sourceforge.pebble.domain.CategoryBuilder
    //#categorybuilder.java:1:1: method: net.sourceforge.pebble.domain.CategoryBuilder.net.sourceforge.pebble.domain.CategoryBuilder__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 java.util.ArrayList;
import java.util.Collections;
import java.util.Iterator;
import java.util.List;

import net.sourceforge.pebble.util.I18n;

/**
 * A class to manage blog categories.
 *
 * @author    Simon Brown
 */
public class CategoryBuilder {

  /** the category separator */
  private static final String CATEGORY_SEPARATOR = "/";

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

  /** the root category */
  private Category rootCategory;

  /**
   * Creates a new instance.
   */
  public CategoryBuilder(Blog blog) {
    //#categorybuilder.java:60: method: void net.sourceforge.pebble.domain.CategoryBuilder.net.sourceforge.pebble.domain.CategoryBuilder(Blog)
    //#input(void net.sourceforge.pebble.domain.CategoryBuilder(Blog)): blog
    //#input(void net.sourceforge.pebble.domain.CategoryBuilder(Blog)): this
    //#output(void net.sourceforge.pebble.domain.CategoryBuilder(Blog)): this.blog
    //#post(void net.sourceforge.pebble.domain.CategoryBuilder(Blog)): this.blog == blog
    //#post(void net.sourceforge.pebble.domain.CategoryBuilder(Blog)): init'ed(this.blog)
    this.blog = blog;
  }
    //#categorybuilder.java:62: end of method: void net.sourceforge.pebble.domain.CategoryBuilder.net.sourceforge.pebble.domain.CategoryBuilder(Blog)

  /**
   * Creates a new instance.
   */
  public CategoryBuilder(Blog blog, Category rootCategory) {
    //#categorybuilder.java:67: method: void net.sourceforge.pebble.domain.CategoryBuilder.net.sourceforge.pebble.domain.CategoryBuilder(Blog, Category)
    //#input(void net.sourceforge.pebble.domain.CategoryBuilder(Blog, Category)): blog
    //#input(void net.sourceforge.pebble.domain.CategoryBuilder(Blog, Category)): rootCategory
    //#input(void net.sourceforge.pebble.domain.CategoryBuilder(Blog, Category)): this
    //#output(void net.sourceforge.pebble.domain.CategoryBuilder(Blog, Category)): this.blog
    //#output(void net.sourceforge.pebble.domain.CategoryBuilder(Blog, Category)): this.rootCategory
    //#post(void net.sourceforge.pebble.domain.CategoryBuilder(Blog, Category)): this.blog == blog
    //#post(void net.sourceforge.pebble.domain.CategoryBuilder(Blog, Category)): init'ed(this.blog)
    //#post(void net.sourceforge.pebble.domain.CategoryBuilder(Blog, Category)): this.rootCategory == rootCategory
    //#post(void net.sourceforge.pebble.domain.CategoryBuilder(Blog, Category)): init'ed(this.rootCategory)
    this.blog = blog;
    this.rootCategory = rootCategory;
  }
    //#categorybuilder.java:70: end of method: void net.sourceforge.pebble.domain.CategoryBuilder.net.sourceforge.pebble.domain.CategoryBuilder(Blog, Category)

  /**
   * Adds a category.
   *
   * @param category    a Category instance
   */
  public void addCategory(Category category) {
    category.setBlog(blog);
    //#categorybuilder.java:78: method: void net.sourceforge.pebble.domain.CategoryBuilder.addCategory(Category)
    //#input(void addCategory(Category)): __Descendant_Table[net/sourceforge/pebble/domain/CategoryBuilder]
    //#input(void addCategory(Category)): __Descendant_Table[others]
    //#input(void addCategory(Category)): __Dispatch_Table.addCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(void addCategory(Category)): __Dispatch_Table.getRootCategory()Lnet/sourceforge/pebble/domain/Category;
    //#input(void addCategory(Category)): category
    //#input(void addCategory(Category)): category.__Tag
    //#input(void addCategory(Category)): category.id
    //#input(void addCategory(Category)): net/sourceforge/pebble/domain/Category.__Descendant_Table[net/sourceforge/pebble/domain/Category]
    //#input(void addCategory(Category)): net/sourceforge/pebble/domain/Category.__Descendant_Table[others]
    //#input(void addCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.addSubCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(void addCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getId()Ljava/lang/String;
    //#input(void addCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getSubCategories()Ljava/util/List;
    //#input(void addCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.isRootCategory()Z
    //#input(void addCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setBlog(Lnet/sourceforge/pebble/domain/Blog;)V
    //#input(void addCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setId(Ljava/lang/String;)V
    //#input(void addCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setParent(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(void addCategory(Category)): this
    //#input(void addCategory(Category)): this.__Tag
    //#input(void addCategory(Category)): this.blog
    //#input(void addCategory(Category)): this.rootCategory
    //#input(void addCategory(Category)): this.rootCategory.__Tag
    //#output(void addCategory(Category)): category.blog
    //#output(void addCategory(Category)): category.parent
    //#output(void addCategory(Category)): new ArrayList(Category#1) num objects
    //#output(void addCategory(Category)): new ArrayList(Category#2) num objects
    //#output(void addCategory(Category)): new ArrayList(Category#3) num objects
    //#output(void addCategory(Category)): new Category(getCategory#2) num objects
    //#output(void addCategory(Category)): new Category(getCategory#2).__Tag
    //#output(void addCategory(Category)): new Category(getCategory#2).blog
    //#output(void addCategory(Category)): new Category(getCategory#2).blogEntries
    //#output(void addCategory(Category)): new Category(getCategory#2).id
    //#output(void addCategory(Category)): new Category(getCategory#2).name
    //#output(void addCategory(Category)): new Category(getCategory#2).parent
    //#output(void addCategory(Category)): new Category(getCategory#2).subCategories
    //#output(void addCategory(Category)): new Category(getCategory#2).tags
    //#output(void addCategory(Category)): new Category(getCategory#2).tagsAsList
    //#output(void addCategory(Category)): new Category(getCategory#3) num objects
    //#output(void addCategory(Category)): new Category(getCategory#3).__Tag
    //#output(void addCategory(Category)): new Category(getCategory#3).blog
    //#output(void addCategory(Category)): new Category(getCategory#3).blogEntries
    //#output(void addCategory(Category)): new Category(getCategory#3).id
    //#output(void addCategory(Category)): new Category(getCategory#3).name
    //#output(void addCategory(Category)): new Category(getCategory#3).parent
    //#output(void addCategory(Category)): new Category(getCategory#3).subCategories
    //#output(void addCategory(Category)): new Category(getCategory#3).tags
    //#output(void addCategory(Category)): new Category(getCategory#3).tagsAsList
    //#output(void addCategory(Category)): this.rootCategory
    //#new obj(void addCategory(Category)): new ArrayList(Category#1)
    //#new obj(void addCategory(Category)): new ArrayList(Category#2)
    //#new obj(void addCategory(Category)): new ArrayList(Category#3)
    //#new obj(void addCategory(Category)): new Category(getCategory#2)
    //#new obj(void addCategory(Category)): new Category(getCategory#3)
    //#pre[1] (void addCategory(Category)): category != null
    //#pre[3] (void addCategory(Category)): category.__Tag == net/sourceforge/pebble/domain/Category
    //#pre[4] (void addCategory(Category)): category.id != null
    //#pre[7] (void addCategory(Category)): (soft) init'ed(this.rootCategory)
    //#pre[9] (void addCategory(Category)): (soft) this.__Tag == net/sourceforge/pebble/domain/CategoryBuilder
    //#pre[10] (void addCategory(Category)): (soft) this.blog != null
    //#presumption(void addCategory(Category)): parent.__Tag == net/sourceforge/pebble/domain/Category
    //#post(void addCategory(Category)): possibly_updated(category.blog)
    //#post(void addCategory(Category)): possibly_updated(category.parent)
    //#post(void addCategory(Category)): (soft) init'ed(this.rootCategory)
    //#post(void addCategory(Category)): init'ed(new ArrayList(Category#1) num objects)
    //#post(void addCategory(Category)): init'ed(new ArrayList(Category#2) num objects)
    //#post(void addCategory(Category)): init'ed(new ArrayList(Category#3) num objects)
    //#post(void addCategory(Category)): init'ed(new Category(getCategory#2) num objects)
    //#post(void addCategory(Category)): init'ed(new Category(getCategory#2).__Tag)
    //#post(void addCategory(Category)): possibly_updated(new Category(getCategory#2).blog)
    //#post(void addCategory(Category)): init'ed(new Category(getCategory#2).blogEntries)
    //#post(void addCategory(Category)): possibly_updated(new Category(getCategory#2).id)
    //#post(void addCategory(Category)): init'ed(new Category(getCategory#2).name)
    //#post(void addCategory(Category)): possibly_updated(new Category(getCategory#2).parent)
    //#post(void addCategory(Category)): possibly_updated(new Category(getCategory#2).subCategories)
    //#post(void addCategory(Category)): init'ed(new Category(getCategory#2).tags)
    //#post(void addCategory(Category)): init'ed(new Category(getCategory#2).tagsAsList)
    //#post(void addCategory(Category)): init'ed(new Category(getCategory#3) num objects)
    //#post(void addCategory(Category)): init'ed(new Category(getCategory#3).__Tag)
    //#post(void addCategory(Category)): possibly_updated(new Category(getCategory#3).blog)
    //#post(void addCategory(Category)): init'ed(new Category(getCategory#3).blogEntries)
    //#post(void addCategory(Category)): possibly_updated(new Category(getCategory#3).id)
    //#post(void addCategory(Category)): init'ed(new Category(getCategory#3).name)
    //#post(void addCategory(Category)): possibly_updated(new Category(getCategory#3).parent)
    //#post(void addCategory(Category)): possibly_updated(new Category(getCategory#3).subCategories)
    //#post(void addCategory(Category)): init'ed(new Category(getCategory#3).tags)
    //#post(void addCategory(Category)): init'ed(new Category(getCategory#3).tagsAsList)
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:getSubCategories
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:getCategory
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:net.sourceforge.pebble.domain.Blog:getLocale
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:net.sourceforge.pebble.util.I18n:getMessage
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:net.sourceforge.pebble.domain.Category
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:addCategory
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.lang.String:length
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:getId
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:setBlog
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:isRootCategory
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:addSubCategory
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.util.Collections:unmodifiableList
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.util.List:contains
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(void addCategory(Category)): Effects-of-calling:java.util.List:add
    //#test_vector(void addCategory(Category)): java.lang.String:equals(...)@142: {0}, {1}

    if (category.isRootCategory()) {
      this.rootCategory = category;
    } else {
      Category parent = getParent(category, true);
      parent.addSubCategory(category);
    //#categorybuilder.java:84: ?null dereference
    //#    parent != null
    //#    severity: MEDIUM
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: void addCategory(Category)
    //#    basic block: bb_3
    //#    assertion: parent != null
    //#    VN: getParent(...)
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#categorybuilder.java:84: ?null dereference
    //#    net/sourceforge/pebble/domain/Category.__Descendant_Table[parent.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: void addCategory(Category)
    //#    basic block: bb_3
    //#    assertion: net/sourceforge/pebble/domain/Category.__Descendant_Table[parent.__Tag] != null
    //#    VN: net/sourceforge/pebble/domain/Category.__Descendant_Table[parent.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    }
  }
    //#categorybuilder.java:86: end of method: void net.sourceforge.pebble.domain.CategoryBuilder.addCategory(Category)

  /**
   * Removes a category.
   *
   * @param category    a Category instance
   */
  public void removeCategory(Category category) {
    Category parent = getParent(category);
    //#categorybuilder.java:94: method: void net.sourceforge.pebble.domain.CategoryBuilder.removeCategory(Category)
    //#input(void removeCategory(Category)): __Descendant_Table[net/sourceforge/pebble/domain/CategoryBuilder]
    //#input(void removeCategory(Category)): __Descendant_Table[others]
    //#input(void removeCategory(Category)): __Dispatch_Table.addCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(void removeCategory(Category)): __Dispatch_Table.getRootCategory()Lnet/sourceforge/pebble/domain/Category;
    //#input(void removeCategory(Category)): category
    //#input(void removeCategory(Category)): category.__Tag
    //#input(void removeCategory(Category)): category.id
    //#input(void removeCategory(Category)): net/sourceforge/pebble/domain/Category.__Descendant_Table[net/sourceforge/pebble/domain/Category]
    //#input(void removeCategory(Category)): net/sourceforge/pebble/domain/Category.__Descendant_Table[others]
    //#input(void removeCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.addSubCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(void removeCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getId()Ljava/lang/String;
    //#input(void removeCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getSubCategories()Ljava/util/List;
    //#input(void removeCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.isRootCategory()Z
    //#input(void removeCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.removeSubCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(void removeCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setBlog(Lnet/sourceforge/pebble/domain/Blog;)V
    //#input(void removeCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setId(Ljava/lang/String;)V
    //#input(void removeCategory(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setParent(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(void removeCategory(Category)): this
    //#input(void removeCategory(Category)): this.__Tag
    //#input(void removeCategory(Category)): this.blog
    //#input(void removeCategory(Category)): this.rootCategory
    //#input(void removeCategory(Category)): this.rootCategory.__Tag
    //#output(void removeCategory(Category)): category.parent
    //#output(void removeCategory(Category)): new ArrayList(Category#1) num objects
    //#output(void removeCategory(Category)): new ArrayList(Category#2) num objects
    //#output(void removeCategory(Category)): new ArrayList(Category#3) num objects
    //#output(void removeCategory(Category)): new Category(getCategory#2) num objects
    //#output(void removeCategory(Category)): new Category(getCategory#2).__Tag
    //#output(void removeCategory(Category)): new Category(getCategory#2).blog
    //#output(void removeCategory(Category)): new Category(getCategory#2).blogEntries
    //#output(void removeCategory(Category)): new Category(getCategory#2).id
    //#output(void removeCategory(Category)): new Category(getCategory#2).name
    //#output(void removeCategory(Category)): new Category(getCategory#2).parent
    //#output(void removeCategory(Category)): new Category(getCategory#2).subCategories
    //#output(void removeCategory(Category)): new Category(getCategory#2).tags
    //#output(void removeCategory(Category)): new Category(getCategory#2).tagsAsList
    //#output(void removeCategory(Category)): new Category(getCategory#3) num objects
    //#output(void removeCategory(Category)): new Category(getCategory#3).__Tag
    //#output(void removeCategory(Category)): new Category(getCategory#3).blog
    //#output(void removeCategory(Category)): new Category(getCategory#3).blogEntries
    //#output(void removeCategory(Category)): new Category(getCategory#3).id
    //#output(void removeCategory(Category)): new Category(getCategory#3).name
    //#output(void removeCategory(Category)): new Category(getCategory#3).parent
    //#output(void removeCategory(Category)): new Category(getCategory#3).subCategories
    //#output(void removeCategory(Category)): new Category(getCategory#3).tags
    //#output(void removeCategory(Category)): new Category(getCategory#3).tagsAsList
    //#output(void removeCategory(Category)): this.rootCategory
    //#new obj(void removeCategory(Category)): new ArrayList(Category#1)
    //#new obj(void removeCategory(Category)): new ArrayList(Category#2)
    //#new obj(void removeCategory(Category)): new ArrayList(Category#3)
    //#new obj(void removeCategory(Category)): new Category(getCategory#2)
    //#new obj(void removeCategory(Category)): new Category(getCategory#3)
    //#pre[1] (void removeCategory(Category)): category != null
    //#pre[2] (void removeCategory(Category)): category.__Tag == net/sourceforge/pebble/domain/Category
    //#pre[3] (void removeCategory(Category)): category.id != null
    //#pre[5] (void removeCategory(Category)): (soft) init'ed(this.rootCategory)
    //#pre[7] (void removeCategory(Category)): (soft) this.__Tag == net/sourceforge/pebble/domain/CategoryBuilder
    //#pre[8] (void removeCategory(Category)): (soft) this.blog != null
    //#presumption(void removeCategory(Category)): parent.__Tag == net/sourceforge/pebble/domain/Category
    //#post(void removeCategory(Category)): possibly_updated(category.parent)
    //#post(void removeCategory(Category)): init'ed(this.rootCategory)
    //#post(void removeCategory(Category)): init'ed(new ArrayList(Category#1) num objects)
    //#post(void removeCategory(Category)): init'ed(new ArrayList(Category#2) num objects)
    //#post(void removeCategory(Category)): init'ed(new ArrayList(Category#3) num objects)
    //#post(void removeCategory(Category)): init'ed(new Category(getCategory#2) num objects)
    //#post(void removeCategory(Category)): init'ed(new Category(getCategory#2).__Tag)
    //#post(void removeCategory(Category)): possibly_updated(new Category(getCategory#2).blog)
    //#post(void removeCategory(Category)): init'ed(new Category(getCategory#2).blogEntries)
    //#post(void removeCategory(Category)): possibly_updated(new Category(getCategory#2).id)
    //#post(void removeCategory(Category)): init'ed(new Category(getCategory#2).name)
    //#post(void removeCategory(Category)): possibly_updated(new Category(getCategory#2).parent)
    //#post(void removeCategory(Category)): (soft) init'ed(new Category(getCategory#2).subCategories)
    //#post(void removeCategory(Category)): init'ed(new Category(getCategory#2).tags)
    //#post(void removeCategory(Category)): init'ed(new Category(getCategory#2).tagsAsList)
    //#post(void removeCategory(Category)): init'ed(new Category(getCategory#3) num objects)
    //#post(void removeCategory(Category)): init'ed(new Category(getCategory#3).__Tag)
    //#post(void removeCategory(Category)): possibly_updated(new Category(getCategory#3).blog)
    //#post(void removeCategory(Category)): init'ed(new Category(getCategory#3).blogEntries)
    //#post(void removeCategory(Category)): possibly_updated(new Category(getCategory#3).id)
    //#post(void removeCategory(Category)): init'ed(new Category(getCategory#3).name)
    //#post(void removeCategory(Category)): possibly_updated(new Category(getCategory#3).parent)
    //#post(void removeCategory(Category)): (soft) init'ed(new Category(getCategory#3).subCategories)
    //#post(void removeCategory(Category)): init'ed(new Category(getCategory#3).tags)
    //#post(void removeCategory(Category)): init'ed(new Category(getCategory#3).tagsAsList)
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:getSubCategories
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:getCategory
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:getParent
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:net.sourceforge.pebble.domain.Blog:getLocale
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:net.sourceforge.pebble.util.I18n:getMessage
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:net.sourceforge.pebble.domain.Category
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:addCategory
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.lang.String:length
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:getId
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:setBlog
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:isRootCategory
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:addSubCategory
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.util.Collections:unmodifiableList
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.util.List:contains
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.util.List:remove
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(void removeCategory(Category)): Effects-of-calling:java.util.List:add
    parent.removeSubCategory(category);
    //#categorybuilder.java:95: ?null dereference
    //#    parent != null
    //#    severity: MEDIUM
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: void removeCategory(Category)
    //#    basic block: Entry_BB_1
    //#    assertion: parent != null
    //#    VN: getParent(...)
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#categorybuilder.java:95: ?use of default init
    //#    init'ed(parent.__Tag)
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: void removeCategory(Category)
    //#    basic block: Entry_BB_1
    //#    assertion: init'ed(parent.__Tag)
    //#    VN: parent.__Tag
    //#    Expected: {-Inf..+Inf}
    //#    Bad: {Invalid}
    //#    Attribs:  Int  Bad only invalid
    //#categorybuilder.java:95: ?null dereference
    //#    net/sourceforge/pebble/domain/Category.__Descendant_Table[parent.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: void removeCategory(Category)
    //#    basic block: Entry_BB_1
    //#    assertion: net/sourceforge/pebble/domain/Category.__Descendant_Table[parent.__Tag] != null
    //#    VN: net/sourceforge/pebble/domain/Category.__Descendant_Table[parent.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#categorybuilder.java:95: ?precondition failure
    //#    net/sourceforge/pebble/domain/Category.removeSubCategory: init'ed(this.subCategories)
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: void removeCategory(Category)
    //#    basic block: Entry_BB_1
    //#    assertion: init'ed(parent.subCategories)
    //#    callee: void net/sourceforge/pebble/domain/Category.removeSubCategory(Category)
    //#    callee assertion: init'ed(this.subCategories)
    //#    callee file: category.java
    //#    callee precondition index: [5]
    //#    callee srcpos: 218
    //#    VN: parent.subCategories
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
  }
    //#categorybuilder.java:96: end of method: void net.sourceforge.pebble.domain.CategoryBuilder.removeCategory(Category)

  /**
   * Gets (and creates if necessary), the parent of the specified category.
   *
   * @param category    the Category to find the parent of
   * @param create      true if the parent should be created if it doesn't
   *                    exist, false otherwise
   * @return  a Category instance
   *
   */
  private Category getParent(Category category, boolean create) {
    String id = category.getId();
    //#categorybuilder.java:108: method: Category net.sourceforge.pebble.domain.CategoryBuilder.getParent(Category, bool)
    //#input(Category getParent(Category, bool)): __Descendant_Table[net/sourceforge/pebble/domain/CategoryBuilder]
    //#input(Category getParent(Category, bool)): __Descendant_Table[others]
    //#input(Category getParent(Category, bool)): __Dispatch_Table.addCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getParent(Category, bool)): __Dispatch_Table.getRootCategory()Lnet/sourceforge/pebble/domain/Category;
    //#input(Category getParent(Category, bool)): category
    //#input(Category getParent(Category, bool)): category.__Tag
    //#input(Category getParent(Category, bool)): category.id
    //#input(Category getParent(Category, bool)): create
    //#input(Category getParent(Category, bool)): net/sourceforge/pebble/domain/Category.__Descendant_Table[net/sourceforge/pebble/domain/Category]
    //#input(Category getParent(Category, bool)): net/sourceforge/pebble/domain/Category.__Descendant_Table[others]
    //#input(Category getParent(Category, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.addSubCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getParent(Category, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getId()Ljava/lang/String;
    //#input(Category getParent(Category, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getSubCategories()Ljava/util/List;
    //#input(Category getParent(Category, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.isRootCategory()Z
    //#input(Category getParent(Category, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setBlog(Lnet/sourceforge/pebble/domain/Blog;)V
    //#input(Category getParent(Category, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setId(Ljava/lang/String;)V
    //#input(Category getParent(Category, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setParent(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getParent(Category, bool)): this
    //#input(Category getParent(Category, bool)): this.__Tag
    //#input(Category getParent(Category, bool)): this.blog
    //#input(Category getParent(Category, bool)): this.rootCategory
    //#input(Category getParent(Category, bool)): this.rootCategory.__Tag
    //#output(Category getParent(Category, bool)): new ArrayList(Category#1) num objects
    //#output(Category getParent(Category, bool)): new ArrayList(Category#2) num objects
    //#output(Category getParent(Category, bool)): new ArrayList(Category#3) num objects
    //#output(Category getParent(Category, bool)): new Category(getCategory#2) num objects
    //#output(Category getParent(Category, bool)): new Category(getCategory#2).__Tag
    //#output(Category getParent(Category, bool)): new Category(getCategory#2).blog
    //#output(Category getParent(Category, bool)): new Category(getCategory#2).blogEntries
    //#output(Category getParent(Category, bool)): new Category(getCategory#2).id
    //#output(Category getParent(Category, bool)): new Category(getCategory#2).name
    //#output(Category getParent(Category, bool)): new Category(getCategory#2).parent
    //#output(Category getParent(Category, bool)): new Category(getCategory#2).subCategories
    //#output(Category getParent(Category, bool)): new Category(getCategory#2).tags
    //#output(Category getParent(Category, bool)): new Category(getCategory#2).tagsAsList
    //#output(Category getParent(Category, bool)): new Category(getCategory#3) num objects
    //#output(Category getParent(Category, bool)): new Category(getCategory#3).__Tag
    //#output(Category getParent(Category, bool)): new Category(getCategory#3).blog
    //#output(Category getParent(Category, bool)): new Category(getCategory#3).blogEntries
    //#output(Category getParent(Category, bool)): new Category(getCategory#3).id
    //#output(Category getParent(Category, bool)): new Category(getCategory#3).name
    //#output(Category getParent(Category, bool)): new Category(getCategory#3).parent
    //#output(Category getParent(Category, bool)): new Category(getCategory#3).subCategories
    //#output(Category getParent(Category, bool)): new Category(getCategory#3).tags
    //#output(Category getParent(Category, bool)): new Category(getCategory#3).tagsAsList
    //#output(Category getParent(Category, bool)): return_value
    //#output(Category getParent(Category, bool)): this.rootCategory
    //#new obj(Category getParent(Category, bool)): new ArrayList(Category#1)
    //#new obj(Category getParent(Category, bool)): new ArrayList(Category#2)
    //#new obj(Category getParent(Category, bool)): new ArrayList(Category#3)
    //#new obj(Category getParent(Category, bool)): new Category(getCategory#2)
    //#new obj(Category getParent(Category, bool)): new Category(getCategory#3)
    //#pre[1] (Category getParent(Category, bool)): category != null
    //#pre[2] (Category getParent(Category, bool)): category.__Tag == net/sourceforge/pebble/domain/Category
    //#pre[3] (Category getParent(Category, bool)): category.id != null
    //#pre[5] (Category getParent(Category, bool)): (soft) init'ed(this.rootCategory)
    //#pre[7] (Category getParent(Category, bool)): (soft) this.__Tag == net/sourceforge/pebble/domain/CategoryBuilder
    //#pre[8] (Category getParent(Category, bool)): (soft) this.blog != null
    //#post(Category getParent(Category, bool)): init'ed(return_value)
    //#post(Category getParent(Category, bool)): init'ed(this.rootCategory)
    //#post(Category getParent(Category, bool)): init'ed(new ArrayList(Category#1) num objects)
    //#post(Category getParent(Category, bool)): init'ed(new ArrayList(Category#2) num objects)
    //#post(Category getParent(Category, bool)): init'ed(new ArrayList(Category#3) num objects)
    //#post(Category getParent(Category, bool)): init'ed(new Category(getCategory#2) num objects)
    //#post(Category getParent(Category, bool)): init'ed(new Category(getCategory#2).__Tag)
    //#post(Category getParent(Category, bool)): possibly_updated(new Category(getCategory#2).blog)
    //#post(Category getParent(Category, bool)): init'ed(new Category(getCategory#2).blogEntries)
    //#post(Category getParent(Category, bool)): possibly_updated(new Category(getCategory#2).id)
    //#post(Category getParent(Category, bool)): init'ed(new Category(getCategory#2).name)
    //#post(Category getParent(Category, bool)): possibly_updated(new Category(getCategory#2).parent)
    //#post(Category getParent(Category, bool)): possibly_updated(new Category(getCategory#2).subCategories)
    //#post(Category getParent(Category, bool)): init'ed(new Category(getCategory#2).tags)
    //#post(Category getParent(Category, bool)): init'ed(new Category(getCategory#2).tagsAsList)
    //#post(Category getParent(Category, bool)): init'ed(new Category(getCategory#3) num objects)
    //#post(Category getParent(Category, bool)): init'ed(new Category(getCategory#3).__Tag)
    //#post(Category getParent(Category, bool)): possibly_updated(new Category(getCategory#3).blog)
    //#post(Category getParent(Category, bool)): init'ed(new Category(getCategory#3).blogEntries)
    //#post(Category getParent(Category, bool)): possibly_updated(new Category(getCategory#3).id)
    //#post(Category getParent(Category, bool)): init'ed(new Category(getCategory#3).name)
    //#post(Category getParent(Category, bool)): possibly_updated(new Category(getCategory#3).parent)
    //#post(Category getParent(Category, bool)): possibly_updated(new Category(getCategory#3).subCategories)
    //#post(Category getParent(Category, bool)): init'ed(new Category(getCategory#3).tags)
    //#post(Category getParent(Category, bool)): init'ed(new Category(getCategory#3).tagsAsList)
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:getSubCategories
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:getCategory
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:net.sourceforge.pebble.domain.Blog:getLocale
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:net.sourceforge.pebble.util.I18n:getMessage
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:net.sourceforge.pebble.domain.Category
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:addCategory
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.lang.String:length
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:getId
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:setBlog
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:isRootCategory
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:addSubCategory
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.util.Collections:unmodifiableList
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.util.List:contains
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(Category getParent(Category, bool)): Effects-of-calling:java.util.List:add
    //#test_vector(Category getParent(Category, bool)): java.lang.String:equals(...)@111: {0}, {1}
    int index = id.lastIndexOf(CATEGORY_SEPARATOR);
    String parentId = id.substring(0, index);
    if (parentId.equals("")) {
      // the parent is the root category
      parentId = "/";
    }

    return getCategory(parentId, create);
    //#categorybuilder.java:116: end of method: Category net.sourceforge.pebble.domain.CategoryBuilder.getParent(Category, bool)
  }

  /**
   * Gets the parent of the specified category.
   *
   * @return  a Category instance
   */
  private Category getParent(Category category) {
    return getParent(category, false);
    //#categorybuilder.java:125: method: Category net.sourceforge.pebble.domain.CategoryBuilder.getParent(Category)
    //#input(Category getParent(Category)): __Descendant_Table[net/sourceforge/pebble/domain/CategoryBuilder]
    //#input(Category getParent(Category)): __Descendant_Table[others]
    //#input(Category getParent(Category)): __Dispatch_Table.addCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getParent(Category)): __Dispatch_Table.getRootCategory()Lnet/sourceforge/pebble/domain/Category;
    //#input(Category getParent(Category)): category
    //#input(Category getParent(Category)): category.__Tag
    //#input(Category getParent(Category)): category.id
    //#input(Category getParent(Category)): net/sourceforge/pebble/domain/Category.__Descendant_Table[net/sourceforge/pebble/domain/Category]
    //#input(Category getParent(Category)): net/sourceforge/pebble/domain/Category.__Descendant_Table[others]
    //#input(Category getParent(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.addSubCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getParent(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getId()Ljava/lang/String;
    //#input(Category getParent(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getSubCategories()Ljava/util/List;
    //#input(Category getParent(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.isRootCategory()Z
    //#input(Category getParent(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setBlog(Lnet/sourceforge/pebble/domain/Blog;)V
    //#input(Category getParent(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setId(Ljava/lang/String;)V
    //#input(Category getParent(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setParent(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getParent(Category)): this
    //#input(Category getParent(Category)): this.__Tag
    //#input(Category getParent(Category)): this.blog
    //#input(Category getParent(Category)): this.rootCategory
    //#input(Category getParent(Category)): this.rootCategory.__Tag
    //#output(Category getParent(Category)): new ArrayList(Category#1) num objects
    //#output(Category getParent(Category)): new ArrayList(Category#2) num objects
    //#output(Category getParent(Category)): new ArrayList(Category#3) num objects
    //#output(Category getParent(Category)): new Category(getCategory#2) num objects
    //#output(Category getParent(Category)): new Category(getCategory#2).__Tag
    //#output(Category getParent(Category)): new Category(getCategory#2).blog
    //#output(Category getParent(Category)): new Category(getCategory#2).blogEntries
    //#output(Category getParent(Category)): new Category(getCategory#2).id
    //#output(Category getParent(Category)): new Category(getCategory#2).name
    //#output(Category getParent(Category)): new Category(getCategory#2).parent
    //#output(Category getParent(Category)): new Category(getCategory#2).subCategories
    //#output(Category getParent(Category)): new Category(getCategory#2).tags
    //#output(Category getParent(Category)): new Category(getCategory#2).tagsAsList
    //#output(Category getParent(Category)): new Category(getCategory#3) num objects
    //#output(Category getParent(Category)): new Category(getCategory#3).__Tag
    //#output(Category getParent(Category)): new Category(getCategory#3).blog
    //#output(Category getParent(Category)): new Category(getCategory#3).blogEntries
    //#output(Category getParent(Category)): new Category(getCategory#3).id
    //#output(Category getParent(Category)): new Category(getCategory#3).name
    //#output(Category getParent(Category)): new Category(getCategory#3).parent
    //#output(Category getParent(Category)): new Category(getCategory#3).subCategories
    //#output(Category getParent(Category)): new Category(getCategory#3).tags
    //#output(Category getParent(Category)): new Category(getCategory#3).tagsAsList
    //#output(Category getParent(Category)): return_value
    //#output(Category getParent(Category)): this.rootCategory
    //#new obj(Category getParent(Category)): new ArrayList(Category#1)
    //#new obj(Category getParent(Category)): new ArrayList(Category#2)
    //#new obj(Category getParent(Category)): new ArrayList(Category#3)
    //#new obj(Category getParent(Category)): new Category(getCategory#2)
    //#new obj(Category getParent(Category)): new Category(getCategory#3)
    //#pre[1] (Category getParent(Category)): category != null
    //#pre[2] (Category getParent(Category)): category.__Tag == net/sourceforge/pebble/domain/Category
    //#pre[3] (Category getParent(Category)): category.id != null
    //#pre[4] (Category getParent(Category)): (soft) init'ed(this.rootCategory)
    //#pre[6] (Category getParent(Category)): (soft) this.__Tag == net/sourceforge/pebble/domain/CategoryBuilder
    //#pre[7] (Category getParent(Category)): (soft) this.blog != null
    //#post(Category getParent(Category)): init'ed(return_value)
    //#post(Category getParent(Category)): init'ed(this.rootCategory)
    //#post(Category getParent(Category)): init'ed(new ArrayList(Category#1) num objects)
    //#post(Category getParent(Category)): init'ed(new ArrayList(Category#2) num objects)
    //#post(Category getParent(Category)): init'ed(new ArrayList(Category#3) num objects)
    //#post(Category getParent(Category)): init'ed(new Category(getCategory#2) num objects)
    //#post(Category getParent(Category)): init'ed(new Category(getCategory#2).__Tag)
    //#post(Category getParent(Category)): possibly_updated(new Category(getCategory#2).blog)
    //#post(Category getParent(Category)): init'ed(new Category(getCategory#2).blogEntries)
    //#post(Category getParent(Category)): possibly_updated(new Category(getCategory#2).id)
    //#post(Category getParent(Category)): init'ed(new Category(getCategory#2).name)
    //#post(Category getParent(Category)): possibly_updated(new Category(getCategory#2).parent)
    //#post(Category getParent(Category)): possibly_updated(new Category(getCategory#2).subCategories)
    //#post(Category getParent(Category)): init'ed(new Category(getCategory#2).tags)
    //#post(Category getParent(Category)): init'ed(new Category(getCategory#2).tagsAsList)
    //#post(Category getParent(Category)): init'ed(new Category(getCategory#3) num objects)
    //#post(Category getParent(Category)): init'ed(new Category(getCategory#3).__Tag)
    //#post(Category getParent(Category)): possibly_updated(new Category(getCategory#3).blog)
    //#post(Category getParent(Category)): init'ed(new Category(getCategory#3).blogEntries)
    //#post(Category getParent(Category)): possibly_updated(new Category(getCategory#3).id)
    //#post(Category getParent(Category)): init'ed(new Category(getCategory#3).name)
    //#post(Category getParent(Category)): possibly_updated(new Category(getCategory#3).parent)
    //#post(Category getParent(Category)): possibly_updated(new Category(getCategory#3).subCategories)
    //#post(Category getParent(Category)): init'ed(new Category(getCategory#3).tags)
    //#post(Category getParent(Category)): init'ed(new Category(getCategory#3).tagsAsList)
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:getSubCategories
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:getCategory
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:net.sourceforge.pebble.domain.Blog:getLocale
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:net.sourceforge.pebble.util.I18n:getMessage
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:net.sourceforge.pebble.domain.Category
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:addCategory
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.lang.String:length
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:getId
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:setBlog
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:isRootCategory
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:addSubCategory
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.util.Collections:unmodifiableList
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.util.List:contains
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(Category getParent(Category)): Effects-of-calling:java.util.List:add
    //#categorybuilder.java:125: end of method: Category net.sourceforge.pebble.domain.CategoryBuilder.getParent(Category)
  }

  /**
   * Gets (and creates if necessary), the specified category.
   *
   * @param id          the id of the category to find
   * @param create      true if the category should be created if it doesn't
   *                    exist, false otherwise
   * @return  a Category instance
   */
  private Category getCategory(String id, boolean create) {
    if (id == null || !id.startsWith("/")) {
    //#categorybuilder.java:137: method: Category net.sourceforge.pebble.domain.CategoryBuilder.getCategory(String, bool)
    //#input(Category getCategory(String, bool)): __Descendant_Table[net/sourceforge/pebble/domain/CategoryBuilder]
    //#input(Category getCategory(String, bool)): __Descendant_Table[others]
    //#input(Category getCategory(String, bool)): __Dispatch_Table.addCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getCategory(String, bool)): __Dispatch_Table.getRootCategory()Lnet/sourceforge/pebble/domain/Category;
    //#input(Category getCategory(String, bool)): create
    //#input(Category getCategory(String, bool)): id
    //#input(Category getCategory(String, bool)): net/sourceforge/pebble/domain/Category.__Descendant_Table[net/sourceforge/pebble/domain/Category]
    //#input(Category getCategory(String, bool)): net/sourceforge/pebble/domain/Category.__Descendant_Table[others]
    //#input(Category getCategory(String, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.addSubCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getCategory(String, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getId()Ljava/lang/String;
    //#input(Category getCategory(String, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getSubCategories()Ljava/util/List;
    //#input(Category getCategory(String, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.isRootCategory()Z
    //#input(Category getCategory(String, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setBlog(Lnet/sourceforge/pebble/domain/Blog;)V
    //#input(Category getCategory(String, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setId(Ljava/lang/String;)V
    //#input(Category getCategory(String, bool)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setParent(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getCategory(String, bool)): this
    //#input(Category getCategory(String, bool)): this.__Tag
    //#input(Category getCategory(String, bool)): this.blog
    //#input(Category getCategory(String, bool)): this.rootCategory
    //#input(Category getCategory(String, bool)): this.rootCategory.__Tag
    //#output(Category getCategory(String, bool)): new ArrayList(Category#1) num objects
    //#output(Category getCategory(String, bool)): new ArrayList(Category#2) num objects
    //#output(Category getCategory(String, bool)): new ArrayList(Category#3) num objects
    //#output(Category getCategory(String, bool)): new Category(getCategory#2) num objects
    //#output(Category getCategory(String, bool)): new Category(getCategory#2).__Tag
    //#output(Category getCategory(String, bool)): new Category(getCategory#2).blog
    //#output(Category getCategory(String, bool)): new Category(getCategory#2).blogEntries
    //#output(Category getCategory(String, bool)): new Category(getCategory#2).id
    //#output(Category getCategory(String, bool)): new Category(getCategory#2).name
    //#output(Category getCategory(String, bool)): new Category(getCategory#2).parent
    //#output(Category getCategory(String, bool)): new Category(getCategory#2).subCategories
    //#output(Category getCategory(String, bool)): new Category(getCategory#2).tags
    //#output(Category getCategory(String, bool)): new Category(getCategory#2).tagsAsList
    //#output(Category getCategory(String, bool)): new Category(getCategory#3) num objects
    //#output(Category getCategory(String, bool)): new Category(getCategory#3).__Tag
    //#output(Category getCategory(String, bool)): new Category(getCategory#3).blog
    //#output(Category getCategory(String, bool)): new Category(getCategory#3).blogEntries
    //#output(Category getCategory(String, bool)): new Category(getCategory#3).id
    //#output(Category getCategory(String, bool)): new Category(getCategory#3).name
    //#output(Category getCategory(String, bool)): new Category(getCategory#3).parent
    //#output(Category getCategory(String, bool)): new Category(getCategory#3).subCategories
    //#output(Category getCategory(String, bool)): new Category(getCategory#3).tags
    //#output(Category getCategory(String, bool)): new Category(getCategory#3).tagsAsList
    //#output(Category getCategory(String, bool)): return_value
    //#output(Category getCategory(String, bool)): this.rootCategory
    //#new obj(Category getCategory(String, bool)): new ArrayList(Category#1)
    //#new obj(Category getCategory(String, bool)): new ArrayList(Category#2)
    //#new obj(Category getCategory(String, bool)): new ArrayList(Category#3)
    //#new obj(Category getCategory(String, bool)): new Category(getCategory#2)
    //#new obj(Category getCategory(String, bool)): new Category(getCategory#3)
    //#pre[3] (Category getCategory(String, bool)): (soft) init'ed(this.rootCategory)
    //#pre[5] (Category getCategory(String, bool)): (soft) this.__Tag == net/sourceforge/pebble/domain/CategoryBuilder
    //#pre[6] (Category getCategory(String, bool)): (soft) this.blog != null
    //#presumption(Category getCategory(String, bool)): category.id@165 != null
    //#presumption(Category getCategory(String, bool)): java.util.Collections:unmodifiableList(...)@230 != null
    //#presumption(Category getCategory(String, bool)): java.util.Iterator:next(...).__Tag@165 == net/sourceforge/pebble/domain/Category
    //#presumption(Category getCategory(String, bool)): java.util.Iterator:next(...)@165 != null
    //#presumption(Category getCategory(String, bool)): parentCategory.__Tag@149 == net/sourceforge/pebble/domain/Category
    //#post(Category getCategory(String, bool)): init'ed(return_value)
    //#post(Category getCategory(String, bool)): (soft) init'ed(this.rootCategory)
    //#post(Category getCategory(String, bool)): init'ed(new ArrayList(Category#1) num objects)
    //#post(Category getCategory(String, bool)): init'ed(new ArrayList(Category#2) num objects)
    //#post(Category getCategory(String, bool)): init'ed(new ArrayList(Category#3) num objects)
    //#post(Category getCategory(String, bool)): new Category(getCategory#2) num objects <= 1
    //#post(Category getCategory(String, bool)): init'ed(new Category(getCategory#2) num objects)
    //#post(Category getCategory(String, bool)): init'ed(new Category(getCategory#2).__Tag)
    //#post(Category getCategory(String, bool)): (soft) init'ed(new Category(getCategory#2).__Tag)
    //#post(Category getCategory(String, bool)): possibly_updated(new Category(getCategory#2).blog)
    //#post(Category getCategory(String, bool)): init'ed(new Category(getCategory#2).blogEntries)
    //#post(Category getCategory(String, bool)): possibly_updated(new Category(getCategory#2).id)
    //#post(Category getCategory(String, bool)): init'ed(new Category(getCategory#2).name)
    //#post(Category getCategory(String, bool)): possibly_updated(new Category(getCategory#2).parent)
    //#post(Category getCategory(String, bool)): possibly_updated(new Category(getCategory#2).subCategories)
    //#post(Category getCategory(String, bool)): init'ed(new Category(getCategory#2).tags)
    //#post(Category getCategory(String, bool)): init'ed(new Category(getCategory#2).tagsAsList)
    //#post(Category getCategory(String, bool)): init'ed(new Category(getCategory#3) num objects)
    //#post(Category getCategory(String, bool)): init'ed(new Category(getCategory#3).__Tag)
    //#post(Category getCategory(String, bool)): possibly_updated(new Category(getCategory#3).blog)
    //#post(Category getCategory(String, bool)): init'ed(new Category(getCategory#3).blogEntries)
    //#post(Category getCategory(String, bool)): possibly_updated(new Category(getCategory#3).id)
    //#post(Category getCategory(String, bool)): init'ed(new Category(getCategory#3).name)
    //#post(Category getCategory(String, bool)): possibly_updated(new Category(getCategory#3).parent)
    //#post(Category getCategory(String, bool)): possibly_updated(new Category(getCategory#3).subCategories)
    //#post(Category getCategory(String, bool)): init'ed(new Category(getCategory#3).tags)
    //#post(Category getCategory(String, bool)): init'ed(new Category(getCategory#3).tagsAsList)
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:getSubCategories
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:getCategory
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:net.sourceforge.pebble.domain.Blog:getLocale
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:net.sourceforge.pebble.util.I18n:getMessage
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:net.sourceforge.pebble.domain.Category
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:addCategory
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.lang.String:length
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:getId
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:setBlog
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:isRootCategory
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:addSubCategory
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.util.Collections:unmodifiableList
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.util.List:contains
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(Category getCategory(String, bool)): Effects-of-calling:java.util.List:add
    //#test_vector(Category getCategory(String, bool)): create: {0}, {1}
    //#test_vector(Category getCategory(String, bool)): id: Addr_Set{null}, Inverse{null}
    //#test_vector(Category getCategory(String, bool)): this.rootCategory: Inverse{null}, Addr_Set{null}
    //#test_vector(Category getCategory(String, bool)): java.lang.String:equals(...)@141: {0}, {1}
    //#test_vector(Category getCategory(String, bool)): java.lang.String:equals(...)@166: {0}, {1}
    //#test_vector(Category getCategory(String, bool)): java.lang.String:indexOf(...)@154: {-2_147_483_648..-2, 0..4_294_967_294}, {-1}
    //#test_vector(Category getCategory(String, bool)): java.lang.String:startsWith(...)@137: {1}, {0}
    //#test_vector(Category getCategory(String, bool)): java.util.Iterator:hasNext(...)@164: {1}, {0}
      id = "/" + id;
    }

    if (id.equals("/")) {
      if (rootCategory == null) {
        Category category = new Category("/", I18n.getMessage(blog.getLocale(), "category.all"));
    //#categorybuilder.java:143: Warning: method not available
    //#    -- call on Locale net.sourceforge.pebble.domain.Blog:getLocale()
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: Category getCategory(String, bool)
    //#    unanalyzed callee: Locale net.sourceforge.pebble.domain.Blog:getLocale()
    //#categorybuilder.java:143: Warning: method not available
    //#    -- call on String net.sourceforge.pebble.util.I18n:getMessage(Locale, String)
    //#    severity: INFORMATIONAL
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: Category getCategory(String, bool)
    //#    unanalyzed callee: String net.sourceforge.pebble.util.I18n:getMessage(Locale, String)
        addCategory(category);
      }

      return rootCategory;
    } else {
      Category parentCategory = getRootCategory();
      Category category = null;
      boolean found = false;
    //#categorybuilder.java:151: Warning: unused assignment
    //#    unused assignment into found
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: Category getCategory(String, bool)
    //#    Attribs:  Uncertain
      int index = 0;
      do {
        index = id.indexOf("/", index+1);
        String categoryId;
        if (index == -1) {
          categoryId = id.substring(0, id.length());
        } else {
          categoryId = id.substring(0, index);
        }

        found = false;
        Iterator it = parentCategory.getSubCategories().iterator();
    //#categorybuilder.java:163: ?null dereference
    //#    parentCategory != null
    //#    severity: MEDIUM
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: Category getCategory(String, bool)
    //#    basic block: bb_12
    //#    assertion: parentCategory != null
    //#    VN: parentCategory
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#categorybuilder.java:163: ?use of default init
    //#    init'ed(parentCategory.__Tag)
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: Category getCategory(String, bool)
    //#    basic block: bb_12
    //#    assertion: init'ed(parentCategory.__Tag)
    //#    VN: parentCategory.__Tag
    //#    Expected: {-Inf..+Inf}
    //#    Bad: {Invalid}
    //#    Attribs:  Int  Bad only invalid
    //#categorybuilder.java:163: ?null dereference
    //#    net/sourceforge/pebble/domain/Category.__Descendant_Table[parentCategory.__Tag] != null
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: Category getCategory(String, bool)
    //#    basic block: bb_12
    //#    assertion: net/sourceforge/pebble/domain/Category.__Descendant_Table[parentCategory.__Tag] != null
    //#    VN: net/sourceforge/pebble/domain/Category.__Descendant_Table[parentCategory.__Tag]
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#categorybuilder.java:163: ?precondition failure
    //#    net/sourceforge/pebble/domain/Category.getSubCategories: init'ed(this.subCategories)
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: Category getCategory(String, bool)
    //#    basic block: bb_12
    //#    assertion: init'ed(parentCategory.subCategories)
    //#    callee: List net/sourceforge/pebble/domain/Category.getSubCategories()
    //#    callee assertion: init'ed(this.subCategories)
    //#    callee file: category.java
    //#    callee precondition index: [2]
    //#    callee srcpos: 230
    //#    VN: parentCategory.subCategories
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
        while (it.hasNext()) {
          category = (Category)it.next();
          if (category.getId().equals(categoryId)) {
            found = true;
            break;
          }
        }

        if (!found) {
          if (create) {
            category = new Category(categoryId, categoryId);
            addCategory(category);
          } else {
            return null;
          }
        }

        parentCategory = category;
      } while (index != -1);

      return category;
    //#categorybuilder.java:184: end of method: Category net.sourceforge.pebble.domain.CategoryBuilder.getCategory(String, bool)
    }
  }

  /**
   * Gets (and creates if necessary), the specified category.
   *
   * @param id          the id of the category to find
   * @return  a Category instance
   */
  public Category getCategory(String id) {
    return getCategory(id, false);
    //#categorybuilder.java:195: method: Category net.sourceforge.pebble.domain.CategoryBuilder.getCategory(String)
    //#input(Category getCategory(String)): __Descendant_Table[net/sourceforge/pebble/domain/CategoryBuilder]
    //#input(Category getCategory(String)): __Descendant_Table[others]
    //#input(Category getCategory(String)): __Dispatch_Table.addCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getCategory(String)): __Dispatch_Table.getRootCategory()Lnet/sourceforge/pebble/domain/Category;
    //#input(Category getCategory(String)): id
    //#input(Category getCategory(String)): net/sourceforge/pebble/domain/Category.__Descendant_Table[net/sourceforge/pebble/domain/Category]
    //#input(Category getCategory(String)): net/sourceforge/pebble/domain/Category.__Descendant_Table[others]
    //#input(Category getCategory(String)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.addSubCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getCategory(String)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getId()Ljava/lang/String;
    //#input(Category getCategory(String)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getSubCategories()Ljava/util/List;
    //#input(Category getCategory(String)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.isRootCategory()Z
    //#input(Category getCategory(String)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setBlog(Lnet/sourceforge/pebble/domain/Blog;)V
    //#input(Category getCategory(String)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setId(Ljava/lang/String;)V
    //#input(Category getCategory(String)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setParent(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getCategory(String)): this
    //#input(Category getCategory(String)): this.__Tag
    //#input(Category getCategory(String)): this.blog
    //#input(Category getCategory(String)): this.rootCategory
    //#input(Category getCategory(String)): this.rootCategory.__Tag
    //#output(Category getCategory(String)): new ArrayList(Category#1) num objects
    //#output(Category getCategory(String)): new ArrayList(Category#2) num objects
    //#output(Category getCategory(String)): new ArrayList(Category#3) num objects
    //#output(Category getCategory(String)): new Category(getCategory#2*) num objects
    //#output(Category getCategory(String)): new Category(getCategory#2*).__Tag
    //#output(Category getCategory(String)): new Category(getCategory#2*).blog
    //#output(Category getCategory(String)): new Category(getCategory#2*).blogEntries
    //#output(Category getCategory(String)): new Category(getCategory#2*).id
    //#output(Category getCategory(String)): new Category(getCategory#2*).name
    //#output(Category getCategory(String)): new Category(getCategory#2*).parent
    //#output(Category getCategory(String)): new Category(getCategory#2*).subCategories
    //#output(Category getCategory(String)): new Category(getCategory#2*).tags
    //#output(Category getCategory(String)): new Category(getCategory#2*).tagsAsList
    //#output(Category getCategory(String)): new Category(getCategory#3*) num objects
    //#output(Category getCategory(String)): new Category(getCategory#3*).__Tag
    //#output(Category getCategory(String)): new Category(getCategory#3*).blog
    //#output(Category getCategory(String)): new Category(getCategory#3*).blogEntries
    //#output(Category getCategory(String)): new Category(getCategory#3*).id
    //#output(Category getCategory(String)): new Category(getCategory#3*).name
    //#output(Category getCategory(String)): new Category(getCategory#3*).parent
    //#output(Category getCategory(String)): new Category(getCategory#3*).subCategories
    //#output(Category getCategory(String)): new Category(getCategory#3*).tags
    //#output(Category getCategory(String)): new Category(getCategory#3*).tagsAsList
    //#output(Category getCategory(String)): return_value
    //#output(Category getCategory(String)): this.rootCategory
    //#new obj(Category getCategory(String)): new ArrayList(Category#1)
    //#new obj(Category getCategory(String)): new ArrayList(Category#2)
    //#new obj(Category getCategory(String)): new ArrayList(Category#3)
    //#new obj(Category getCategory(String)): new Category(getCategory#2*)
    //#new obj(Category getCategory(String)): new Category(getCategory#3*)
    //#pre[2] (Category getCategory(String)): (soft) init'ed(this.rootCategory)
    //#pre[4] (Category getCategory(String)): (soft) this.__Tag == net/sourceforge/pebble/domain/CategoryBuilder
    //#pre[5] (Category getCategory(String)): (soft) this.blog != null
    //#post(Category getCategory(String)): init'ed(return_value)
    //#post(Category getCategory(String)): init'ed(this.rootCategory)
    //#post(Category getCategory(String)): init'ed(new ArrayList(Category#1) num objects)
    //#post(Category getCategory(String)): init'ed(new ArrayList(Category#2) num objects)
    //#post(Category getCategory(String)): init'ed(new ArrayList(Category#3) num objects)
    //#post(Category getCategory(String)): init'ed(new Category(getCategory#2*) num objects)
    //#post(Category getCategory(String)): init'ed(new Category(getCategory#2*).__Tag)
    //#post(Category getCategory(String)): possibly_updated(new Category(getCategory#2*).blog)
    //#post(Category getCategory(String)): init'ed(new Category(getCategory#2*).blogEntries)
    //#post(Category getCategory(String)): possibly_updated(new Category(getCategory#2*).id)
    //#post(Category getCategory(String)): init'ed(new Category(getCategory#2*).name)
    //#post(Category getCategory(String)): possibly_updated(new Category(getCategory#2*).parent)
    //#post(Category getCategory(String)): possibly_updated(new Category(getCategory#2*).subCategories)
    //#post(Category getCategory(String)): init'ed(new Category(getCategory#2*).tags)
    //#post(Category getCategory(String)): init'ed(new Category(getCategory#2*).tagsAsList)
    //#post(Category getCategory(String)): init'ed(new Category(getCategory#3*) num objects)
    //#post(Category getCategory(String)): init'ed(new Category(getCategory#3*).__Tag)
    //#post(Category getCategory(String)): possibly_updated(new Category(getCategory#3*).blog)
    //#post(Category getCategory(String)): init'ed(new Category(getCategory#3*).blogEntries)
    //#post(Category getCategory(String)): possibly_updated(new Category(getCategory#3*).id)
    //#post(Category getCategory(String)): init'ed(new Category(getCategory#3*).name)
    //#post(Category getCategory(String)): possibly_updated(new Category(getCategory#3*).parent)
    //#post(Category getCategory(String)): possibly_updated(new Category(getCategory#3*).subCategories)
    //#post(Category getCategory(String)): init'ed(new Category(getCategory#3*).tags)
    //#post(Category getCategory(String)): init'ed(new Category(getCategory#3*).tagsAsList)
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:getSubCategories
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:getCategory
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:net.sourceforge.pebble.domain.Blog:getLocale
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:net.sourceforge.pebble.util.I18n:getMessage
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:net.sourceforge.pebble.domain.Category
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:addCategory
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.lang.String:length
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:getId
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:setBlog
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:isRootCategory
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:addSubCategory
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.util.Collections:unmodifiableList
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.util.List:contains
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(Category getCategory(String)): Effects-of-calling:java.util.List:add
    //#categorybuilder.java:195: end of method: Category net.sourceforge.pebble.domain.CategoryBuilder.getCategory(String)
  }

  /**
   * Gets the root category.
   *
   * @return  a Category instance
   */
  public Category getRootCategory() {
    return getCategory("/", true);
    //#categorybuilder.java:204: method: Category net.sourceforge.pebble.domain.CategoryBuilder.getRootCategory()
    //#input(Category getRootCategory()): __Descendant_Table[net/sourceforge/pebble/domain/CategoryBuilder]
    //#input(Category getRootCategory()): __Descendant_Table[others]
    //#input(Category getRootCategory()): __Dispatch_Table.addCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getRootCategory()): __Dispatch_Table.getRootCategory()Lnet/sourceforge/pebble/domain/Category;
    //#input(Category getRootCategory()): net/sourceforge/pebble/domain/Category.__Descendant_Table[net/sourceforge/pebble/domain/Category]
    //#input(Category getRootCategory()): net/sourceforge/pebble/domain/Category.__Descendant_Table[others]
    //#input(Category getRootCategory()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.addSubCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getRootCategory()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getId()Ljava/lang/String;
    //#input(Category getRootCategory()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getSubCategories()Ljava/util/List;
    //#input(Category getRootCategory()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.isRootCategory()Z
    //#input(Category getRootCategory()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setBlog(Lnet/sourceforge/pebble/domain/Blog;)V
    //#input(Category getRootCategory()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setId(Ljava/lang/String;)V
    //#input(Category getRootCategory()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setParent(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(Category getRootCategory()): this
    //#input(Category getRootCategory()): this.__Tag
    //#input(Category getRootCategory()): this.blog
    //#input(Category getRootCategory()): this.rootCategory
    //#input(Category getRootCategory()): this.rootCategory.__Tag
    //#output(Category getRootCategory()): new ArrayList(Category#1) num objects
    //#output(Category getRootCategory()): new ArrayList(Category#2) num objects
    //#output(Category getRootCategory()): new ArrayList(Category#3) num objects
    //#output(Category getRootCategory()): new Category(getCategory#2) num objects
    //#output(Category getRootCategory()): new Category(getCategory#2).__Tag
    //#output(Category getRootCategory()): new Category(getCategory#2).blog
    //#output(Category getRootCategory()): new Category(getCategory#2).blogEntries
    //#output(Category getRootCategory()): new Category(getCategory#2).id
    //#output(Category getRootCategory()): new Category(getCategory#2).name
    //#output(Category getRootCategory()): new Category(getCategory#2).parent
    //#output(Category getRootCategory()): new Category(getCategory#2).subCategories
    //#output(Category getRootCategory()): new Category(getCategory#2).tags
    //#output(Category getRootCategory()): new Category(getCategory#2).tagsAsList
    //#output(Category getRootCategory()): new Category(getCategory#3) num objects
    //#output(Category getRootCategory()): new Category(getCategory#3).__Tag
    //#output(Category getRootCategory()): new Category(getCategory#3).blog
    //#output(Category getRootCategory()): new Category(getCategory#3).blogEntries
    //#output(Category getRootCategory()): new Category(getCategory#3).id
    //#output(Category getRootCategory()): new Category(getCategory#3).name
    //#output(Category getRootCategory()): new Category(getCategory#3).parent
    //#output(Category getRootCategory()): new Category(getCategory#3).subCategories
    //#output(Category getRootCategory()): new Category(getCategory#3).tags
    //#output(Category getRootCategory()): new Category(getCategory#3).tagsAsList
    //#output(Category getRootCategory()): return_value
    //#output(Category getRootCategory()): this.rootCategory
    //#new obj(Category getRootCategory()): new ArrayList(Category#1)
    //#new obj(Category getRootCategory()): new ArrayList(Category#2)
    //#new obj(Category getRootCategory()): new ArrayList(Category#3)
    //#new obj(Category getRootCategory()): new Category(getCategory#2)
    //#new obj(Category getRootCategory()): new Category(getCategory#3)
    //#pre[1] (Category getRootCategory()): (soft) init'ed(this.rootCategory)
    //#pre[3] (Category getRootCategory()): (soft) this.__Tag == net/sourceforge/pebble/domain/CategoryBuilder
    //#pre[4] (Category getRootCategory()): (soft) this.blog != null
    //#post(Category getRootCategory()): init'ed(return_value)
    //#post(Category getRootCategory()): init'ed(this.rootCategory)
    //#post(Category getRootCategory()): init'ed(new ArrayList(Category#1) num objects)
    //#post(Category getRootCategory()): init'ed(new ArrayList(Category#2) num objects)
    //#post(Category getRootCategory()): init'ed(new ArrayList(Category#3) num objects)
    //#post(Category getRootCategory()): init'ed(new Category(getCategory#2) num objects)
    //#post(Category getRootCategory()): init'ed(new Category(getCategory#2).__Tag)
    //#post(Category getRootCategory()): possibly_updated(new Category(getCategory#2).blog)
    //#post(Category getRootCategory()): init'ed(new Category(getCategory#2).blogEntries)
    //#post(Category getRootCategory()): possibly_updated(new Category(getCategory#2).id)
    //#post(Category getRootCategory()): init'ed(new Category(getCategory#2).name)
    //#post(Category getRootCategory()): possibly_updated(new Category(getCategory#2).parent)
    //#post(Category getRootCategory()): possibly_updated(new Category(getCategory#2).subCategories)
    //#post(Category getRootCategory()): init'ed(new Category(getCategory#2).tags)
    //#post(Category getRootCategory()): init'ed(new Category(getCategory#2).tagsAsList)
    //#post(Category getRootCategory()): init'ed(new Category(getCategory#3) num objects)
    //#post(Category getRootCategory()): init'ed(new Category(getCategory#3).__Tag)
    //#post(Category getRootCategory()): possibly_updated(new Category(getCategory#3).blog)
    //#post(Category getRootCategory()): init'ed(new Category(getCategory#3).blogEntries)
    //#post(Category getRootCategory()): possibly_updated(new Category(getCategory#3).id)
    //#post(Category getRootCategory()): init'ed(new Category(getCategory#3).name)
    //#post(Category getRootCategory()): possibly_updated(new Category(getCategory#3).parent)
    //#post(Category getRootCategory()): possibly_updated(new Category(getCategory#3).subCategories)
    //#post(Category getRootCategory()): init'ed(new Category(getCategory#3).tags)
    //#post(Category getRootCategory()): init'ed(new Category(getCategory#3).tagsAsList)
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:getSubCategories
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:getCategory
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:net.sourceforge.pebble.domain.Blog:getLocale
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:net.sourceforge.pebble.util.I18n:getMessage
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:net.sourceforge.pebble.domain.Category
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:addCategory
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.lang.String:length
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:getId
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:setBlog
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:isRootCategory
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:addSubCategory
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.util.Collections:unmodifiableList
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.util.List:contains
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(Category getRootCategory()): Effects-of-calling:java.util.List:add
    //#categorybuilder.java:204: end of method: Category net.sourceforge.pebble.domain.CategoryBuilder.getRootCategory()
  }

  /**
   * Gets a collection containing all blog categories,
   * ordered by category name.
   *
   * @return  a sorted List of Category instances
   */
  public List<Category> getCategories() {
    List<Category> allCategories = new ArrayList<Category>();
    //#categorybuilder.java:214: method: List net.sourceforge.pebble.domain.CategoryBuilder.getCategories()
    //#input(List getCategories()): __Descendant_Table[net/sourceforge/pebble/domain/CategoryBuilder]
    //#input(List getCategories()): __Descendant_Table[others]
    //#input(List getCategories()): __Dispatch_Table.addCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(List getCategories()): __Dispatch_Table.getCategories(Lnet/sourceforge/pebble/domain/Category;)Ljava/util/List;
    //#input(List getCategories()): __Dispatch_Table.getRootCategory()Lnet/sourceforge/pebble/domain/Category;
    //#input(List getCategories()): net/sourceforge/pebble/domain/Category.__Descendant_Table[net/sourceforge/pebble/domain/Category]
    //#input(List getCategories()): net/sourceforge/pebble/domain/Category.__Descendant_Table[others]
    //#input(List getCategories()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.addSubCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(List getCategories()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getId()Ljava/lang/String;
    //#input(List getCategories()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getSubCategories()Ljava/util/List;
    //#input(List getCategories()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.isRootCategory()Z
    //#input(List getCategories()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setBlog(Lnet/sourceforge/pebble/domain/Blog;)V
    //#input(List getCategories()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setId(Ljava/lang/String;)V
    //#input(List getCategories()): net/sourceforge/pebble/domain/Category.__Dispatch_Table.setParent(Lnet/sourceforge/pebble/domain/Category;)V
    //#input(List getCategories()): this
    //#input(List getCategories()): this.__Tag
    //#input(List getCategories()): this.blog
    //#input(List getCategories()): this.rootCategory
    //#input(List getCategories()): this.rootCategory.__Tag
    //#output(List getCategories()): new ArrayList(Category#1) num objects
    //#output(List getCategories()): new ArrayList(Category#2) num objects
    //#output(List getCategories()): new ArrayList(Category#3) num objects
    //#output(List getCategories()): new ArrayList(getCategories#1) num objects
    //#output(List getCategories()): new Category(getCategory#2) num objects
    //#output(List getCategories()): new Category(getCategory#2).__Tag
    //#output(List getCategories()): new Category(getCategory#2).blog
    //#output(List getCategories()): new Category(getCategory#2).blogEntries
    //#output(List getCategories()): new Category(getCategory#2).id
    //#output(List getCategories()): new Category(getCategory#2).name
    //#output(List getCategories()): new Category(getCategory#2).parent
    //#output(List getCategories()): new Category(getCategory#2).subCategories
    //#output(List getCategories()): new Category(getCategory#2).tags
    //#output(List getCategories()): new Category(getCategory#2).tagsAsList
    //#output(List getCategories()): new Category(getCategory#3) num objects
    //#output(List getCategories()): new Category(getCategory#3).__Tag
    //#output(List getCategories()): new Category(getCategory#3).blog
    //#output(List getCategories()): new Category(getCategory#3).blogEntries
    //#output(List getCategories()): new Category(getCategory#3).id
    //#output(List getCategories()): new Category(getCategory#3).name
    //#output(List getCategories()): new Category(getCategory#3).parent
    //#output(List getCategories()): new Category(getCategory#3).subCategories
    //#output(List getCategories()): new Category(getCategory#3).tags
    //#output(List getCategories()): new Category(getCategory#3).tagsAsList
    //#output(List getCategories()): return_value
    //#output(List getCategories()): this.rootCategory
    //#new obj(List getCategories()): new ArrayList(Category#1)
    //#new obj(List getCategories()): new ArrayList(Category#2)
    //#new obj(List getCategories()): new ArrayList(Category#3)
    //#new obj(List getCategories()): new ArrayList(getCategories#1)
    //#new obj(List getCategories()): new Category(getCategory#2)
    //#new obj(List getCategories()): new Category(getCategory#3)
    //#pre[1] (List getCategories()): (soft) init'ed(this.rootCategory)
    //#pre[3] (List getCategories()): (soft) this.__Tag == net/sourceforge/pebble/domain/CategoryBuilder
    //#pre[4] (List getCategories()): (soft) this.blog != null
    //#presumption(List getCategories()): getRootCategory(...).__Tag@215 == net/sourceforge/pebble/domain/Category
    //#post(List getCategories()): return_value == &new ArrayList(getCategories#1)
    //#post(List getCategories()): init'ed(this.rootCategory)
    //#post(List getCategories()): init'ed(new ArrayList(Category#1) num objects)
    //#post(List getCategories()): init'ed(new ArrayList(Category#2) num objects)
    //#post(List getCategories()): init'ed(new ArrayList(Category#3) num objects)
    //#post(List getCategories()): new ArrayList(getCategories#1) num objects == 1
    //#post(List getCategories()): init'ed(new Category(getCategory#2) num objects)
    //#post(List getCategories()): init'ed(new Category(getCategory#2).__Tag)
    //#post(List getCategories()): possibly_updated(new Category(getCategory#2).blog)
    //#post(List getCategories()): init'ed(new Category(getCategory#2).blogEntries)
    //#post(List getCategories()): possibly_updated(new Category(getCategory#2).id)
    //#post(List getCategories()): init'ed(new Category(getCategory#2).name)
    //#post(List getCategories()): possibly_updated(new Category(getCategory#2).parent)
    //#post(List getCategories()): (soft) init'ed(new Category(getCategory#2).subCategories)
    //#post(List getCategories()): init'ed(new Category(getCategory#2).tags)
    //#post(List getCategories()): init'ed(new Category(getCategory#2).tagsAsList)
    //#post(List getCategories()): init'ed(new Category(getCategory#3) num objects)
    //#post(List getCategories()): init'ed(new Category(getCategory#3).__Tag)
    //#post(List getCategories()): possibly_updated(new Category(getCategory#3).blog)
    //#post(List getCategories()): init'ed(new Category(getCategory#3).blogEntries)
    //#post(List getCategories()): possibly_updated(new Category(getCategory#3).id)
    //#post(List getCategories()): init'ed(new Category(getCategory#3).name)
    //#post(List getCategories()): possibly_updated(new Category(getCategory#3).parent)
    //#post(List getCategories()): (soft) init'ed(new Category(getCategory#3).subCategories)
    //#post(List getCategories()): init'ed(new Category(getCategory#3).tags)
    //#post(List getCategories()): init'ed(new Category(getCategory#3).tagsAsList)
    //#unanalyzed(List getCategories()): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(List getCategories()): Effects-of-calling:java.util.List:add
    //#unanalyzed(List getCategories()): Effects-of-calling:getSubCategories
    //#unanalyzed(List getCategories()): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(List getCategories()): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(List getCategories()): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(List getCategories()): Effects-of-calling:getCategories
    //#unanalyzed(List getCategories()): Effects-of-calling:java.util.List:addAll
    //#unanalyzed(List getCategories()): Effects-of-calling:getCategory
    //#unanalyzed(List getCategories()): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(List getCategories()): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(List getCategories()): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(List getCategories()): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(List getCategories()): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(List getCategories()): Effects-of-calling:net.sourceforge.pebble.domain.Blog:getLocale
    //#unanalyzed(List getCategories()): Effects-of-calling:net.sourceforge.pebble.util.I18n:getMessage
    //#unanalyzed(List getCategories()): Effects-of-calling:net.sourceforge.pebble.domain.Category
    //#unanalyzed(List getCategories()): Effects-of-calling:addCategory
    //#unanalyzed(List getCategories()): Effects-of-calling:java.lang.String:indexOf
    //#unanalyzed(List getCategories()): Effects-of-calling:java.lang.String:length
    //#unanalyzed(List getCategories()): Effects-of-calling:java.lang.String:substring
    //#unanalyzed(List getCategories()): Effects-of-calling:getId
    //#unanalyzed(List getCategories()): Effects-of-calling:java.lang.String:lastIndexOf
    //#unanalyzed(List getCategories()): Effects-of-calling:setBlog
    //#unanalyzed(List getCategories()): Effects-of-calling:isRootCategory
    //#unanalyzed(List getCategories()): Effects-of-calling:addSubCategory
    //#unanalyzed(List getCategories()): Effects-of-calling:java.util.Collections:unmodifiableList
    //#unanalyzed(List getCategories()): Effects-of-calling:java.util.List:contains
    allCategories.addAll(getCategories(getRootCategory()));
    //#categorybuilder.java:215: ?precondition failure
    //#    net/sourceforge/pebble/domain/CategoryBuilder.getCategories: category != null
    //#    severity: MEDIUM
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: List getCategories()
    //#    basic block: Entry_BB_1
    //#    assertion: getRootCategory(...) != null
    //#    callee: List net/sourceforge/pebble/domain/CategoryBuilder.getCategories(Category)
    //#    callee assertion: category != null
    //#    callee file: categorybuilder.java
    //#    callee precondition index: [1]
    //#    callee srcpos: 222
    //#    VN: getRootCategory(...)
    //#    Expected: Inverse{null}
    //#    Bad: Addr_Set{null}
    //#    Attribs:  Ptr  null in Bad
    //#categorybuilder.java:215: ?precondition failure
    //#    net/sourceforge/pebble/domain/CategoryBuilder.getCategories: category.__Tag == net/sourceforge/pebble/domain/Category
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: List getCategories()
    //#    basic block: Entry_BB_1
    //#    assertion: getRootCategory(...).__Tag == net/sourceforge/pebble/domain/Category
    //#    callee: List net/sourceforge/pebble/domain/CategoryBuilder.getCategories(Category)
    //#    callee assertion: category.__Tag == net/sourceforge/pebble/domain/Category
    //#    callee file: categorybuilder.java
    //#    callee precondition index: [2]
    //#    callee srcpos: 222
    //#    VN: getRootCategory(...).__Tag
    //#    Expected: {792_320}
    //#    Bad: {0..792_319, 792_321..+Inf, Invalid}
    //#    Attribs:  Int  Exp singleton  Bad overlaps +/-1000  Bad < Exp  Bad > Exp
    //#categorybuilder.java:215: ?precondition failure
    //#    net/sourceforge/pebble/domain/CategoryBuilder.getCategories: init'ed(category.subCategories)
    //#    severity: SUPPRESSED
    //#    class: net.sourceforge.pebble.domain.CategoryBuilder
    //#    method: List getCategories()
    //#    basic block: Entry_BB_1
    //#    assertion: init'ed(getRootCategory(...).subCategories)
    //#    callee: List net/sourceforge/pebble/domain/CategoryBuilder.getCategories(Category)
    //#    callee assertion: init'ed(category.subCategories)
    //#    callee file: categorybuilder.java
    //#    callee precondition index: [3]
    //#    callee srcpos: 222
    //#    VN: getRootCategory(...).subCategories
    //#    Expected: Univ-VN-Set
    //#    Bad: {Invalid}
    //#    Attribs:  Ptr  Bad only invalid
    Collections.sort(allCategories);

    return allCategories;
    //#categorybuilder.java:218: end of method: List net.sourceforge.pebble.domain.CategoryBuilder.getCategories()
  }

  public List<Category> getCategories(Category category) {
    List<Category> allCategories = new ArrayList<Category>();
    //#categorybuilder.java:222: method: List net.sourceforge.pebble.domain.CategoryBuilder.getCategories(Category)
    //#input(List getCategories(Category)): __Descendant_Table[net/sourceforge/pebble/domain/CategoryBuilder]
    //#input(List getCategories(Category)): __Descendant_Table[others]
    //#input(List getCategories(Category)): __Dispatch_Table.getCategories(Lnet/sourceforge/pebble/domain/Category;)Ljava/util/List;
    //#input(List getCategories(Category)): category
    //#input(List getCategories(Category)): category.__Tag
    //#input(List getCategories(Category)): category.subCategories
    //#input(List getCategories(Category)): net/sourceforge/pebble/domain/Category.__Descendant_Table[net/sourceforge/pebble/domain/Category]
    //#input(List getCategories(Category)): net/sourceforge/pebble/domain/Category.__Descendant_Table[others]
    //#input(List getCategories(Category)): net/sourceforge/pebble/domain/Category.__Dispatch_Table.getSubCategories()Ljava/util/List;
    //#input(List getCategories(Category)): this
    //#input(List getCategories(Category)): this.__Tag
    //#output(List getCategories(Category)): new ArrayList(getCategories#1) num objects
    //#output(List getCategories(Category)): return_value
    //#new obj(List getCategories(Category)): new ArrayList(getCategories#1)
    //#pre[1] (List getCategories(Category)): category != null
    //#pre[2] (List getCategories(Category)): category.__Tag == net/sourceforge/pebble/domain/Category
    //#pre[3] (List getCategories(Category)): init'ed(category.subCategories)
    //#pre[5] (List getCategories(Category)): (soft) this.__Tag == net/sourceforge/pebble/domain/CategoryBuilder
    //#presumption(List getCategories(Category)): java.util.Collections:unmodifiableList(...)@230 != null
    //#presumption(List getCategories(Category)): java.util.Iterator:next(...).__Tag@226 == net/sourceforge/pebble/domain/Category
    //#presumption(List getCategories(Category)): java.util.Iterator:next(...)@226 != null
    //#post(List getCategories(Category)): return_value == &new ArrayList(getCategories#1)
    //#post(List getCategories(Category)): new ArrayList(getCategories#1) num objects == 1
    //#unanalyzed(List getCategories(Category)): Effects-of-calling:java.util.ArrayList
    //#unanalyzed(List getCategories(Category)): Effects-of-calling:java.util.List:add
    //#unanalyzed(List getCategories(Category)): Effects-of-calling:getSubCategories
    //#unanalyzed(List getCategories(Category)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(List getCategories(Category)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(List getCategories(Category)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(List getCategories(Category)): Effects-of-calling:getCategories
    //#unanalyzed(List getCategories(Category)): Effects-of-calling:java.util.List:addAll
    //#unanalyzed(List getCategories(Category)): Effects-of-calling:java.util.Collections:unmodifiableList
    //#test_vector(List getCategories(Category)): java.util.Iterator:hasNext(...)@225: {1}, {0}
    allCategories.add(category);
    Iterator it = category.getSubCategories().iterator();
    while (it.hasNext()) {
      allCategories.addAll(getCategories((Category)it.next()));
    }

    return allCategories;
    //#categorybuilder.java:229: end of method: List net.sourceforge.pebble.domain.CategoryBuilder.getCategories(Category)
  }

}    //#output(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Descendant_Table[net/sourceforge/pebble/domain/CategoryBuilder]
    //#output(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.addCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#output(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getCategories()Ljava/util/List;
    //#output(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getCategories(Lnet/sourceforge/pebble/domain/Category;)Ljava/util/List;
    //#output(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getCategory(Ljava/lang/String;)Lnet/sourceforge/pebble/domain/Category;
    //#output(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getCategory(Ljava/lang/String;Z)Lnet/sourceforge/pebble/domain/Category;
    //#output(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getParent(Lnet/sourceforge/pebble/domain/Category;)Lnet/sourceforge/pebble/domain/Category;
    //#output(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getParent(Lnet/sourceforge/pebble/domain/Category;Z)Lnet/sourceforge/pebble/domain/Category;
    //#output(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getRootCategory()Lnet/sourceforge/pebble/domain/Category;
    //#output(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.removeCategory(Lnet/sourceforge/pebble/domain/Category;)V
    //#post(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Descendant_Table[net/sourceforge/pebble/domain/CategoryBuilder] == &__Dispatch_Table
    //#post(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.addCategory(Lnet/sourceforge/pebble/domain/Category;)V == &addCategory
    //#post(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getCategories()Ljava/util/List; == &getCategories
    //#post(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getCategories(Lnet/sourceforge/pebble/domain/Category;)Ljava/util/List; == &getCategories
    //#post(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getCategory(Ljava/lang/String;)Lnet/sourceforge/pebble/domain/Category; == &getCategory
    //#post(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getCategory(Ljava/lang/String;Z)Lnet/sourceforge/pebble/domain/Category; == &getCategory
    //#post(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getParent(Lnet/sourceforge/pebble/domain/Category;)Lnet/sourceforge/pebble/domain/Category; == &getParent
    //#post(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getParent(Lnet/sourceforge/pebble/domain/Category;Z)Lnet/sourceforge/pebble/domain/Category; == &getParent
    //#post(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.getRootCategory()Lnet/sourceforge/pebble/domain/Category; == &getRootCategory
    //#post(net.sourceforge.pebble.domain.CategoryBuilder__static_init): __Dispatch_Table.removeCategory(Lnet/sourceforge/pebble/domain/Category;)V == &removeCategory
    //#categorybuilder.java:: end of method: net.sourceforge.pebble.domain.CategoryBuilder.net.sourceforge.pebble.domain.CategoryBuilder__static_init
    //#categorybuilder.java:: end of class: net.sourceforge.pebble.domain.CategoryBuilder
