plugins

Class TranslatePlugin

java.lang.Object

com.fujitsu.vdmj.commands.CommandPlugin

plugins.TranslatePlugin

public class TranslatePlugin
extends CommandPlugin

All command line plugins must extend CommandPlugin and be in the class "plugins" by default. The packages searched for plugins can be changed using the "vdmj.plugins" JVM property.

Field Summary

Fields inherited from class com.fujitsu.vdmj.commands.CommandPlugin

interpreter

Constructor Summary

Constructors

Constructor and Description
TranslatePlugin(Interpreter interpreter) The constructor is called from the command line interpreter when the user first types "translate ".

Method Summary

Modifier and Type	Method and Description
String	help() Once this plugin is loaded (but not before) the following help line is added to the general "help" output in the command line.
boolean	run(String[] argv) The run method is called whenever the user types "translate " in the VDMJ command line interpreter (CommandReader.java).

Methods inherited from class java.lang.Object

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

Constructor Detail

TranslatePlugin

public TranslatePlugin(Interpreter interpreter)

The constructor is called from the command line interpreter when the user first types "translate ". It is passed an instance of the runtime interpreter, which is saved in a protected field by the superclass.

Parameters:

interpreter -

Method Detail

run

public boolean run(String[] argv)

The run method is called whenever the user types "translate " in the VDMJ command line interpreter (CommandReader.java). Note that this class has access to the "interpreter" instance that is running, which is passed during construction (above). The example run method uses the ClassMapper to turn the type checked tree (from the interpreter) into a "TR" tree. This uses the mappings file defined in the TRNode root class, which all translatable classes must extend. After converting the TC tree to a TR tree, this is then used to translate the specification into "C". The result, a String, is just printed to stdout, which appears in the user console session. By returning "true", the method indicates that the command was processed, even if it failed. If it returns "false", the command line interpreter will say "Unknown command".

Specified by:

run in class CommandPlugin

help

public String help()

Once this plugin is loaded (but not before) the following help line is added to the general "help" output in the command line. The format is the same as the other help lines, with an indication of what arguments the command takes, and a one line description.

Specified by:

help in class CommandPlugin