org.jmlspecs.ant.tasks
Class CompileTask

java.lang.Object
  org.apache.tools.ant.ProjectComponent
      org.apache.tools.ant.Task
          org.jmlspecs.ant.tasks.AbstractFileSetTask
              org.jmlspecs.ant.tasks.CommonOptionsTask
                  org.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

CompileTask

public CompileTask()

Specifications:

ensures this.getVerbose() == false;

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