JML

java.io
Class File

java.lang.Object
  extended byjava.io.File
All Implemented Interfaces:
Comparable, Serializable
Direct Known Subclasses:
Destination

public class File
extends Object
implements Serializable, Comparable

JML's specification of java.io.File.

Author:
Katie Becker, Elizabeth Seagren, Gary T. Leavens

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;

JML

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.