| method | Collection findCollection(String, String) |
| pre | this.collections != null |
| pre | (soft) contentType != null |
| presumption | col.accepts@84 != null |
| presumption | java.util.Iterator:next(...)@84 != null |
| post | (soft) init'ed(return_value) |
| unanalyzed | call on java.lang.String:trim |
| unanalyzed | call on java.lang.String:equals |
| unanalyzed | call on java.util.List:size |
| unanalyzed | call on java.util.List:toArray |
| unanalyzed | call on java.lang.String:indexOf |
| unanalyzed | call on java.lang.String:substring |
| unanalyzed | call on java.lang.String:startsWith |
| test_vector | title: Addr_Set{null}, Inverse{null} |
| test_vector | java.util.Iterator:hasNext(...)@83: {0}, {1} |
| method | Workspace elementToWorkspace(Element) |
| pre | element != null |
| pre | init'ed(org/apache/roller/weblogger/webservices/ato mprotocol/AtomService.ATOM_FORMAT) |
| pre | init'ed(org/apache/roller/weblogger/webservices/ato mprotocol/AtomService.ATOM_PROTOCOL) |
| presumption | java.util.Iterator:next(...)@106 != null |
| presumption | org.jdom.Element:getAttribute(...)@100 != null |
| presumption | org.jdom.Element:getChild(...)@96 != null |
| presumption | org.jdom.Element:getChildren(...)@103 != null |
| post | return_value == &new Workspace(elementToWorkspa ce#1) |
| post | new ArrayList(Workspace#1) num objects == 1 |
| post | new Workspace(elementToWorkspace#1) num objects == 1 |
| post | return_value.collections == &new ArrayList(Workspace#1) |
| post | init'ed(return_value.title) |
| post | init'ed(return_value.titleType) |
| unanalyzed | call on java.util.ArrayList |
| unanalyzed | call on java.util.List:add |
| unanalyzed | call on java.lang.String:equals |
| unanalyzed | call on java.util.List:size |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on org.jdom.Element:getAttribute |
| unanalyzed | call on org.jdom.Attribute:getValue |
| unanalyzed | call on org.jdom.Element:getChild |
| unanalyzed | call on org.jdom.Element:getText |
| unanalyzed | call on org.jdom.Element:getChildren |
| unanalyzed | call on org.jdom.Element:getTextTrim |
| unanalyzed | call on com.sun.syndication.feed.atom.Category |
| unanalyzed | call on org.jdom.Element:getAttributeValue |
| unanalyzed | call on com.sun.syndication.feed.atom. Category:setTerm |
| unanalyzed | call on com.sun.syndication.feed.atom. Category:setLabel |
| unanalyzed | call on com.sun.syndication.feed.atom. Category:setScheme |
| test_vector | java.util.Iterator:hasNext(...)@105: {0}, {1} |
| test_vector | org.jdom.Element:getAttribute(...)@99: Addr_Set{null}, Inverse{null} |
| method | Element workspaceToElement(Workspace) |
| pre | init'ed(org/apache/roller/weblogger/webservices/ato mprotocol/AtomService.ATOM_FORMAT) |
| pre | init'ed(org/apache/roller/weblogger/webservices/ato mprotocol/AtomService.ATOM_PROTOCOL) |
| pre | space != null |
| pre | space.collections != null |
| pre | init'ed(space.title) |
| pre | init'ed(space.titleType) |
| presumption | col.accepts@127 != null |
| presumption | col.categories@127 != null |
| presumption | java.util.Iterator:next(...)@127 != null |
| post | return_value == &new Element(workspaceToElement #1) |
| post | new Element(workspaceToElement#1) num objects == 1 |
| unanalyzed | call on java.lang.String:equals |
| unanalyzed | call on java.util.List:iterator |
| unanalyzed | call on org.jdom.Element |
| unanalyzed | call on org.jdom.Element:setAttribute |
| unanalyzed | call on org.jdom.Element:setText |
| unanalyzed | call on org.jdom.Element:addContent |
| unanalyzed | call on com.sun.syndication.feed.atom. Category:getTerm |
| unanalyzed | call on com.sun.syndication.feed.atom. Category:getScheme |
| unanalyzed | call on com.sun.syndication.feed.atom. Category:getLabel |
| test_vector | space.titleType: Addr_Set{null}, Inverse{null} |
| test_vector | java.lang.String:equals(...)@121: {1}, {0} |
| test_vector | java.util.Iterator:hasNext(...)@126: {0}, {1} |