method

com.dmdirc.util.TextFile__static_init

method	void com.dmdirc.util.TextFile(String)
post	init'ed(this.charset)
post	this.file == &new File(TextFile#1)
post	new File(TextFile#1) num objects == 1
unanalyzed	call on java.nio.charset.Charset:defaultCharset

method	void com.dmdirc.util.TextFile(File)
post	init'ed(this.charset)
post	this.file == file
post	init'ed(this.file)

method	void com.dmdirc.util.TextFile(InputStream)
post	init'ed(this.charset)
post	this.is == is
post	init'ed(this.is)

method	void com.dmdirc.util.TextFile(File, Charset)
post	this.charset == charset
post	init'ed(this.charset)
post	this.file == file
post	init'ed(this.file)

method	void com.dmdirc.util.TextFile(InputStream, Charset)
post	this.charset == charset
post	init'ed(this.charset)
post	this.is == is
post	init'ed(this.is)

method	List getLines()
pre	init'ed(this.lines)
pre	(soft) init'ed(this.file)
pre	(soft) init'ed(this.is)
post	return_value == One-of{old this.lines, &new ArrayList(readLines#4)}
post	return_value != null
post	this.lines == return_value
post	new ArrayList(readLines#4) num objects <= 1
unanalyzed	call on java.io.FileInputStream
unanalyzed	call on java.io.InputStreamReader
unanalyzed	call on java.io.BufferedReader
unanalyzed	call on java.util.ArrayList
unanalyzed	call on java.io.BufferedReader:readLine
unanalyzed	call on java.util.List:add
unanalyzed	call on java.io.BufferedReader:close
test_vector	this.lines: Inverse{null}, Addr_Set{null}

method	void readLines()
pre	init'ed(this.file)
pre	(soft) init'ed(this.is)
post	this.lines == &new ArrayList(readLines#4)
post	new ArrayList(readLines#4) num objects == 1
test_vector	java.io.BufferedReader:readLine(...)@140: Addr_Set{null}, Inverse{null}

method	bool isWritable()
pre	init'ed(this.file)
post	init'ed(return_value)

method	void writeLines(List)
pre	lines != null
pre	this.file != null
test_vector	java.util.Iterator:hasNext(...)@170: {0}, {1}

method	File getFile()
pre	init'ed(this.file)
post	return_value == this.file
post	init'ed(return_value)

method	void delete()
pre	this.file != null