Code Generation - overturetool/vdm-vscode GitHub Wiki

It is possible to generate Java code for a large subset of VDM-SL and VDM++ models. In addition to Java, C and C++ code generators are currently being developed. Both these code generators are in the early stages of development. For comparison, code generation of VDM-SL and VDM++ specifications to both Java and C++ is a feature that is available in VDMTools.

See here how VDM values are used in Java.

Java Code Generation

The Java code generator can be launched by right-clinking the editor or the project in the explorer and selecting VDM > Generate Java Code. Upon completion of the code generation process, the status is output to the console. The generated code is available as a VS Code project in the .generated/java folder.

Limitations

If the Java code generator encounters a construct that it cannot code generate it will report it as unsupported to the user and the user can then try to rewrite that part of the specification using other (supported) constructs. Reporting of unsupported constructs is done via the console output and using editor markers.

The Java code generator currently does not support code generation of multiple inheritances and neither does it support traces, type binds, invariant checks and pre- and post-conditions. Furthermore, let expressions appearing on the right-hand side of an assignment will also be reported as unsupported. The Java code generator also does not support every pattern. The patterns that are currently not supported are: object, map union, map, union, set, sequence, concatenation and match value.

About the Runtime Library

The generated code relies on a runtime library used to represent some of the types available in VDM (tokens, tuples etc.) as well as collections and support for some of the complex operators such as sequence modifications. For simplicity, every project generated by the Java code generator contains the runtime library. More specifically, there is a copy of the runtime library containing only the binaries (lib/codegen-runtime.jar) as well as a version of the runtime the library that has the source code attached (lib/codegen-runtime-sources.jar). The runtime library is imported by every code generated class using the Java import statement import org.overture.codegen.runtime.*; and in order to compile the generated Java code, the runtime library must be visible to the Java compiler. Similar to VDMTools the runtime library also provides an implementation for a subset of the functionality available in the standard libraries: The runtime library provides a full implementation of the MATH library, support for conversion of values into character sequences as provided by the VDMUtil, and finally functionality to write to the console as available in the IO library.

Configuration

The Java code generator provides a few options that allow the user to configure the code generation process. This is configured via a preference page that can be accessed at:

  1. Go to File > Preferences > Settings
  2. Choosing Workspace (not User)
  3. Select in the left side tab Extenstions > VDM VSCode

Disable Cloning

In order to respect the value semantics of VDM the Java code generator sometimes needs to perform deep copying of objects that represent composite value types (records, tuples, tokens, sets, sequences and maps). For example, in VDM a record is a value type, which means that occurrences of the record must be copied when it appears on the right-hand side of an assignment, it is passed as an argument or returned as a result. However, Java does not support composite value types like structs and records, and as a consequence, record types must be represented using classes, which use reference semantics. This means that an object reference, which is used to represent a composite value type in the generated Java code must be deep copied when it appears in the right-hand side of an assignment, it is passed as an argument or returned as a result. For arbitrarily complex value types (such as records composed of records) deep copying may introduce significant overhead in the generated code. If the specification subject to code generation does not truly rely on value semantics the user may wish to disable deep copying of value types in the generated code in order to remove this overhead. The user should, however, be aware that disabling cloning may lead to code being generated that does not preserve the semantics of the input specification and in general disabling cloning is discouraged. By default, cloning is enabled.

Generate Character Sequences as Strings

In VDM a string is a sequence of characters and there is no notion of a string type. Java in particular works differently since it uses a separate type to represent a string. The default behaviour of the Java code generator is to code generate sequences of characters as strings and subsequently do the necessary conversion between strings and sequences in the generated code. Another possibility is to treat a string literal for what it truly is, namely a sequence of characters, and thereby avoid any conversion between strings and sequences. In order to do that, i.e., not generating character sequences as strings, the corresponding option must be disabled.

Generate Concurrency Mechanisms

If the user does not rely on the concurrency mechanisms of VDM++ and does not want to include support for them in the generated code the corresponding option in the preference page must be unchecked. By default, the behaviour of the Java code generator is to not include support for the concurrency mechanisms of VDM++ in the generated code.

Generate VDM Location Information For Code Generated Constructs

When a VDM model is code generated it can be helpful to know where the constructs in the generated code originate from. When this option is enabled the Java code generator will generate VDM location information for methods, statements and local declarations in the generated code. More specifically, the Java code generator will generate a Java source code comment containing the name of the VDM source file and the line number and the position, for each method, statement and local declaration. As an example, the code fragment below says that the Java return statement originates from a VDM construct at line 25, position 12 in File.vdmsl.

/* File.vdmsl 25:12 */
return 42;

Choose Output Package

The Java code generator allows the output package of the generated code to be specified. If the user does not specify a package, the code generator outputs the generated Java code to a package with the same name as the VDM project. If the name of the project is not a valid java package, then the generated code is output to the default Java package.

Skip Classes/Modules During the Code Generation Process

It may not always make sense to code generate every class or module in a VDM project. A class or module can often be skipped if it acts as an execution entry point or is used to load input for the specification. Classes or modules that the user wants to skip can be specified in the text box in the Java code generator preference page by separating the class/module names by a semicolon. As an example, World;Env makes the code generator skip code generation of World and Env, while generating code for any other module or class. For convenience, the output of the Java code generator will also inform the user about what classes or modules are being skipped.

Translations of the VDM Types and Type Constructors

The Table below describes how VDM types in the left column are represented in the generated Java code (the right column). In this table pack is the user-specified root package of the generated Java code and E, D and R represent arbitrary VDM types. The type mapping in the last row is only used when the Generate character sequences as strings option is selected. Some of the types used to represent the VDM types are native Java types (from package java.lang), others are part of the Java code generator runtime library (from package org.overture.codegen.runtime), and some are generated.

VDM type(s) Java type
bool java.lang.Boolean
nat, nat1, int, rat, real java.lang.Number
char java.lang.Character
token org.overture.codegen.runtime.Token
Tuple types (e.g. nat * nat) org.overture.codegen.runtime.Tuple
Union types (e.g. nat | nat) java.lang.Object
Quote type <T> pack.quotes.TQuote
User-defined types T = D Represented using the representation of type D
A class C pack.C
Record type R defined in class or module M Inner class pack.M.R
set of E org.overture.codegen.runtime.VDMSet
map D to R, inmap D to R org.overture.codegen.runtime.VDMMap
seq of E, seq1 of E org.overture.codegen.runtime.VDMSeq
seq of char, seq1 of char java.lang.String