org.jmlspecs.checker
Class Main.Filter

java.lang.Object
  org.jmlspecs.checker.Main.Filter

All Implemented Interfaces:

FilenameFilter

Enclosing class:

Main

static class Main.Filter

extends Object

implements FilenameFilter

This class is used with the Directory.list method to list those files in a directory that this program is interested in processing - in this case, all those that end in '.java', '.jml' or '.spec'.

Field Summary
private static String[]	suffixes

 

Constructor Summary

Main.Filter()

 

Method Summary
boolean	accept(File dir, String name)

 

Methods inherited from class java.lang.Object

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

 

Field Detail

suffixes

private static String[] suffixes

Main.Filter

public Main.Filter()

accept

public boolean accept(File dir,
                      String name)

Specified by:

accept in interface FilenameFilter