Messages

Last Msg First Msg

method

com.dmdirc.util.RollingList__static_init

method	void com.dmdirc.util.RollingList(int)
post	this.addEmpty == 0
post	this.position == 0
post	this.capacity == capacity
post	init'ed(this.capacity)
post	this.items == &new ArrayList(RollingList#1)
post	new ArrayList(RollingList#1) num objects == 1

method	void com.dmdirc.util.RollingList(int, Object)
post	this.addEmpty == 1
post	new ArrayList(RollingList#1) num objects == 1
post	this.capacity == capacity
post	init'ed(this.capacity)
post	this.empty == empty
post	init'ed(this.empty)
post	this.items == &new ArrayList(RollingList#1)
post	this.position == 0

method	bool remove(Object)
pre	this.items != null
post	init'ed(return_value)

method	bool isEmpty()
pre	this.items != null
post	init'ed(return_value)

method	Object get(int)
pre	this.items != null
post	init'ed(return_value)

method	bool contains(Object)
pre	this.items != null
post	init'ed(return_value)

method	void clear()
pre	this.items != null

method	bool add(Object)
pre	this.capacity >= -2³¹+1
pre	this.items != null
pre	(soft) this.position >= -2³¹+1
post	init'ed(return_value)
post	init'ed(this.position)
post	this.position - old this.position in {-6_442_450_943..0}

Prev Msg Next Msg

overflow

click for all messages in this file Low Prob.

check that this.position in {-2³¹+1.. 2³²}

Prev Msg Next Msg

method	int getPosition()
pre	init'ed(this.position)
post	return_value == this.position
post	init'ed(return_value)

method	void setPosition(int)
post	this.position == position
post	init'ed(this.position)

method	bool hasNext()
pre	this.items != null
pre	init'ed(this.position)
pre	(soft) init'ed(this.addEmpty)
post	init'ed(return_value)

method	Object getNext()
pre	this.position <= 2³²-2
pre	this.items != null
pre	(soft) init'ed(this.addEmpty)
pre	(soft) init'ed(this.empty)
post	init'ed(return_value)
post	this.position == old this.position + 1
post	this.position >= -2³¹+1
unanalyzed	call on java.util.List:get
test_vector	this.addEmpty: {1}, {0}

method	bool hasPrevious()
pre	init'ed(this.position)
post	init'ed(return_value)

method	Object getPrevious()
pre	this.position >= -2³¹+1
pre	this.items != null
post	init'ed(return_value)
post	this.position == old this.position - 1
post	this.position <= 2³²-2
unanalyzed	call on java.util.List:get

method	void seekToEnd()
pre	this.items != null
post	init'ed(this.position)

method	void seekToStart()
post	this.position == 0

method	List getList()
post	return_value == &new ArrayList(getList#1)
post	new ArrayList(getList#1) num objects == 1