Package commands

Class TranslateCommand

java.lang.Object
com.fujitsu.vdmj.plugins.AnalysisCommand
commands.TranslateCommand
public class TranslateCommand extends com.fujitsu.vdmj.plugins.AnalysisCommand
All command line plugins must extend AnalysisCommand and be in the class "plugins" by default. The packages searched for plugins can be changed using the "vdmj.cmd.plugin_packages" JVM property.

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    static final String
    HELP
     

    Fields inherited from class com.fujitsu.vdmj.plugins.AnalysisCommand

    argv, line, registry

  • Constructor Summary

    Constructors
    Constructor
    Description
    TranslateCommand(String line)
    The constructor is called from the command line interpreter when the user first types "translate ".

  • Method Summary

    Modifier and Type
    Method
    Description
    String
    run(String line)
    The run method is called whenever the user types "translate " in the VDMJ command line interpreter (CommandReader.java).

    Methods inherited from class com.fujitsu.vdmj.plugins.AnalysisCommand

    getCommandHelp, parse

    Methods inherited from class java.lang.Object

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

  • Field Details

  • Constructor Details

    • TranslateCommand

      public TranslateCommand(String line)
      The constructor is called from the command line interpreter when the user first types "translate ". It is passed the whole line typed by the user, which is broken into an argv[] array by the superclass.

  • Method Details

    • run

      public String run(String line)
      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 "argv" array, which is created during construction (above). The example run method uses the ClassMapper to turn the type checked tree (from the TCPlugin) 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 returned by the method, which appears in the user console session.
      Specified by:
      run in class com.fujitsu.vdmj.plugins.AnalysisCommand