org.jmlspecs.ant.tasks
Class FileSetWrapper

java.lang.Object
  org.jmlspecs.ant.tasks.FileSetWrapper

public class FileSetWrapper

extends Object

The inner class Visitor is provided to conveniently perform a certain action on all element in a FileSet. It is typically used as follows in a task:

 fileset.new Visitor() {
   public void visit(File file) {
     //action code
   }
 }.visit(project);

Version:

$Revision: 1.3 $

Author:

Marko van Dooren

Class Specifications

Specifications inherited from class Object

represents objectState <- org.jmlspecs.lang.JMLDataGroup.IT; public represents _getClass <- \typeof(this);

Nested Class Summary
class	FileSetWrapper.Visitor

 

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  org.apache.tools.ant.types.FileSet	_fileset

 

Constructor Summary

FileSetWrapper(org.apache.tools.ant.types.FileSet fileset)

 

Model Method Summary

 

Model methods inherited from class java.lang.Object

hashValue

 

Method Summary
org.apache.tools.ant.types.FileSet	getFileSet()

 

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Field Detail

_fileset

private org.apache.tools.ant.types.FileSet _fileset

Specifications: non_null

FileSetWrapper

public FileSetWrapper(org.apache.tools.ant.types.FileSet fileset)

Specifications:

public normal_behavior
requires fileset != null;
assignable \not_specified;
ensures this.getFileSet() == fileset;

getFileSet

public org.apache.tools.ant.types.FileSet getFileSet()

Specifications: pure non_null

public behavior
ensures \result != null;