File (JML and MultiJava documentation)

Class Specifications

public invariant (this.prefix == null) ==> !this.names.isEmpty();
public invariant ( \forall java.lang.Object o; java.io.File.toDelete.has(o); o instanceof java.io.File);
initially java.io.File.separator.equals(java.lang.System.getProperty("java.io.tmpdir"));
initially java.io.File.separator.equals(java.lang.System.getProperty("file.separator"));
initially java.io.File.pathSeparator.equals(java.lang.System.getProperty("path.separator"));
initially java.io.File.separatorChar == java.io.File.separator.charAt(0);
initially java.io.File.pathSeparatorChar == java.io.File.pathSeparator.charAt(0);

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Specifications inherited from interface Comparable

instance public invariant ( \forall java.lang.Comparable x; x != null; x.compareTo(x) == 0);
instance public invariant ( \forall java.lang.Comparable x, y; x != null&&y != null&&this.definedComparison(x,y)&&this.definedComparison(y,x); this.sgn(x.compareTo(y)) == -this.sgn(y.compareTo(x)));
instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == n ==> this.sgn(x.compareTo(z)) == n));
instance public invariant ( \forall int n; n == -1||n == 1; ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(y,z)&&this.definedComparison(x,z); (this.sgn(x.compareTo(y)) == 0&&this.sgn(y.compareTo(z)) == n||this.sgn(x.compareTo(y)) == n&&this.sgn(y.compareTo(z)) == 0) ==> this.sgn(x.compareTo(z)) == n));
instance public invariant ( \forall java.lang.Comparable x, y, z; x != null&&y != null&&z != null&&this.definedComparison(x,y)&&this.definedComparison(x,z)&&this.definedComparison(y,z); this.sgn(x.compareTo(y)) == 0 ==> this.sgn(x.compareTo(z)) == this.sgn(y.compareTo(z)));

Model Field Summary

static JMLDataGroup fileSystem


JMLObjectSequence names


String prefix


static JMLObjectSet toDelete


Model fields inherited from class java.lang.Object

_getClass, objectState, theString

Ghost Field Summary

static String tempDir


Ghost fields inherited from class java.lang.Object

objectTimesFinalized, owner

Field Summary

static String pathSeparator


static char pathSeparatorChar


static String separator


static char separatorChar


Constructor Summary

File(File parent, String child)


File(String pathname)


File(String parent, String child)


File(URI uri)


Model Method Summary

String concatenate(JMLObjectSequence strs)


JMLObjectSequence extractNames(String pathname)


String extractPrefix(String pathname)


Model methods inherited from class java.lang.Object

hashValue

Model methods inherited from interface java.lang.Comparable

definedComparison, sgn

Method Summary

boolean canRead()


boolean canWrite()


int compareTo(non_null File pathname)


int compareTo(non_null Object o)


boolean createNewFile()


static File createTempFile(String prefix, String suffix)


static File createTempFile(String prefix, String suffix, File directory)


boolean delete()


void deleteOnExit()


boolean equals(nullable Object obj)


boolean exists()


File getAbsoluteFile()


String getAbsolutePath()


File getCanonicalFile()


String getCanonicalPath()


String getName()


String getParent()


File getParentFile()


String getPath()


int hashCode()


boolean isAbsolute()


boolean isDirectory()


boolean isFile()


boolean isHidden()


long lastModified()


long length()


String[] list()


String[] list(FilenameFilter filter)


File[] listFiles()


File[] listFiles(FileFilter filter)


File[] listFiles(FilenameFilter filter)


static File[] listRoots()


boolean mkdir()


boolean mkdirs()


boolean renameTo(File dest)


boolean setLastModified(long time)


boolean setReadOnly()


String toString()


URI toURI()


URL toURL()


Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Model Field Detail

prefix

public String prefix

names

public JMLObjectSequence names

fileSystem

public static JMLDataGroup fileSystem

toDelete

public static JMLObjectSet toDelete

Ghost Field Detail

tempDir

public static final String tempDir

Field Detail

separator

public static final String separator

pathSeparator

public static final String pathSeparator

separatorChar

public static final char separatorChar

pathSeparatorChar

public static final char pathSeparatorChar

Constructor Detail

File

public File(String pathname)

Specifications: pure: public normal_behavior
requires pathname != null;
assignable prefix, names;
ensures this.prefix.equals(this.extractPrefix(pathname));
ensures this.names.equals(this.extractNames(pathname));
also: public exceptional_behavior
requires pathname == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

File

public File(String parent,
            String child)

Specifications: pure: public normal_behavior
requires parent == null&&child != null;
assignable prefix, names;
ensures this.prefix.equals(this.extractPrefix(child));
ensures this.names.equals(this.extractNames(child));
also: public normal_behavior
requires parent != null&&child != null;
assignable prefix, names;
ensures this.prefix.equals(this.extractPrefix(parent));
ensures this.names.equals(this.extractNames(parent+child));
also: public exceptional_behavior
requires child == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

File

public File(File parent,
            String child)

Specifications: pure: public normal_behavior
requires parent == null&&child != null;
assignable prefix, names;
ensures this.prefix.equals(this.extractPrefix(child));
ensures this.names.equals(this.extractNames(child));
also: public normal_behavior
requires parent != null&&child != null;
assignable prefix, names;
ensures this.prefix.equals(parent.prefix);
ensures this.names.equals(parent.names.concat(this.extractNames(child)));
also: public exceptional_behavior
requires child == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

File

public File(URI uri)

Specifications: pure: public behavior
requires uri != null;
assignable prefix, names;
ensures (* a new File instance by converting the given file: URI into an abstract pathname. *);
signals_only java.lang.IllegalArgumentException;
also: public exceptional_behavior
requires uri == null;
assignable \nothing;
signals_only java.lang.NullPointerException;

Model Method Detail

extractPrefix

public String extractPrefix(String pathname)

Specifications: pure: public normal_behavior
requires pathname != null;
ensures \result != null&&pathname.startsWith(\result );

extractNames

public JMLObjectSequence extractNames(String pathname)

Specifications: pure: public normal_behavior
requires pathname != null&&!pathname.endsWith(java.io.File.separator);
ensures \result != null;
ensures (this.prefix+this.concatenate(\result )).equals(pathname);
also: public normal_behavior
requires pathname != null&&pathname.endsWith(java.io.File.separator);
ensures \result != null;
ensures (this.prefix+this.concatenate(\result )).equals(pathname.substring(0,pathname.length()-2));

concatenate

public String concatenate(JMLObjectSequence strs)

Specifications: pure: requires strs != null&&( \forall int i; 0 <= i&&i < strs.int_size(); strs.get(i) instanceof java.lang.String);

Method Detail

getName

public String getName()

Specifications: pure: public normal_behavior
requires this.names.isEmpty();
assignable \nothing;
ensures \result .equals("");
also: public normal_behavior
requires !this.names.isEmpty();
assignable \nothing;
ensures \result != null&&\result .equals(this.names.last());

getParent

public String getParent()

Specifications: pure: public normal_behavior
requires this.names.isEmpty();
assignable \nothing;
ensures \result == null;
also: public normal_behavior
requires this.prefix == null;
assignable \nothing;
ensures \result .equals(this.concatenate(this.names.header()));
also: public normal_behavior
requires this.prefix != null&&!this.names.isEmpty();
assignable \nothing;
ensures \result != null&&\result .equals(this.prefix+this.concatenate(this.names.header()));

getParentFile

public File getParentFile()

Specifications: pure: public normal_behavior
requires this.names.isEmpty();
assignable \nothing;
ensures \result == null;
also: public normal_behavior
requires this.prefix == null;
assignable \nothing;
ensures \result .prefix.equals(null);
also: public normal_behavior
requires this.prefix != null;
assignable \nothing;
ensures \result != null&&\result .names.equals(this.names.header())&&\result .prefix.equals(this.prefix);

getPath

public String getPath()

Specifications: pure: public normal_behavior
requires this.prefix == null;
assignable \nothing;
ensures \result .equals(this.concatenate(this.names));
also: public normal_behavior
requires this.prefix != null;
assignable \nothing;
ensures \result .equals(this.prefix+this.concatenate(this.names));

isAbsolute

public boolean isAbsolute()

Specifications: pure: public normal_behavior
assignable \nothing;
ensures \result <==> (this.prefix != null)&&this.prefix.endsWith(java.io.File.separator);

getAbsolutePath

public String getAbsolutePath()

Specifications: pure: public normal_behavior
requires this.prefix == null;
assignable \nothing;
ensures \result .equals(java.lang.System.getProperty("usr.dir")+this.concatenate(this.names));
also: public normal_behavior
requires this.prefix != null&&!this.names.isEmpty();
assignable \nothing;
ensures \result .equals(this.prefix+this.concatenate(this.names));

getAbsoluteFile

public File getAbsoluteFile()

Specifications: pure: public normal_behavior
requires this.prefix == null;
assignable \nothing;
ensures \result .prefix.equals(this.extractPrefix(java.lang.System.getProperty("usr.dir")));
ensures \result .names.equals(this.extractNames(java.lang.System.getProperty("usr.dir")).concat(this.names));
also: public normal_behavior
requires this.prefix != null&&!this.names.isEmpty();
assignable \nothing;
ensures \result .prefix.equals(this.prefix)&&\result .names.equals(this.names);

getCanonicalPath

public String getCanonicalPath()
                        throws IOException

Throws:: IOException

Specifications:: public behavior
assignable \nothing;
ensures \result != null;
ensures (* returns the canonical pathname string denoting the same file or directory as this abstract pathname *);
signals_only java.io.IOException;

getCanonicalFile

public File getCanonicalFile()
                      throws IOException

Throws:: IOException

Specifications:: public behavior
assignable \nothing;
ensures \result != null;
ensures (* returns the canonical pathname string denoting the same file or directory as this abstract pathname *);
signals_only java.io.IOException;

toURL

public URL toURL()
          throws MalformedURLException

Throws:: MalformedURLException

Specifications:: public behavior
assignable \nothing;
ensures \result != null;
ensures (* \result is this abstract pathname converted into file:URL *);
signals_only java.net.MalformedURLException;

toURI

public URI toURI()

Specifications:: public normal_behavior
assignable \nothing;
ensures \result != null;
ensures (* \result is an absolute, hierarchical URI with a scheme equal to "file", a path representing this abstract pathname, and undefined authority, query, and fragment components *);

canRead

public boolean canRead()

Specifications: pure: public behavior
assignable \nothing;
ensures (* true if and only if this file has read access. *);
signals_only java.lang.SecurityException;

canWrite

public boolean canWrite()

Specifications: pure: public behavior
assignable \nothing;
ensures (* true if and only if this file has write access. *);
signals_only java.lang.SecurityException;

exists

public boolean exists()

Specifications: pure: public behavior
assignable \nothing;
ensures (* true if and only if this file exists. *);
signals_only java.lang.SecurityException;

isDirectory

public boolean isDirectory()

Specifications: pure: public behavior
assignable \nothing;
ensures (* true if and only if this file exists and is a directory. *);
signals_only java.lang.SecurityException;

isFile

public boolean isFile()

Specifications: pure: public behavior
assignable \nothing;
ensures (* true if and only if this file exists and is a normal file. A normal file is not a directory and satisfies other system-dependent criteria *);
signals_only java.lang.SecurityException;

isHidden

public boolean isHidden()

Specifications: pure: public behavior
assignable \nothing;
ensures (* true if and only if this file is hidden according to the conventions of the underlying platform *);
signals_only java.lang.SecurityException;

lastModified

public long lastModified()

Specifications: pure: public behavior
assignable \nothing;
ensures \result >= 0;
ensures (* \result is a long value representing the time the file was last modified, measured in milliseconds since the epoch (00:00:00 GMT, January 1, 1970), or 0L if the file does not exist or if an I/O error occurs *);
signals_only java.lang.SecurityException;

length

public long length()

Specifications: pure: public behavior
assignable \nothing;
ensures \result >= 0;
ensures (* \result is the length, in bytes, of this file, or 0L if the file does not exist *);
signals_only java.lang.SecurityException;

createNewFile

public boolean createNewFile()
                      throws IOException

Throws:: IOException

Specifications:: public behavior
assignable fileSystem;
ensures \old(this.exists()) ==> (\result == false);
ensures (!\old(this.exists())&&this.exists()) ==> (\result == true);
signals_only java.io.IOException, java.lang.SecurityException;

delete

public boolean delete()

Specifications:: public behavior
assignable fileSystem;
ensures \result <==> (\old(this.exists())&&!this.exists());
signals_only java.lang.SecurityException;

deleteOnExit

public void deleteOnExit()

Specifications:: public behavior
assignable fileSystem;
ensures java.io.File.toDelete.has(this);
signals_only java.lang.SecurityException;

list

public String[] list()

Specifications: pure nullable: public behavior
assignable \nothing;
ensures !this.isDirectory() ==> \result == null;
ensures (* An array of strings naming the files and directories in this directory. The array will be empty if the directory is empty. *);
signals_only java.lang.SecurityException;

list

public String[] list(FilenameFilter filter)

Specifications: pure nullable: public behavior
assignable \nothing;
ensures !this.isDirectory() ==> \result == null;
ensures (* returns an array of strings naming the files and directories in this directory that were accepted by the given filter. The array will be empty if the directory is empty or if no names were accepted by the filter. *);
signals_only java.lang.SecurityException;

listFiles

public File[] listFiles()

Specifications: pure nullable: public behavior
assignable \nothing;
ensures !this.isDirectory() ==> \result == null;
ensures (* returns an array of Files denoting the files and directories in this directory. The array will be empty if the directory is empty. *);
signals_only java.lang.SecurityException;

listFiles

public File[] listFiles(FilenameFilter filter)

Specifications: nullable: public behavior
assignable \nothing;
ensures !this.isDirectory() ==> \result == null;
ensures (* Returns an array of Files denoting the files and directories in this directory. The array will be empty if the directory is empty. All filenames must satify the given filter *);
signals_only java.lang.SecurityException;

listFiles

public File[] listFiles(FileFilter filter)

Specifications: nullable: public behavior
assignable \nothing;
ensures !this.isDirectory() ==> \result == null;
ensures (* Returns an array of Files denoting the files and directories in this directory. The array will be empty if the directory is empty. All filenames must satify the given filter *);
signals_only java.lang.SecurityException;

mkdir

public boolean mkdir()

Specifications:: public behavior
assignable fileSystem;
ensures \result <==> (!\old(this.isDirectory())&&this.isDirectory());
signals_only java.lang.SecurityException;

mkdirs

public boolean mkdirs()

Specifications:: public behavior
assignable fileSystem;
ensures (\result == true) ==> (!\old(this.isDirectory())&&this.isDirectory());
ensures (* all parent directories that did not exist were created *);
signals_only java.lang.SecurityException;

renameTo

public boolean renameTo(File dest)

Specifications:: public behavior
assignable fileSystem;
ensures (* (\result == true) ==> this file was renamed *);
signals_only java.lang.SecurityException, java.lang.NullPointerException;

setLastModified

public boolean setLastModified(long time)

Specifications:: public behavior
assignable fileSystem;
ensures (\result == true) ==> this.lastModified() == time;
signals_only java.lang.IllegalArgumentException, java.lang.NullPointerException;

setReadOnly

public boolean setReadOnly()

Specifications:: public behavior
assignable fileSystem;
ensures (\result == true) ==> this.canRead();
ensures (\result == false) ==> !this.canWrite();
signals_only java.lang.SecurityException;

listRoots

public static File[] listRoots()

Specifications: pure: public normal_behavior
assignable \nothing;
ensures \result != null;
ensures (* Returns an array of File objects denoting the available filesystem roots, or null if the set of roots could not be determined. The array will be empty if there are no filesystem roots. *);

createTempFile

public static File createTempFile(String prefix,
                                  String suffix,
                                  File directory)
                           throws IOException

Throws:: IOException

Specifications:: public behavior
old java.io.File tf = new java.io.File(java.io.File.tempDir);
requires prefix != null;
assignable fileSystem;
ensures (directory == null&&suffix == null) ==> (\result .prefix.equals(tf.prefix)&&\result .names.equals(tf.names.insertBack(prefix+".tmp")));
ensures (directory == null&&suffix != null) ==> (\result .prefix.equals(tf.prefix)&&\result .names.equals(tf.names.insertBack(prefix+suffix)));
ensures (directory != null&&suffix == null) ==> (\result .prefix.equals(directory.prefix)&&\result .names.equals(directory.names.insertBack(prefix+".tmp")));
ensures (directory != null&&suffix != null) ==> (\result .prefix.equals(directory.prefix)&&\result .names.equals(directory.names.insertBack(prefix+suffix)));
signals_only java.io.IOException, java.lang.SecurityException, java.lang.IllegalArgumentException;
signals (java.lang.IllegalArgumentException) prefix.length() < 3;

createTempFile

public static File createTempFile(String prefix,
                                  String suffix)
                           throws IOException

Throws:: IOException

Specifications:: public behavior
old java.io.File tf = new java.io.File(java.io.File.tempDir);
requires prefix != null;
assignable fileSystem;
ensures (suffix == null) ==> (\result .prefix.equals(tf.prefix)&&\result .names.equals(tf.names.insertBack(prefix+".tmp")));
ensures (suffix != null) ==> (\result .prefix.equals(tf.prefix)&&\result .names.equals(tf.names.insertBack(prefix+suffix)));
signals_only java.io.IOException, java.lang.SecurityException, java.lang.IllegalArgumentException;
signals (java.lang.IllegalArgumentException) prefix.length() < 3;

compareTo

public int compareTo(non_null File pathname)

Specifications: pure: public normal_behavior
requires pathname != null;
assignable \nothing;
ensures \result == this.toString().compareTo(pathname.toString());
ensures_redundantly (\result == 0) <==> this.equals(pathname);
Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
pure: public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);
also: public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);

compareTo

public int compareTo(non_null Object o)

Specified by:: compareTo in interface Comparable

Specifications: pure
also: public normal_behavior
requires o instanceof java.io.File;
assignable \nothing;
ensures (\result == 0) <==> this.equals((java.io.File)o);
ensures (* returns a value less than zero if this abstract pathname is lexicographically less than the argument, or a value greater than zero if this abstract pathname is lexicographically greater than the argument *);
also: public exceptional_behavior
requires !(o instanceof java.io.File)&&o != null;
assignable \nothing;
signals_only java.lang.ClassCastException;
Specifications inherited from overridden method compareTo(Object o) in interface Comparable:
pure: public behavior
requires o != null;
ensures (* \result is negative if this is "less than" o *);
ensures (* \result is 0 if this is "equal to" o *);
ensures (* \result is positive if this is "greater than" o *);
signals_only java.lang.ClassCastException;
signals (java.lang.ClassCastException) (* the class of o prohibits it from being compared to this *);
also: public behavior
requires o != null&&o instanceof java.lang.Comparable;
ensures this.definedComparison((java.lang.Comparable)o,this);
ensures o == this ==> \result == 0;
ensures this.sgn(\result ) == -this.sgn(((java.lang.Comparable)o).compareTo(this));
signals (java.lang.ClassCastException) !this.definedComparison((java.lang.Comparable)o,this);

equals

public boolean equals(nullable Object obj)

Overrides:: equals in class Object

Specifications: pure
also: public normal_behavior
requires obj instanceof java.io.File;
ensures \result == (((java.io.File)obj).names.equals(this.names)&&org.jmlspecs.models.JMLNullSafe.equals(((java.io.File)obj).prefix,this.prefix));
also: public normal_behavior
requires !(obj instanceof java.io.File);
ensures \result == false;
Specifications inherited from overridden method equals(Object obj) in class Object:
pure: public normal_behavior
requires obj != null;
ensures (* \result is true when obj is "equal to" this object *);
also: public normal_behavior
requires this == obj;
ensures \result ;
also: public code normal_behavior
requires obj != null;
ensures \result <==> this == obj;
also: diverges false;
ensures obj == null ==> !\result ;

hashCode

public int hashCode()

Overrides:: hashCode in class Object

Specifications inherited from overridden method in class Object:: public behavior
assignable objectState;
ensures (* \result is a hash code for this object *);
also: public code normal_behavior
assignable \nothing;

toString

public String toString()

Overrides:: toString in class Object

Specifications: pure
also: public normal_behavior
requires this.prefix == null;
assignable \nothing;
ensures \result .equals(this.concatenate(this.names));
also: public normal_behavior
requires this.prefix != null;
assignable \nothing;
ensures \result .equals(this.prefix+this.concatenate(this.names));
Specifications inherited from overridden method in class Object:
non_null: public normal_behavior
assignable objectState;
ensures \result != null&&\result .equals(this.theString);
ensures (* \result is a string representation of this object *);
also: public code normal_behavior
assignable \nothing;
ensures \result != null&&(* \result is the instance's class name, followed by an @, followed by the instance's hashcode in hex *);
also: public code model_program { ... }
implies_that: assignable objectState;
ensures \result != null;

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.

Model Field Summary
`static JMLDataGroup`	`fileSystem`
`JMLObjectSequence`	`names`
`String`	`prefix`
`static JMLObjectSet`	`toDelete`

Field Summary
`static String`	`pathSeparator`
`static char`	`pathSeparatorChar`
`static String`	`separator`
`static char`	`separatorChar`

Constructor Summary
`File(File parent, String child)`
`File(String pathname)`
`File(String parent, String child)`
`File(URI uri)`

Model Method Summary
`String`	`concatenate(JMLObjectSequence strs)`
`JMLObjectSequence`	`extractNames(String pathname)`
`String`	`extractPrefix(String pathname)`

Method Summary
`boolean`	`canRead()`
`boolean`	`canWrite()`
`int`	`compareTo(non_null File pathname)`
`int`	`compareTo(non_null Object o)`
`boolean`	`createNewFile()`
`static File`	`createTempFile(String prefix, String suffix)`
`static File`	`createTempFile(String prefix, String suffix, File directory)`
`boolean`	`delete()`
`void`	`deleteOnExit()`
`boolean`	`equals(nullable Object obj)`
`boolean`	`exists()`
`File`	`getAbsoluteFile()`
`String`	`getAbsolutePath()`
`File`	`getCanonicalFile()`
`String`	`getCanonicalPath()`
`String`	`getName()`
`String`	`getParent()`
`File`	`getParentFile()`
`String`	`getPath()`
`int`	`hashCode()`
`boolean`	`isAbsolute()`
`boolean`	`isDirectory()`
`boolean`	`isFile()`
`boolean`	`isHidden()`
`long`	`lastModified()`
`long`	`length()`
`String[]`	`list()`
`String[]`	`list(FilenameFilter filter)`
`File[]`	`listFiles()`
`File[]`	`listFiles(FileFilter filter)`
`File[]`	`listFiles(FilenameFilter filter)`
`static File[]`	`listRoots()`
`boolean`	`mkdir()`
`boolean`	`mkdirs()`
`boolean`	`renameTo(File dest)`
`boolean`	`setLastModified(long time)`
`boolean`	`setReadOnly()`
`String`	`toString()`
`URI`	`toURI()`
`URL`	`toURL()`

java.io Class File

prefix

names

fileSystem

toDelete

tempDir

separator

pathSeparator

separatorChar

pathSeparatorChar

File

File

File

File

extractPrefix

extractNames

concatenate

getName

getParent

getParentFile

getPath

isAbsolute

getAbsolutePath

getAbsoluteFile

getCanonicalPath

getCanonicalFile

toURL

toURI

canRead

canWrite

exists

isDirectory

isFile

isHidden

lastModified

length

createNewFile

delete

deleteOnExit

list

list

listFiles

listFiles

listFiles

mkdir

mkdirs

renameTo

setLastModified

setReadOnly

listRoots

createTempFile

createTempFile

compareTo

compareTo

equals

hashCode

toString

java.io
Class File