Package commands

Class 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 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 ".
    • Constructor Detail

      • 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 Detail

      • 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