Integration between VS Code and Java code can be established, either by writing native libraries in Java that can be called from VDM or by giving a Java program overall control of a VDM model by making calls to that model as a user interacts with a GUI. In both cases, internal VDM values have to be handled by Java -– either because they are passed as arguments to a Java library, and returned as results to VDM, or because they are returned from a VDM model evaluation to a controlling Java program. This page describes the internal class hierarchy used by VDMJ to represent internal VDM model values and describes how a Java program can convert these to Java values (int, long, String etc.) as well as creating internal values for returning to the VDM model (e.g. as the return value of library methods).

All internal VDM values in VDMJ are held by instances of the Value class with the fully qualified name, com.fujitsu.vdmj.values.Value. The Value class itself is abstract, but subclasses can be instantiated to represent any VDM value, such as a “seq of char”, “nat1’” or a value of an arbitrarily complex type. The hierarchy is shown in the figure below.

Generally, the name of the Value subclass for a VDM type is on the form <name>Value, for example BooleanValue or SeqValue.

The following sections describe how to obtain Java values from a Value object, and how to create Value objects from basic Java values (or iteratively from other values).

Most primitive VDM types have subclasses with simple constructors that take a Java primitive type as an argument:

public BooleanValue(boolean value)
public CharacterValue(char value)
public RealValue(double value) throws Exception
public RationalValue(double value) throws Exception
public IntegerValue(long value)
public NaturalValue(long value) throws Exception
public NaturalOneValue(long value) throws Exception
public QuoteValue(String value)
public NilValue()

The constructors that throw exceptions are the ones for which some Java value does not match the VDM type concerned. For example, a RealValue or RationalValue cannot take the Java values Double.NaN or Double.POSITIVE_INFINITY as a constructor argument. Similarly, NaturalValue and NaturalOneValue cannot take a negative long as an argument.

Note that a QuoteValue is constructed with a string. This is simply the string value that would appear between angle brackets in VDM, for example <FAIL> would be constructed with the Java string "FAIL".

To convert a VDM value into a Java value, the Value class provides a number of conversion methods, each of which returns the corresponding Java primitive value, or throws an exception if the conversion cannot be made for the VDM type concerned:

public boolean boolValue(Context ctxt) throws ValueException
public char charValue(Context ctxt) throws ValueException
public double realValue(Context ctxt) throws ValueException
public double ratValue(Context ctxt) throws ValueException
public long intValue(Context ctxt) throws ValueException
public long natValue(Context ctxt) throws ValueException
public long nat1Value(Context ctxt) throws ValueException
public String quoteValue(Context ctxt) throws ValueException

Note that all of these conversion functions take a Context parameter as argument and potentially throw a ValueException. The Context parameter is used internally by VDMJ and represents the call stack during the evaluation of an expression. This parameter can be set to null when using these methods in Java code outside VDMJ. A ValueException is thrown if the VDM value cannot be converted into the Java type requested. For example, calling booleanValue on a RealValue object will raise a ValueException with the message text "Can’t get bool value of real".

VDM allows primitive types to be built into more complex aggregations and collections, and these can also be converted to and from Java types, though the process is a little more involved. Three classes are provided to assist with this conversion: ValueSet, ValueList and ValueMap (all within the same com.fujitsu.vdmj.values package). These classes represent, respectively, a Java Set, List and Map of VDM values:

public class ValueSet extends Vector<Value>
public class ValueList extends Vector<Value>
public class ValueMap extends LinkedHashMap<Value, Value>

Note that the ValueSet class is actually based on a Java Vector, not a Java Set type, though the class does have set semantics (no duplicates). This is an implementation detail and allows VDMJ to permute set orderings in certain circumstances.

These three classes have obvious constructors, and allow Values (or collections of them) to be added to the collection subsequently, using standard Java collection methods:

public ValueSet()
public ValueSet(int size)
public ValueSet(ValueSet from)
public ValueSet(Value v)

public ValueList()
public ValueList(ValueList from)
public ValueList(Value v)
public ValueList(int size)

public ValueMap()
public ValueMap(ValueMap from)
public ValueMap(Value k, Value v)

Using these three helper classes, it is now possible to create VDM set, sequence and map values, using constructors of the SetValue, SeqValue and MapValue classes:

public SetValue()
public SetValue(ValueSet values)

public SeqValue()
public SeqValue(ValueList values)
public SeqValue(String s)

public MapValue()
public MapValue(ValueMap values)

Note that there is a special constructor for SeqValue that takes a Java string. This creates a VDM seq of char, but without the need to create a ValueList with CharacterValues.

If the ValueList (or another) collection passed to these constructors contains a mixture of VDM types -– i.e. a mixture of VDM Value subclasses, such as a BooleanValue and a NaturalOneValue -– then the type of the constructed VDM value is the union of the various types passed, in this example seq of (bool j nat1). If this VDM type is not compatible with the use of a corresponding value in the VDM model a dynamic type exception occurs when the value is processed by the model.

Lastly, as before, to get the primitive Java values of a VDM collection, the following methods are provided:

public ValueList seqValue(Context ctxt) throws ValueException
public String stringValue(Context ctxt) throws ValueException
public ValueSet setValue(Context ctxt) throws ValueException
public ValueMap mapValue(Context ctxt) throws ValueException

Note that, as with the SeqValue constructor, there is a special method to return a Java String from a seq of char SeqValue, rather than a ValueList of CharacterValues. As before, if the Value being used is not a sequence, set or map, then these methods will throw a ValueException.

The sections above describe how to create or deconstruct simple VDM values in Java as well as simple collections of these. The remainder of this section describes the unusual cases, for more sophisticated types.

VDMJ has an internal FunctionValue class used for holding values of functions (e.g. the value of a "lambda" expression or the value of a function defined within a module). But as far as Java is concerned, these values are opaque -– there is no equivalent Java construct, and the only way to evaluate a VDM function is to let VDMJ perform that evaluation. Similarly, Java cannot construct a FunctionValue.

The only operation that Java can reasonably perform with a FunctionValue is to create a composite function (eg. f1 comp f2 in VDM) or a function iteration (e.g. f ** 3 in VDM) using existing FunctionValues. In order to do this, there are two subclasses of FunctionValue, called CompFunctionValue and IterFunctionValue, the constructors for which are as follows:

public CompFunctionValue(FunctionValue f1, FunctionValue f2)
public IterFunctionValue(FunctionValue function, long count)

These both create new FunctionValues, which when evaluated by VDMJ act as the composition and iteration of the arguments, respectively.

There is a method for obtaining a FunctionValue from a Value, but note that this is not an internal Java value (unlike other Value methods, like realValue). It is used as a more convenient way of casting the Value to a FunctionValue.

public FunctionValue functionValue(Context ctxt)

When VDM++ and VDM-RT create new objects using the new operator, the resulting values are held as ObjectValues in VDMJ. These are complex types that involve function and operation definitions for the object as well as any type, value, sync, thread or traces sections defined. Therefore ObjectValues are really opaque to Java and cannot be used directly.

Like for FunctionValue, the ObjectValue class has a method for converting a Value into an ObjectValue:

public ObjectValue objectValue(Context ctxt)

A VDM record is just a collection of typed field values. A RecordValue can be obtained from a Value using the following method, which returns a RecordValue rather than some other Java representation:

public RecordValue recordValue(Context ctxt)

To get individual field values from a RecordValue, two more Java helper types have to be introduced, called FieldMap and FieldValue. A FieldValue has the following constructor, and represents a record field:

public FieldValue(String name, Value value, boolean comparable)

The comparable argument indicates whether this field is used in the value comparison between record values. A field declared with “-” in VDM would have a false argument, but normally this argument would be true, and the value must match the record type being used. FieldValues are added to a FieldMap, which is just a Java List of FieldValues.

So given a RecordValue, its FieldMap can be obtained from a public final field in the object, called fieldMap, and from there, individual FieldValues can be accessed -– e.g. fieldMap.get(0).name and fieldmap.get(0).value.

To create a RecordValue, the record type is obtained from the RemoteInterpreter:

type = remoteInterpreter.getInterpreter().findType(typename)

The type is then passed to the RecordValue constructor, along with a FieldMap or a ValueList (of the fields in order).

public RecordValue(RecordType type,
                   ValueList values,
                   Context ctxt)
public RecordValue(RecordType type,
                   FieldMap mapvalues,
                   Context ctxt)

The Context parameter is needed to allow records with invariants to check the invariant before the value is constructed. Note that currently, record types with an invariant cannot be constructed in Java. The Context parameter can be passed as null from Java.

The caller is responsible for passing field values that match their expected type. If they do not match, VDMJ throws a dynamic type exception for subsequent evaluations.

Token values are simply wrappers for normal VDM values, reflecting the way they are created in VDM, like mk_token("hello"), which would be a wrapper for a seq of char. There is no special way of getting a TokenValue from a Value, other than casting it. Having casted the Value, the wrapped value can be obtained from the public final Value field called "value".

Constructing a TokenValue is just a matter of passing the Value required:

public TokenValue(Value exp)

A TupleValue in VDMJ is a wrapper for a ValueList. The following method and constructor can be used like one would expect:

public TupleValue(ValueList argvals)
public ValueList tupleValue(Context ctxt)

A VDM type can be given a name and an invariant, e.g. when wrapping a primitive type without an invariant. VDMJ has a separate Value subclass for values of such types that simply combine the primitive Value with a FunctionValue for the invariant. However, as with RecordValues (which can also have invariants), it is not currently possible to create InvariantValues in Java for types that have an invariant. For types without an invariant, the constructor is as follows:

public InvariantValue(NamedType type, Value value, Context ctxt)

The NamedType is obtained in a similar way to the RecordType above, using the RemoteInterpreter. Note that the caller is responsible for passing a Value that matches the expected type. If they do not match, VDMJ will throw a dynamic type exception for subsequent evaluations.

Operations which do not return a value in VDM (i.e. ==> ()) return an instance of VoidValue in Java. The constructor has no arguments.