org.jmlspecs.ant.tasks
Class CheckTask

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.CheckTask

public class CheckTask

extends CommonOptionsTask

An Ant task to run the JML checker.

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

 

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

CheckTask()

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
void	execute()           Check all the files in the filesets.

 

Methods inherited from class org.jmlspecs.ant.tasks.CommonOptionsTask

getArguments, getClasspath, getDestination, getFilesAndDirectories, getRecursive, getSourcepath, getToolSpecificOptions, 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

 

Constructor Detail

CheckTask

public CheckTask()

Specifications:

public normal_behavior
assignable \not_specified;
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