org.jutil.java.io
Class ExtendedFile

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

All Implemented Interfaces:

java.lang.Comparable, java.io.Serializable

Direct Known Subclasses:

File

public class ExtendedFile

extends java.io.File

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

Fields inherited from class java.io.File

pathSeparator, pathSeparatorChar, separator, separatorChar

 

Constructor Summary

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

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

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

 

Method Summary
static void	copy(java.io.File source, java.io.File destination)           Copies the given source file to the given destination file.
void	copyTo(java.io.File destination)           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, getPrefixLength, 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

ExtendedFile

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

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

ExtendedFile

public ExtendedFile(java.lang.String pathname)

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

ExtendedFile

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

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

copy

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

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

Specifications:

public behavior
requires source != null;
requires destination != null;
requires !source.getCanonicalPath().equals(destination.getCanonicalPath());
ensures (* 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 *);

copyTo

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

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

Specifications:

public behavior
requires destination != null;
requires !getCanonicalPath().equals(destination.getCanonicalPath());
ensures (* 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 *);