JML

org.multijava.util
Class Destination

java.lang.Object
  extended byjava.io.File
      extended byorg.multijava.util.Destination
All Implemented Interfaces:
Comparable, Serializable

public class Destination
extends File

This class represents the destination of the output of one of the tools included in the project. If a destination is specified on the command line and the input belongs to a package then the output should be written to the concatenation of the destination directory and the package names. If no destination is specified then the output should be written to the same directory as the input. The destination parameter from the command line is used to construct an instance of this. That instance provides File objects (via the ...target() methods) for writing particular output files.


Field Summary
private  boolean unspecified
          Indicates whether the destination directory was unspecified on the command line.
 
Fields inherited from class java.io.File
pathSeparator, pathSeparatorChar, separator, separatorChar
 
Constructor Summary
private Destination(String destination, boolean unspecified)
           
 
Method Summary
static Destination check(String dest)
          Establish a new destination based on the command line argument.
 File classFileTargetDirectory(String packageName, File sourceFile)
          Returns the target directory for writing a class file of the given package and source file.
 File textTarget(String filename)
          Returns the target for a text file, which is simply filename appended to the destination directory.
 
Methods inherited from class java.io.File
canExecute, canRead, canWrite, compareTo, compareTo, createNewFile, createTempFile, createTempFile, delete, deleteOnExit, equals, exists, getAbsoluteFile, getAbsolutePath, getCanonicalFile, getCanonicalPath, getFreeSpace, getName, getParent, getParentFile, getPath, getTotalSpace, getUsableSpace, hashCode, isAbsolute, isDirectory, isFile, isHidden, lastModified, length, list, list, listFiles, listFiles, listFiles, listRoots, mkdir, mkdirs, renameTo, setExecutable, setExecutable, setLastModified, setReadable, setReadable, setReadOnly, setWritable, setWritable, toString, toURI, toURL
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
 

Field Detail

unspecified

private boolean unspecified
Indicates whether the destination directory was unspecified on the command line.

Constructor Detail

Destination

private Destination(String destination,
                    boolean unspecified)
Method Detail

check

public static Destination check(String dest)
Establish a new destination based on the command line argument. If the argument is null then the destination is unspecified and will be the current working directory.


textTarget

public File textTarget(String filename)
Returns the target for a text file, which is simply filename appended to the destination directory.


classFileTargetDirectory

public File classFileTargetDirectory(String packageName,
                                     File sourceFile)
Returns the target directory for writing a class file of the given package and source file.

 ensures unspecified && sourceFile != null ==> \result == sourceFile;
 ensures unspecified && sourceFile == null ==> \result == this;
 ensures !unspecified ==> \result.equals( new File( this, packageName ));
 


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.