// @(#)$Id: File.refines-java,v 1.10 2007/02/08 14:05:50 leavens Exp $ // Copyright (C) 2005 Iowa State University // // This file is part of the runtime library of the Java Modeling Language. // // This library is free software; you can redistribute it and/or // modify it under the terms of the GNU Lesser General Public License // as published by the Free Software Foundation; either version 2.1, // of the License, or (at your option) any later version. // // This library is distributed in the hope that it will be useful, // but WITHOUT ANY WARRANTY; without even the implied warranty of // MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU // Lesser General Public License for more details. // // You should have received a copy of the GNU Lesser General Public License // along with JML; see the file LesserGPL.txt. If not, write to the Free // Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA // 02110-1301 USA. package java.io; import java.net.URI; import java.net.URL; import java.net.MalformedURLException; import java.net.URISyntaxException; //@ model import org.jmlspecs.models.*; /** JML's specification of java.io.File. * @author Katie Becker * @author Elizabeth Seagren * @author Gary T. Leavens */ public class File implements java.io.Serializable, Comparable { // CLASS SPECIFICATIONS /*@ public model String prefix; @ public model JMLObjectSequence names; @*/ //@ public invariant (prefix==null) ==> !names.isEmpty(); // METHODS AND CONSTRUCTORS /*@ public normal_behavior @ requires pathname != null; @ assignable prefix, names; @ ensures prefix.equals(extractPrefix(pathname)); @ ensures names.equals(extractNames(pathname)); @ also @ public exceptional_behavior @ requires pathname == null; @ assignable \nothing; @ signals_only NullPointerException; @*/ public /*@ pure @*/ File(String pathname); /*@ public normal_behavior @ requires pathname != null; @ ensures \result != null && pathname.startsWith(\result); public pure model String extractPrefix(String pathname) { String ret = ""; if(separatorChar=='/' && pathname.startsWith("/")) { ret = "/"; } else if(separatorChar == '\\') { if(pathname.startsWith("\\")) { ret = "\\"; } else if(pathname.charAt(1) == ':') { if(pathname.charAt(2)=='\\') ret = pathname.substring(0,2); } else ret = pathname.substring(0,1); } else { throw new InternalError("Missing Case in extractPrefix."); } return ret; } @*/ /*@ public normal_behavior @ requires pathname != null && !pathname.endsWith(separator); @ ensures \result != null; @ ensures (prefix + concatenate(\result)).equals(pathname); @ also @ public normal_behavior @ requires pathname != null && pathname.endsWith(separator); @ ensures \result != null; @ ensures (prefix + concatenate(\result)) @ .equals(pathname.substring(0,pathname.length()-2)); public pure model JMLObjectSequence extractNames(String pathname) { String names = pathname.substring(extractPrefix(pathname).length()); String word = ""; JMLObjectSequence ret = new JMLObjectSequence(); //@ maintaining (prefix + concatenate(ret) + names).equals(pathname); while(!names.equals("")) { while(names != "" && names.charAt(0) != separatorChar) { word += names.charAt(0); names = names.substring(1); } //@ assert names.equals("") || names.charAt(0) == separatorChar; if(!word.equals("")) { ret.insertBack(word); } word = ""; //@ decreasing names.length(); while(!names.equals("") && names.charAt(0)==separatorChar) { names=names.substring(1); } //@ assert names.equals("") || names.charAt(0) != separatorChar; //@ hence_by (* logic *); //@ assert !names.equals("") ==> names.charAt(0) != separatorChar; } //@ assert names.equals("") && (prefix + concatenate(ret)).equals(pathname); return ret; } @*/ /*@ requires strs != null @ && (\forall int i; 0 <= i && i < strs.int_size(); @ strs.get(i) instanceof String); public pure model String concatenate(JMLObjectSequence strs) { String ret = ""; JMLIterator iter = strs.iterator(); ret += iter.next(); while(iter.hasNext()) { ret += separator + iter.next(); } return ret; } @*/ /*@ public normal_behavior @ requires parent == null && child != null; @ assignable prefix, names; @ ensures prefix.equals(extractPrefix(child)); @ ensures names.equals(extractNames(child)); @ also @ public normal_behavior @ requires parent != null && child != null; @ assignable prefix, names; @ ensures prefix.equals(extractPrefix(parent)); @ ensures names.equals(extractNames(parent + child)); @ // !FIXME! incomplete @ also @ public exceptional_behavior @ requires child == null; @ assignable \nothing; @ signals_only NullPointerException; @*/ public /*@ pure @*/ File(String parent, String child); /*@ public normal_behavior @ requires parent == null && child != null; @ assignable prefix, names; @ ensures prefix.equals(extractPrefix(child)); @ ensures names.equals(extractNames(child)); @ also @ public normal_behavior @ requires parent != null && child != null; @ assignable prefix, names; @ ensures prefix.equals(parent.prefix); @ ensures names.equals(parent.names.concat(extractNames(child))); @ also @ public exceptional_behavior @ requires child == null; @ assignable \nothing; @ signals_only NullPointerException; @*/ public /*@ pure @*/ File(File parent, String child); /*@ 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 IllegalArgumentException; @ also @ public exceptional_behavior @ requires uri == null; @ assignable \nothing; @ signals_only NullPointerException; @*/ public /*@ pure @*/ File(URI uri); /*@ public normal_behavior @ requires names.isEmpty(); @ assignable \nothing; @ ensures \result.equals(""); @ also @ public normal_behavior @ requires !names.isEmpty(); @ assignable \nothing; @ ensures \result != null && \result.equals(names.last()); @*/ public /*@ pure @*/ String getName(); /*@ public normal_behavior @ requires names.isEmpty(); @ assignable \nothing; @ ensures \result == null; @ also @ public normal_behavior @ requires prefix == null; @ assignable \nothing; @ ensures \result.equals(concatenate(names.header())); @ also @ public normal_behavior @ requires prefix != null && !names.isEmpty(); @ assignable \nothing; @ ensures \result != null @ && \result.equals(prefix + concatenate(names.header())); @*/ public /*@ pure @*/ String getParent(); /*@ public normal_behavior @ requires names.isEmpty(); @ assignable \nothing; @ ensures \result == null; @ also @ public normal_behavior @ requires prefix == null; @ assignable \nothing; @ ensures \result.prefix.equals(null); @ also @ public normal_behavior @ requires prefix != null; @ assignable \nothing; @ ensures \result != null @ && \result.names.equals(names.header()) @ && \result.prefix.equals(prefix); @*/ public /*@ pure @*/ File getParentFile(); /*@ public normal_behavior @ requires prefix == null; @ assignable \nothing; @ ensures \result.equals(concatenate(names)); @ also @ public normal_behavior @ requires prefix != null; @ assignable \nothing; @ ensures \result.equals(prefix + concatenate(names)); @*/ public /*@ pure @*/ String getPath(); /*@ public normal_behavior @ assignable \nothing; @ ensures \result <==> (prefix!=null) && prefix.endsWith(separator); @*/ public /*@ pure @*/ boolean isAbsolute(); /*@ public normal_behavior @ requires prefix == null; @ assignable \nothing; @ ensures \result.equals(System.getProperty("usr.dir") + concatenate(names)); @ also @ public normal_behavior @ requires prefix != null && !names.isEmpty(); @ assignable \nothing; @ ensures \result.equals(prefix + concatenate(names)); @*/ public /*@ pure @*/ String getAbsolutePath(); /*@ public normal_behavior @ requires prefix == null; @ assignable \nothing; @ ensures \result.prefix.equals(extractPrefix(System.getProperty("usr.dir"))); @ ensures \result.names.equals(extractNames(System.getProperty("usr.dir")).concat(names)); @ also @ public normal_behavior @ requires prefix != null && !names.isEmpty(); @ assignable \nothing; @ ensures \result.prefix.equals(prefix) && @ \result.names.equals(names); @*/ public /*@ pure @*/ File getAbsoluteFile(); /*@ 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 IOException; @*/ public String getCanonicalPath() throws IOException; /*@ 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 IOException; @*/ public File getCanonicalFile() throws IOException; /*@ public behavior @ assignable \nothing; @ ensures \result != null; @ ensures (* \result is this abstract pathname converted into file:URL *); @ signals_only MalformedURLException; @*/ public URL toURL() throws MalformedURLException; /*@ 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 *); @*/ public URI toURI(); /*@ public behavior @ assignable \nothing; @ ensures (* true if and only if this file has read access. *); @ signals_only SecurityException; @*/ public /*@ pure @*/ boolean canRead(); /*@ public behavior @ assignable \nothing; @ ensures (* true if and only if this file has write access. *); @ signals_only SecurityException; @*/ public /*@ pure @*/ boolean canWrite(); /*@ public behavior @ assignable \nothing; @ ensures (* true if and only if this file exists. *); @ signals_only SecurityException; @*/ public /*@ pure @*/ boolean exists(); /*@ public behavior @ assignable \nothing; @ ensures (* true if and only if this file exists and is a directory. *); @ signals_only SecurityException; @*/ public /*@ pure @*/ boolean isDirectory(); /*@ 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 SecurityException; @*/ public /*@ pure @*/ boolean isFile(); /*@ public behavior @ assignable \nothing; @ ensures (* true if and only if this file is hidden according to the @ conventions of the underlying platform *); @ signals_only SecurityException; @*/ public /*@ pure @*/ boolean isHidden(); /*@ 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 SecurityException; @*/ public /*@ pure @*/ long lastModified(); /*@ 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 SecurityException; @*/ public /*@ pure @*/ long length(); //@ public static model JMLDataGroup fileSystem; /*@ public behavior @ assignable fileSystem; @ ensures \old(this.exists()) ==> (\result == false); @ ensures (!\old(this.exists()) && this.exists()) ==> (\result == true); @ signals_only IOException, SecurityException; @*/ public boolean createNewFile() throws IOException; /*@ public behavior @ assignable fileSystem; @ ensures \result <==> (\old(this.exists()) && !this.exists()); @ signals_only SecurityException; @*/ public boolean delete(); //@ public static model JMLObjectSet toDelete; /*@ public invariant @ (\forall Object o; toDelete.has(o); o instanceof File); @*/ /*@ public behavior @ assignable fileSystem; @ ensures toDelete.has(this); @ signals_only SecurityException; @*/ public void deleteOnExit(); /*@ 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 SecurityException; @*/ public /*@ pure nullable @*/ String[] list(); /*@ 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 SecurityException; @*/ public /*@ pure nullable @*/ String[] list(FilenameFilter filter); /*@ 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 SecurityException; @*/ public /*@ pure nullable */ File[] listFiles(); /*@ 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 SecurityException; @*/ public /*@ nullable */ File[] listFiles(FilenameFilter filter); /*@ 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 SecurityException; @*/ public /*@ nullable */ File[] listFiles(FileFilter filter); /*@ public behavior @ assignable fileSystem; @ ensures \result <==> (!\old(this.isDirectory()) && this.isDirectory()); @ signals_only SecurityException; @*/ public boolean mkdir(); /*@ public behavior @ assignable fileSystem; @ ensures (\result==true) ==> (!\old(this.isDirectory()) && this.isDirectory()); @ ensures (* all parent directories that did not exist were created *); @ signals_only SecurityException; @*/ public boolean mkdirs(); /*@ public behavior @ assignable fileSystem; @ ensures (* (\result == true) ==> this file was renamed *); @ signals_only SecurityException, NullPointerException; @*/ public boolean renameTo(File dest); /*@ public behavior @ assignable fileSystem; @ ensures (\result == true) ==> this.lastModified()==time; @ signals_only IllegalArgumentException, NullPointerException; @*/ public boolean setLastModified(long time); /*@ public behavior @ assignable fileSystem; @ ensures (\result == true) ==> this.canRead(); @ ensures (\result == false) ==> !this.canWrite(); @ signals_only SecurityException; @*/ public boolean setReadOnly(); /*@ 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. *); @*/ public /*@ pure @*/ static File[] listRoots(); /*@ public behavior @ old File tf = new 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 IOException, SecurityException, @ IllegalArgumentException; @ signals (IllegalArgumentException) prefix.length() < 3; @*/ public static File createTempFile(String prefix, String suffix, File directory) throws IOException; /*@ public behavior @ old File tf = new 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 IOException, SecurityException, IllegalArgumentException; @ signals (IllegalArgumentException) prefix.length() < 3; @*/ public static File createTempFile(String prefix, String suffix) throws IOException; /*@ public normal_behavior @ requires pathname!=null; @ assignable \nothing; @ ensures \result == this.toString().compareTo(pathname.toString()); @ ensures_redundantly (\result == 0) <==> this.equals(pathname); @*/ public /*@ pure @*/ int compareTo(/*@ non_null @*/ File pathname); /*@ also @ public normal_behavior @ requires o instanceof File; @ assignable \nothing; @ ensures (\result == 0) <==> this.equals((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 File) && o != null; @ assignable \nothing; @ signals_only ClassCastException; @*/ public /*@ pure @*/ int compareTo(/*@ non_null @*/ Object o); /*@ also @ public normal_behavior @ requires obj instanceof File; @ ensures \result == (((File)obj).names.equals(names) && @ JMLNullSafe.equals(((File)obj).prefix, prefix)); @ also @ public normal_behavior @ requires !(obj instanceof File); @ ensures \result == false; @*/ public /*@ pure @*/ boolean equals(/*@ nullable @*/ Object obj); public int hashCode(); /*@ also @ public normal_behavior @ requires prefix == null; @ assignable \nothing; @ ensures \result.equals(concatenate(names)); @ also @ public normal_behavior @ requires prefix != null; @ assignable \nothing; @ ensures \result.equals(prefix + concatenate(names)); @*/ public /*@ pure @*/ String toString(); // FIELDS //@ ghost public static final String tempDir; /*@ initially separator.equals(System.getProperty("java.io.tmpdir")); @*/ public static final String separator; /*@ initially separator.equals(System.getProperty("file.separator")); @*/ public static final String pathSeparator; /*@ initially pathSeparator.equals(System.getProperty("path.separator")); @*/ public static final char separatorChar; /*@ initially separatorChar == separator.charAt(0); @*/ public static final char pathSeparatorChar; /*@ initially pathSeparatorChar == pathSeparator.charAt(0); @*/ }