Messages

Last Msg First Msg

method

net.sourceforge.pebble.domain.Comment__static_ init

method	void net.sourceforge.pebble.domain.Comment()
post	this.authenticated == 0
post	this.spamScore == 0
post	this.comments == &new ArrayList(Comment#1)
post	this.events == &new ArrayList(Content#1)
post	init'ed(this.eventsEnabled)
post	this.propertyChangeEvents == &new ArrayList(Content#3)
post	this.propertyChangeSupport == &new PropertyChangeSupport(Content#2)
post	new ArrayList(Comment#1) num objects == 1
post	new ArrayList(Content#1) num objects == 1
post	new ArrayList(Content#3) num objects == 1
post	new PropertyChangeSupport(Content#2) num objects == 1
unanalyzed	call on java.util.ArrayList
unanalyzed	call on net.sourceforge.pebble.domain.Content
unanalyzed	call on java.beans.PropertyChangeSupport
unanalyzed	call on java.beans.PropertyChangeSupport:addPropert yChangeListener

method	void net.sourceforge.pebble.domain.Comment(String, String, String, String, String, String, Date, State, BlogEntry)
pre	blogEntry != null
post	init'ed(this.authenticated)
post	this.author == One-of{&"Anonymous", author}
post	this.author != null
post	this.blogEntry == blogEntry
post	this.blogEntry != null
post	this.body == One-of{null, body}
post	init'ed(this.body)
post	this.comments == &new ArrayList(Comment#1)
post	init'ed(this.date)
post	init'ed(this.email)
post	this.events == &new ArrayList(Content#1)
post	init'ed(this.eventsEnabled)
post	this.ipAddress == One-of{null, ipAddress}
post	init'ed(this.ipAddress)
post	this.propertyChangeEvents == &new ArrayList(Content#3)
post	this.propertyChangeSupport == &new PropertyChangeSupport(Content#2)
post	init'ed(this.spamScore)
post	possibly_updated(this.state)
post	possibly_updated(this.title)
post	init'ed(this.website)
post	new ArrayList(Comment#1) num objects == 1
post	new ArrayList(Content#1) num objects == 1
post	new ArrayList(Content#3) num objects == 1
post	new PropertyChangeSupport(Content#2) num objects == 1
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.beans.PropertyChangeSupport
unanalyzed	call on java.beans.PropertyChangeSupport:addPropert yChangeListener
unanalyzed	call on java.lang.String:length
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:getTitle
unanalyzed	call on net.sourceforge.pebble.util. StringUtils:filterHTML
unanalyzed	call on areEventsEnabled
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on getBlogEntry
unanalyzed	call on net.sourceforge.pebble.util. StringUtils:transformHTML
unanalyzed	call on net.sourceforge.pebble.api.event. PebbleEvent
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:addEvent
unanalyzed	call on java.lang.String:equals
unanalyzed	call on isApproved
unanalyzed	call on getState
unanalyzed	call on isRejected
unanalyzed	call on java.util.Date
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:getBlog
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed	call on net.sourceforge.pebble.domain.Content
unanalyzed	call on java.util.Calendar:setTime
unanalyzed	call on java.util.Calendar:getTime
unanalyzed	call on setState
unanalyzed	call on net.sourceforge.pebble.domain. Response:setState
unanalyzed	call on java.util.EventObject

method	String getBody()
pre	init'ed(this.body)
post	return_value == this.body
post	init'ed(return_value)

method	String getContent()
pre	init'ed(this.body)
post	return_value == this.body
post	init'ed(return_value)

method	String getTruncatedBody()
pre	(soft) init'ed(this.body)
pre	(soft) init'ed(this.excerpt)
post	init'ed(return_value)
unanalyzed	call on java.lang.String:length
unanalyzed	call on getContent
unanalyzed	call on net.sourceforge.pebble.util. StringUtils:truncate

method	void setTitle(String)
pre	(soft) init'ed(this.blogEntry)
post	this.title != null
test_vector	this.blogEntry: Addr_Set{null}, Inverse{null}
test_vector	title: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:length(...)@126: {1.. 2³²-1}, {0}

info method not available -- call on String net.sourceforge.pebble.domain. BlogEntry:getTitle()

method	void setBody(String)
post	this.body == One-of{null, body}
post	init'ed(this.body)
test_vector	body: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:length(...)@143: {1.. 2³²-1}, {0}

method	String getAuthor()
pre	init'ed(this.author)
post	return_value == this.author
post	init'ed(return_value)

method	String getSourceName()
pre	init'ed(this.author)
post	return_value == this.author
post	init'ed(return_value)

method	void setAuthor(String)
post	this.author == One-of{&"Anonymous", author}
post	this.author != null
test_vector	author: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:length(...)@175: {1.. 2³²-1}, {0}

method	String getEmail()
pre	init'ed(this.email)
post	return_value == this.email
post	init'ed(return_value)

method	void setEmail(String)
post	init'ed(this.email)
test_vector	email: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:length(...)@197: {1.. 2³²-1}, {0}

info method not available -- call on String net.sourceforge.pebble.util. StringUtils:transformHTML(String)

method	String getWebsite()
pre	init'ed(this.website)
post	return_value == this.website
post	init'ed(return_value)

method	String getSourceLink()
pre	init'ed(this.website)
post	return_value == this.website
post	init'ed(return_value)

method	void setWebsite(String)
post	init'ed(this.website)
test_vector	java.lang.String:length(...)@229: {1.. 2³²-1}, {0}
test_vector	java.lang.String:startsWith(...)@232: {1}, {0}
test_vector	java.lang.String:startsWith(...)@233: {1}, {0}
test_vector	java.lang.String:startsWith(...)@234: {1}, {0}
test_vector	java.lang.String:startsWith(...)@235: {1}, {0}
test_vector	net.sourceforge.pebble.util.StringUtils:filterHTML( ...)@228: Addr_Set{null}, Inverse{null}

info method not available -- call on String net.sourceforge.pebble.util. StringUtils:filterHTML(String)

method	String getPermalink()
pre	init'ed(this.blogEntry)
pre	(soft) init'ed(this.blogEntry.permalink)
pre	(soft) this.blogEntry.blog != null
pre	(soft) this.date != null
post	return_value != null
post	init'ed(this.blogEntry.permalink)
pre	(soft) net/sourceforge/pebble/domain/BlogManager. instance != null
unanalyzed	call on java.util.Date:getTime
pre	(soft) init'ed(net/sourceforge/pebble/domain/BlogMa nager.instance.multiBlog)
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:substring
unanalyzed	call on getUrl
pre	(soft) init'ed(this.blogEntry.blog.id)
pre	(soft) this.blogEntry.blog.permalinkProvider != null
unanalyzed	call on getPermalinkProvider
unanalyzed	call on java.lang.String:length
unanalyzed	call on java.lang.String:indexOf
unanalyzed	call on net.sourceforge.pebble.PebbleContext:getIns tance
unanalyzed	call on net.sourceforge.pebble.PebbleContext:getCon figuration
unanalyzed	call on getPermalink
test_vector	this.blogEntry: Addr_Set{null}, Inverse{null}

method	Comment getParent()
pre	init'ed(this.parent)
post	return_value == this.parent
post	init'ed(return_value)

method	void setParent(Comment)
post	this.parent == parent
post	init'ed(this.parent)

method	int getNumberOfParents()
pre	init'ed(this.parent)
pre	(soft) init'ed(this...parent)
post	return_value >= 0

Prev Msg Next Msg

click for all messages in this file low

overflow check might fail: requires count in -2³¹-1..2³²-2

Prev Msg Next Msg

method	void addComment(Comment)
pre	(soft) this.comments != null
post	comment.parent == One-of{old comment.parent, this}
test_vector	comment: Addr_Set{null}, Inverse{null}
test_vector	java.util.List:contains(...)@295: {1}, {0}

method	void removeComment(Comment)
unanalyzed	call on areEventsEnabled
unanalyzed	call on getBlogEntry
pre	(soft) comment.blogEntry != null
pre	(soft) comment.comments != null
pre	(soft) init'ed(comment.eventsEnabled)
pre	(soft) this.blogEntry != null
pre	(soft) this.comments != null
pre	(soft) init'ed(this.eventsEnabled)
presumption	child.blogEntry@309 != null
presumption	child.comments@309 != null
post	comment.parent == One-of{old comment.parent, null}
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.util.List:contains
unanalyzed	call on java.util.List:iterator
unanalyzed	call on removeComment
unanalyzed	call on java.util.List:remove
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:addEvent
unanalyzed	call on java.util.EventObject
test_vector	comment: Addr_Set{null}, Inverse{null}
test_vector	java.util.Iterator:hasNext(...)@309: {1}, {0}
test_vector	java.util.List:contains(...)@307: {0}, {1}

info method not available -- call on void net.sourceforge.pebble.domain. BlogEntry:addEvent(PebbleEvent)

method	List getComments()
pre	init'ed(this.comments)
post	return_value == &new ArrayList(getComments#1)
post	new ArrayList(getComments#1) num objects == 1

method	Object clone()
pre	init'ed(this.authenticated)
pre	init'ed(this.author)
pre	this.blogEntry != null
pre	init'ed(this.body)
pre	init'ed(this.date)
pre	init'ed(this.email)
pre	init'ed(this.ipAddress)
pre	init'ed(this.parent)
pre	init'ed(this.state)
pre	init'ed(this.title)
pre	init'ed(this.website)
post	return_value == &new Comment(clone#1)
post	new ArrayList(Comment#1) num objects == 1
post	new ArrayList(Content#1) num objects == 1
unanalyzed	call on areEventsEnabled
unanalyzed	call on getBlogEntry
post	new ArrayList(Content#3) num objects == 1
post	new Comment(clone#1) num objects == 1
post	new PropertyChangeSupport(Content#2) num objects == 1
unanalyzed	call on getState
post	return_value.authenticated == this.authenticated
post	init'ed(return_value.authenticated)
post	return_value.author == One-of{&"Anonymous", this.author}
post	return_value.author != null
post	return_value.blogEntry == this.blogEntry
unanalyzed	call on net.sourceforge.pebble.domain.Response
unanalyzed	call on net.sourceforge.pebble.domain.Content
post	return_value.blogEntry != null
post	return_value.body == One-of{null, this.body}
post	init'ed(return_value.body)
post	return_value.comments == &new ArrayList(Comment #1)
post	init'ed(return_value.date)
post	init'ed(return_value.email)
post	return_value.events == &new ArrayList(Content#1 )
post	init'ed(return_value.eventsEnabled)
post	return_value.ipAddress == One-of{null, this.ipAddress}
post	init'ed(return_value.ipAddress)
post	return_value.parent == this.parent
post	init'ed(return_value.parent)
post	return_value.propertyChangeEvents == &new ArrayList(Content#3)
post	return_value.propertyChangeSupport == &new PropertyChangeSupport(Content#2)
post	init'ed(return_value.spamScore)
post	possibly_updated(return_value.state)
post	possibly_updated(return_value.title)
post	init'ed(return_value.website)
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.beans.PropertyChangeSupport
unanalyzed	call on java.beans.PropertyChangeSupport:addPropert yChangeListener
unanalyzed	call on java.lang.String:length
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:getTitle
unanalyzed	call on net.sourceforge.pebble.util. StringUtils:filterHTML
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on net.sourceforge.pebble.util. StringUtils:transformHTML
unanalyzed	call on net.sourceforge.pebble.api.event. PebbleEvent
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:addEvent
unanalyzed	call on java.lang.String:equals
unanalyzed	call on isApproved
unanalyzed	call on isRejected
unanalyzed	call on java.util.Date
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:getBlog
unanalyzed	call on net.sourceforge.pebble.domain. Blog:getCalendar
unanalyzed	call on java.util.Calendar:setTime
unanalyzed	call on java.util.Calendar:getTime
unanalyzed	call on setState
unanalyzed	call on net.sourceforge.pebble.domain. Response:setState
unanalyzed	call on java.util.EventObject

method	bool equals(Object)
pre	(soft) o.blogEntry != null
pre	(soft) o.date != null
pre	(soft) this.blogEntry != null
pre	(soft) this.date != null
presumption	net.sourceforge.pebble.domain.BlogEntry:getId(... )@355 != null
post	init'ed(return_value)
unanalyzed	call on java.util.Date:getTime
test_vector	this == o: {0}, {1}
test_vector	java.lang.String:equals(...)@355: {0}, {1}

info method not available -- call on String net.sourceforge.pebble.domain. BlogEntry:getId()

method	int hashCode()
pre	this.date != null
post	init'ed(return_value)
unanalyzed	call on java.util.Date:getTime

method	void setState(State)
unanalyzed	call on getState
pre	init'ed(this.state)
pre	init'ed(this.eventsEnabled)
pre	(soft) net.sourceforge.pebble.domain.State__static_ init.new State(State__static_init#1).name != null
pre	(soft) net.sourceforge.pebble.domain.State__static_ init.new State(State__static_init#2).name != null
pre	(soft) s != null
pre	(soft) init'ed(s.name)
pre	(soft) this.blogEntry != null
post	this.state == s
post	(soft) this.state != null
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.EventObject
test_vector	this.eventsEnabled: {0}, {1}

info method not available -- call on void net.sourceforge.pebble.domain. BlogEntry:addEvent(PebbleEvent)

method	bool isAuthenticated()
pre	init'ed(this.authenticated)
post	return_value == this.authenticated
post	init'ed(return_value)

method	void setAuthenticated(bool)
post	this.authenticated == authenticated
post	init'ed(this.authenticated)