Messages

method

net.sourceforge.pebble.domain.Response__static_ init

method	void net.sourceforge.pebble.domain.Response()
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	this.spamScore == 0
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

method	void net.sourceforge.pebble.domain. Response(String, String, Date, State, BlogEntry)
pre	blogEntry != null
post	this.blogEntry == blogEntry
post	this.blogEntry != null
post	init'ed(this.date)
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	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 net.sourceforge.pebble.util. StringUtils:transformHTML
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 setState
unanalyzed	call on java.util.Calendar:setTime
unanalyzed	call on areEventsEnabled
unanalyzed	call on java.util.Calendar:getTime
unanalyzed	call on java.lang.String:length
unanalyzed	call on getBlogEntry
unanalyzed	call on net.sourceforge.pebble.domain. Response:setState
unanalyzed	call on isApproved
unanalyzed	call on net.sourceforge.pebble.api.event. PebbleEvent
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:addEvent
unanalyzed	call on getState
unanalyzed	call on isRejected
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.EventObject
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:getTitle

method	long getId()
pre	this.date != null
post	init'ed(return_value)

method	String getGuid()
pre	this.blogEntry != null
pre	this.date != null
post	return_value != null
unanalyzed	call on java.util.Date:getTime

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

method	String getTitle()
pre	init'ed(this.title)
post	return_value == this.title
post	init'ed(return_value)

method	void setTitle(String)
post	init'ed(this.title)

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

method	String getIpAddress()
pre	init'ed(this.ipAddress)
post	return_value == this.ipAddress
post	init'ed(return_value)

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

method	Date getDate()
pre	init'ed(this.date)
post	return_value == this.date
post	init'ed(return_value)

method	void setDate(Date)
pre	this.blogEntry != null
presumption	net.sourceforge.pebble.domain.Blog:getCalendar(... )@185 != null
presumption	net.sourceforge.pebble.domain.BlogEntry:getBlog(... )@185 != null
post	init'ed(this.date)
test_vector	date: Inverse{null}, Addr_Set{null}

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

info method not available -- call on Calendar net.sourceforge.pebble.domain. Blog:getCalendar()

method	BlogEntry getBlogEntry()
pre	init'ed(this.blogEntry)
post	return_value == this.blogEntry
post	init'ed(return_value)

method	void setBlogEntry(BlogEntry)
post	this.blogEntry == blogEntry
post	init'ed(this.blogEntry)

method	int getSpamScore()
pre	init'ed(this.spamScore)
post	return_value == this.spamScore
post	init'ed(return_value)

method	void incrementSpamScore()
pre	this.spamScore <= 2³²-2
post	this.spamScore == old this.spamScore + 1
post	this.spamScore >= -2³¹+1

method	void setRejected()
post	this.state == One-of{&net.sourceforge.pebble. domain.State__static_init.new State(State__static_i nit#2), old this.state}
unanalyzed	call on net.sourceforge.pebble.domain. Response:setState
unanalyzed	call on isApproved
unanalyzed	call on net.sourceforge.pebble.api.event. PebbleEvent
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:addEvent
unanalyzed	call on setState
unanalyzed	call on isRejected
unanalyzed	call on java.lang.String:equals
unanalyzed	call on areEventsEnabled
unanalyzed	call on java.util.EventObject
unanalyzed	call on getBlogEntry
unanalyzed	call on getState

method	bool isRejected()
pre	this.state != null
pre	(soft) net.sourceforge.pebble.domain.State__static_ init.new State(State__static_init#2).name != null
pre	(soft) init'ed(this.state.name)
post	init'ed(return_value)
unanalyzed	call on java.lang.String:equals

method	void setApproved()
post	this.state == One-of{&net.sourceforge.pebble. domain.State__static_init.new State(State__static_i nit#1), old this.state}
unanalyzed	call on net.sourceforge.pebble.domain. Response:setState
unanalyzed	call on isApproved
unanalyzed	call on net.sourceforge.pebble.api.event. PebbleEvent
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:addEvent
unanalyzed	call on isRejected
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.EventObject
unanalyzed	call on setState
unanalyzed	call on areEventsEnabled
unanalyzed	call on getBlogEntry
unanalyzed	call on getState

method	bool isApproved()
pre	this.state != null
pre	(soft) net.sourceforge.pebble.domain.State__static_ init.new State(State__static_init#1).name != null
pre	(soft) init'ed(this.state.name)
post	init'ed(return_value)
unanalyzed	call on java.lang.String:equals

method	void setPending()
post	this.state == One-of{&net.sourceforge.pebble. domain.State__static_init.new State(State__static_i nit#3), old this.state}
unanalyzed	call on net.sourceforge.pebble.domain. Response:setState
unanalyzed	call on isApproved
unanalyzed	call on net.sourceforge.pebble.api.event. PebbleEvent
unanalyzed	call on net.sourceforge.pebble.domain. BlogEntry:addEvent
unanalyzed	call on isRejected
unanalyzed	call on java.lang.String:equals
unanalyzed	call on java.util.EventObject
unanalyzed	call on setState
unanalyzed	call on areEventsEnabled
unanalyzed	call on getBlogEntry
unanalyzed	call on getState

method	bool isPending()
pre	this.state != null
pre	(soft) net.sourceforge.pebble.domain.State__static_ init.new State(State__static_init#3).name != null
pre	(soft) init'ed(this.state.name)
post	init'ed(return_value)
unanalyzed	call on java.lang.String:equals

	info	method not available	-- call on Blog net.sourceforge.pebble.domain. BlogEntry:getBlog()
	info	method not available	-- call on Calendar net.sourceforge.pebble.domain. Blog:getCalendar()