JML

org.jmlspecs.launcher
Class JmlLauncher

java.lang.Object
  extended byorg.multijava.launcher.Launcher
      extended byorg.jmlspecs.launcher.JmlLauncher

public class JmlLauncher
extends Launcher

A launcher for the JML tools

Version:
$Revision: 1.8 $
Author:
Kristina Boysen

Nested Class Summary
 
Nested classes inherited from class org.multijava.launcher.Launcher
Launcher.ToolIterator, Launcher.ToolIteratorPair
 
Field Summary
private  String[] args
          The arguments to be used by these tools
private  Launcher.ToolIterator iterator
          The iterator that cycles through all of the tool names and launchers for the JML tools
private  String LOGO_NAME
          The path to the logo
 
Fields inherited from class org.multijava.launcher.Launcher
impLauncher
 
Constructor Summary
JmlLauncher(String name, String[] args)
          Constructor for the JmlLauncher
 
Method Summary
private  Launcher.ToolIterator createToolIterator()
          Builds the iterator that contains the tool description and the AbstractLaunchTool that can access the tool
protected  Launcher.ToolIterator getTools()
          Returns the iterator that contains the tool description and the AbstractLaunchTool that can access the tool
static void main(String[] args)
          Main method for running the JmlLauncher
 
Methods inherited from class org.multijava.launcher.Launcher
getImpLauncher
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

args

private String[] args
The arguments to be used by these tools


iterator

private Launcher.ToolIterator iterator
The iterator that cycles through all of the tool names and launchers for the JML tools


LOGO_NAME

private String LOGO_NAME
The path to the logo

Constructor Detail

JmlLauncher

public JmlLauncher(String name,
                   String[] args)
Constructor for the JmlLauncher

Method Detail

main

public static void main(String[] args)
Main method for running the JmlLauncher


getTools

protected Launcher.ToolIterator getTools()
Returns the iterator that contains the tool description and the AbstractLaunchTool that can access the tool


createToolIterator

private Launcher.ToolIterator createToolIterator()
Builds the iterator that contains the tool description and the AbstractLaunchTool that can access the tool


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.