Using command line

One simple way to start using VDMJ is to install the distribution and start the tool from a terminal.

The VDMJ distribution is a ZIP file containing all of the necessary jars and documentation. Unzip this in a convenient location and then include that folder in your shell's PATH. You will then be able to run a bash shell script called vdmj.sh which gathers all of the necessary jars and starts Java for you.

PATH=$PATH:~/vdmj-suite-4.5.0/

nick@cube:~> vdmj.sh 
Usage: vdmj.sh [-help] <VM and VDMJ options>

nick@cube:~> vdmj.sh -help
Usage: VDMJ [-vdmsl | -vdmpp | -vdmrt] [<options>] [<files or dirs>]
-vdmsl: parse files as VDM-SL (default)
-vdmpp: parse files as VDM++
-vdmrt: parse files as VDM-RT
-w: suppress warning messages
-v: show VDMJ jar version
...

nick@cube:~> vdmj.sh -vdmsl -i test.vdmsl
Parsed 2 modules in 0.057 secs. No syntax errors
Type checked 2 modules in 0.135 secs. No type errors and no warnings
Initialized 2 modules in 0.156 secs. No init errors
Interpreter started
> print f(10)
= 11
Executed in 0.009 secs.
>

The vdmj.sh script uses bash. If you do not have this shell available (it is available on Macs, and can be installed on Windows machines), you can alternatively start VDMJ by calling Java directly. For simple use, you can use the main VDMJ jar; for more complex use, you must append other jars from the distribution on your classpath and specify the main class as "VDMJ" in the default package. For example:

nick@cube> java -jar vdmj-4.5.0.jar 
You did not identify any source files

nick@cube> java -jar vdmj-4.5.0.jar -vdmsl -i test.vdmsl
Parsed 2 modules in 0.057 secs. No syntax errors
Type checked 2 modules in 0.135 secs. No type errors and no warnings
Initialized 2 modules in 0.156 secs. No init errors
Interpreter started
> p f(1)
= 2
Executed in 0.009 secs. 
> q
Bye

nick@cube> java -cp vdmj-4.5.0.jar:annotations-4.5.0.jar:cmd-plugins-4.5.0.jar:stdlib-4.5.0.jar VDMJ -annotations -i test2.vdmsl
Parsed 1 module in 0.103 secs. No syntax errors
Type checked 1 module in 0.313 secs. No type errors
Initialized 1 module in 0.292 secs. No init errors
Interpreter started
> q
Bye

Note that there are two builds of VDMJ, one that uses standard 64-bit precision arithmetic, and one that uses high-precision. The high-precision distribution ZIP has a version that includes -P, both in the ZIP name and in the extracted folder. So you can install both versions of VDMJ at the same time, as long as you are careful to only use jar(s) from one location at runtime - don't try to mix jars!

The high-precision jar adds a -precision <n> command line option and interactive command to set the decimal precision you want:

nick@pollux:~> vdmj.sh -precision 20 -i
Interpreter started
> precision
Decimal precision = 20
> p 1/3
= 0.33333333333333333333
Executed in 0.008 secs. 

> precision 50
Decimal precision = 50
> p 1/3
= 0.33333333333333333333333333333333333333333333333333
Executed in 0.002 secs. 

> precision 100
Decimal precision = 100
> p 1/3
= 0.3333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333
Executed in 0.002 secs. 
>