RollingList.java

RollingList.java

current inspection = 2009-09-03 21:56:13 (id #1)

Filter Options

Annotation Kind:

pre

presumption

post

unanalyzed

test_vector

bool add(Object)

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

Kind	Annotation Text
pre	this.items != null

void com.dmdirc.util.RollingList(int)

Kind	Annotation Text
post	init'ed(this.capacity)
post	new ArrayList(RollingList#1) num objects == 1
post	this.addEmpty == 0
post	this.capacity == capacity
post	this.items == &new ArrayList(RollingList#1)
post	this.position == 0

void com.dmdirc.util.RollingList(int, Object)

Kind	Annotation Text
post	init'ed(this.capacity)
post	init'ed(this.empty)
post	new ArrayList(RollingList#1) num objects == 1
post	this.addEmpty == 1
post	this.capacity == capacity
post	this.empty == empty
post	this.items == &new ArrayList(RollingList#1)
post	this.position == 0

com.dmdirc.util.RollingList__static_init

Kind	Annotation Text

bool contains(Object)

Kind	Annotation Text
pre	this.items != null
post	init'ed(return_value)

Object get(int)

Kind	Annotation Text
pre	this.items != null
post	init'ed(return_value)

Kind	Annotation Text
post	new ArrayList(getList#1) num objects == 1
post	return_value == &new ArrayList(getList#1)

Object getNext()

Kind	Annotation Text
pre	(soft) init'ed(this.addEmpty)
pre	(soft) init'ed(this.empty)
pre	this.items != null
pre	this.position <= 2³²-2
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}

int getPosition()

Kind	Annotation Text
pre	init'ed(this.position)
post	init'ed(return_value)
post	return_value == this.position

Object getPrevious()

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

Kind	Annotation Text
pre	(soft) init'ed(this.addEmpty)
pre	init'ed(this.position)
pre	this.items != null
post	init'ed(return_value)

bool hasPrevious()

Kind	Annotation Text
pre	init'ed(this.position)
post	init'ed(return_value)

Kind	Annotation Text
pre	this.items != null
post	init'ed(return_value)

bool remove(Object)

Kind	Annotation Text
pre	this.items != null
post	init'ed(return_value)

void seekToEnd()

Kind	Annotation Text
pre	this.items != null
post	init'ed(this.position)

void seekToStart()

Kind	Annotation Text
post	this.position == 0

void setPosition(int)

Kind	Annotation Text
post	init'ed(this.position)
post	this.position == position