org.jutil.java.io
Class File

java.lang.Object
  |
  +--java.io.File
        |
        +--org.jutil.java.io.File

All Implemented Interfaces:

java.lang.Comparable, java.io.Serializable

public class File

extends java.io.File

A class that acts as an extension of java.io.File.

Version:

$Revision: 1.2 $

Author:

Tom Schrijvers, Marko van Dooren

See Also:

Serialized Form

Fields inherited from class java.io.File

pathSeparator, pathSeparatorChar, separator, separatorChar

Constructor Summary

File(java.io.File parent, java.lang.String child)
Initialize a new File using the given parent and child.

File(java.lang.String pathname)
Initialize a new File See java.io.File.File(File, String).

File(java.lang.String parent, java.lang.String child)
Initialize a new File See java.io.File.File(File, String).

Method Summary

static void

copy(File source, File destination) public behavior pre source != null; pre destination != null; // both files must be different pre ! source.getCanonicalPath().equals(destination.getCanonicalPath()); post (* The source file is copied to the destination file *); signals (FileNotFoundException) (* The source file does not exist, is a directory or not readable *); signals (FileNotFoundException) (* The destination file does not exist and can not be create, is a directory or exists, but is not writable *); signals (SecurityException) (* The source file may not be read from *); signals (SecurityException) (* The destination file may not be writen to *); signals (IOException) (* An IO errors occurs *); Copies the given source file to the given destination file.

void

copyTo(File destination) public behavior pre destination != null; // both files must be different pre ! getCanonicalPath().equals(destination.getCanonicalPath()); post (* This file is copied to the destination file *); signals (FileNotFoundException) (* This file does not exist, is a directory or not readable *); signals (FileNotFoundException) (* The destination file does not exist and can not be create, is a directory or exists, but is not writable *); signals (SecurityException) (* This file may not be read from *); signals (SecurityException) (* The destination file may not be writen to *); signals (IOException) (* An IO errors occurs *); Copies this file to the given destination file.

Methods inherited from class java.io.File

canRead, canWrite, compareTo, compareTo, createNewFile, createTempFile, createTempFile, delete, deleteOnExit, equals, exists, getAbsoluteFile, getAbsolutePath, getCanonicalFile, getCanonicalPath, getName, getParent, getParentFile, getPath, hashCode, isAbsolute, isDirectory, isFile, isHidden, lastModified, length, list, list, listFiles, listFiles, listFiles, listRoots, mkdir, mkdirs, renameTo, setLastModified, setReadOnly, toString, toURL

Methods inherited from class java.lang.Object

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

Constructor Detail

File

public File(java.io.File parent,
            java.lang.String child)

Initialize a new File using the given parent and child. See java.io.File.File(File, String).

File

public File(java.lang.String pathname)

Initialize a new File See java.io.File.File(File, String).

File

public File(java.lang.String parent,
            java.lang.String child)

Initialize a new File See java.io.File.File(File, String).

Method Detail

copy

public static void copy(File source,
                        File destination)
                 throws java.io.FileNotFoundException,
                        java.lang.SecurityException,
                        java.io.IOException

public behavior

pre source != null;
pre destination != null;
// both files must be different
pre ! source.getCanonicalPath().equals(destination.getCanonicalPath());

post (* The source file is copied to the destination file *);

signals (FileNotFoundException) (* The source file does not exist, is a directory
or not readable *);
signals (FileNotFoundException) (* The destination file does not exist and can not
be create, is a directory or exists, but is not
writable *);
signals (SecurityException) (* The source file may not be read from *);
signals (SecurityException) (* The destination file may not be writen to *);
signals (IOException) (* An IO errors occurs *);
Copies the given source file to the given destination file. If an exception occurs, the possibly incomplete destination file is not deleted.

Parameters:

source - The source file

destination - The destination file

copyTo

public void copyTo(File destination)
            throws java.io.FileNotFoundException,
                   java.lang.SecurityException,
                   java.io.IOException

public behavior

pre destination != null;
// both files must be different
pre ! getCanonicalPath().equals(destination.getCanonicalPath());

post (* This file is copied to the destination file *);

signals (FileNotFoundException) (* This file does not exist, is a directory
or not readable *);
signals (FileNotFoundException) (* The destination file does not exist and can not
be create, is a directory or exists, but is not
writable *);
signals (SecurityException) (* This file may not be read from *);
signals (SecurityException) (* The destination file may not be writen to *);
signals (IOException) (* An IO errors occurs *);
Copies this file to the given destination file. If an exception occurs, the possibly incomplete destination file is not deleted.

Parameters:

destination - The destination file