JML

org.jmlspecs.ant.tasks
Class CompileTask

java.lang.Object
  extended byorg.apache.tools.ant.ProjectComponent
      extended byorg.apache.tools.ant.Task
          extended byorg.jmlspecs.ant.tasks.AbstractFileSetTask
              extended byorg.jmlspecs.ant.tasks.CommonOptionsTask
                  extended byorg.jmlspecs.ant.tasks.CompileTask

public class CompileTask
extends CommonOptionsTask

An Ant task to run the JML runtime assertion checking compiler.

Version:
$Revision: 1.2 $
Author:
Marko van Dooren

Class Specifications

Specifications inherited from class AbstractFileSetTask
private invariant !this._filesets.contains(null);
private invariant ( \forall java.lang.Object o; this._filesets.contains(o); o instanceof org.apache.tools.ant.types.FileSet);

Specifications inherited from class Object
represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT;
public represents _getClass <- \typeof(this);

Nested Class Summary
 
Nested classes inherited from class org.jmlspecs.ant.tasks.AbstractFileSetTask
AbstractFileSetTask.FileSetVisitor
 
Model Field Summary
 
Model fields inherited from class java.lang.Object
_getClass, objectState, theString
 
Ghost Field Summary
 
Ghost fields inherited from class java.lang.Object
objectTimesFinalized, owner
 
Field Summary
private  boolean _source
           
 
Fields inherited from class org.jmlspecs.ant.tasks.CommonOptionsTask
 
Fields inherited from class org.jmlspecs.ant.tasks.AbstractFileSetTask
 
Fields inherited from class org.apache.tools.ant.Task
description, location, target, taskName, taskType, wrapper
 
Fields inherited from class org.apache.tools.ant.ProjectComponent
project
 
Constructor Summary
CompileTask()
           
 
Model Method Summary
 
Model methods inherited from class java.lang.Object
hashValue
 
Method Summary
 void execute()
          Check all the files in the filesets.
 boolean getSource()
          Check whether or not this task will generate source instead of class files.
 List getToolSpecificOptions()
          Return a list of the tool-specific options for running a JML tool.
 void setSource(boolean source)
          Set the source generation property of this CompileTask.
 
Methods inherited from class org.jmlspecs.ant.tasks.CommonOptionsTask
getArguments, getClasspath, getDestination, getFilesAndDirectories, getRecursive, getSourcepath, getVerbose, setClasspath, setDestination, setRecursive, setSourcepath, setVerbose
 
Methods inherited from class org.jmlspecs.ant.tasks.AbstractFileSetTask
addFileset, getFileSets
 
Methods inherited from class org.apache.tools.ant.Task
getDescription, getLocation, getOwningTarget, getRuntimeConfigurableWrapper, getTaskName, getTaskType, getWrapper, handleErrorFlush, handleErrorOutput, handleFlush, handleInput, handleOutput, init, isInvalid, log, log, maybeConfigure, perform, reconfigure, setDescription, setLocation, setOwningTarget, setRuntimeConfigurableWrapper, setTaskName, setTaskType
 
Methods inherited from class org.apache.tools.ant.ProjectComponent
getProject, setProject
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

_source

private boolean _source
Constructor Detail

CompileTask

public CompileTask()
Specifications:
ensures this.getVerbose() == false;
Method Detail

execute

public void execute()
             throws org.apache.tools.ant.BuildException
Check all the files in the filesets.

Overrides:
execute in class org.apache.tools.ant.Task
Throws:
org.apache.tools.ant.BuildException

getToolSpecificOptions

public List getToolSpecificOptions()
Return a list of the tool-specific options for running a JML tool.

Overrides:
getToolSpecificOptions in class CommonOptionsTask
Specifications: pure non_null
Specifications inherited from overridden method in class CommonOptionsTask:
       pure non_null

setSource

public void setSource(boolean source)
Set the source generation property of this CompileTask.

Parameters:
source - True if source should be generated, false otherwise.
Specifications:
public normal_behavior
assignable \not_specified;
ensures this.getSource() == source;

getSource

public boolean getSource()
Check whether or not this task will generate source instead of class files.

Specifications: pure

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.