method

net.sourceforge.pebble.domain.FileMetaData__ static_init

method	void net.sourceforge.pebble.domain. FileMetaData(FileManager, String)
presumption	java.lang.String:lastIndexOf(...)@74 <= 232-2
post	this.context == context
post	init'ed(this.context)
post	this.name != null
post	this.path != null
test_vector	absolutePath: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:endsWith(...)@65: {0}, {1}
test_vector	java.lang.String:equals(...)@61: {1}, {0}
test_vector	java.lang.String:equals(...)@61: {0}, {1}
test_vector	java.lang.String:indexOf(...)@69: {-231.. -1}, {0..232-1}
test_vector	java.lang.String:length(...)@71: {1.. 232-1}, {0}
test_vector	java.lang.String:startsWith(...)@81: {1}, {0}

method	String getName()
pre	init'ed(this.name)
post	return_value == this.name
post	init'ed(return_value)

method	void setName(String)
post	this.name == name
post	init'ed(this.name)

method	Date getLastModified()
pre	init'ed(this.lastModified)
post	return_value == this.lastModified
post	init'ed(return_value)

method	void setLastModified(Date)
post	this.lastModified == lastModified
post	init'ed(this.lastModified)

method	bool isDirectory()
pre	init'ed(this.directory)
post	return_value == this.directory
post	init'ed(return_value)

method	void setDirectory(bool)
post	this.directory == directory
post	init'ed(this.directory)

method	String getPath()
pre	init'ed(this.path)
post	return_value == this.path
post	init'ed(return_value)

method	String getAbsolutePath()
pre	init'ed(this.name)
pre	this.path != null
post	return_value != null
test_vector	java.lang.String:endsWith(...)@116: {1}, {0}

method	String getUrl()
pre	init'ed(this.type)
pre	(soft) init'ed(this.directory)
pre	(soft) init'ed(this.name)
pre	(soft) this.path != null
post	init'ed(return_value)
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
test_vector	this.directory: {0}, {1}
test_vector	this.type: Addr_Set{null}, Inverse{null}
test_vector	java.lang.String:endsWith(...)@134: {1}, {0}
test_vector	java.lang.String:equals(...)@126: {0}, {1}
test_vector	java.lang.String:equals(...)@128: {0}, {1}
test_vector	java.lang.String:equals(...)@130: {0}, {1}

method	bool isEditable()
pre	init'ed(this.directory)
pre	(soft) this.name != null
post	init'ed(return_value)
test_vector	this.directory: {0}, {1}
test_vector	java.lang.String:endsWith(...)@147: {1}, {0}
test_vector	java.lang.String:endsWith(...)@148: {1}, {0}
test_vector	java.lang.String:endsWith(...)@149: {1}, {0}
test_vector	java.lang.String:endsWith(...)@150: {1}, {0}
test_vector	java.lang.String:endsWith(...)@151: {1}, {0}
test_vector	java.lang.String:endsWith(...)@152: {1}, {0}
test_vector	java.lang.String:endsWith(...)@153: {1}, {0}
test_vector	java.lang.String:endsWith(...)@154: {1}, {0}

method	long getSize()
pre	init'ed(this.size)
post	return_value == this.size
post	init'ed(return_value)

method	double getSizeInKB()
pre	init'ed(this.size)
post	return_value == (float) (this.size)/1024
post	return_value in (-Inf..+Inf)

method	void setSize(long)
post	this.size == size
post	init'ed(this.size)

method	void setType(String)
post	this.type == type
post	init'ed(this.type)

method	File getFile()
pre	this.context != null
pre	init'ed(this.context.root)
pre	init'ed(this.name)
pre	this.path != null
post	return_value == &new File(getFile#1*)
post	new File(getFile#1*) num objects == 1
unanalyzed	call on java.lang.String:endsWith
unanalyzed	call on java.lang.String:valueOf
unanalyzed	call on java.lang.String:startsWith
unanalyzed	call on java.lang.String:substring
unanalyzed	call on java.io.File