4.7.0-SNAPSHOT Release

This is the snapshot release of the upcoming 4.7.0 release of VDMJ.

Note: the release removes the classes and methods deprecated in the 4.5.0 release.

The VSIX file is a patched version of the 1.5.0 VDM-VSCode extension that uses this VDMJ snapshot. It fixes the following issues in 1.5.0:

• VDMUnit libraries now include @NoPOG annotations
• The POG view is corrected so that dynamic changes to the specification are visible to QuickCheck
• The vsix.sh script allows a patch to change the version of VDMJ artifacts
• More operation POs are now analysable by QuckCheck
• A new code lens has been added for launching PO counterexamples "inline"
• Change POG timeout to use milliseconds - remember to update .vscode/quickcheck.json
• MAYBE QC results now check for PO variables that may not have been reasoned about, as a warning.

4.6.0 Release

This is the 4.6.0 release of VDMJ.

The release mainly focusses on adding the necessary support to enable QuickCheck to be used effectively via the LSP protocol in the VDM-VSCode extension (which is available in release 1.5.0).

4.6.0-SNAPSHOT Release

This is the snapshot release of 4.6.0. It is initially the same as 4.5.0.

The VSIX is a snapshot of the upcoming 1.4.0 release, with the 4.6.0-SNAPSHOT jars included.

4.5.0 Release

This is the 4.5.0 release of VDMJ.

The most significant change in this release is the addition of the QuickCheck tool.

4.5.0-SNAPSHOT Release

This is a snapshot of the upcoming 4.5.0 release. It is initially the same as the 4.4.6 release.

Build 220813: Fixed bug #63 for the high precision build
Build 220814: Updated Apfloat library in high precision build to version 1.10.1.
Build 221122: Updated to cope with Java 19, which refines isVirtual() on Threads.
Build 230213: Created distribution assembly, including all jars and docs - see README in the ZIPs.
Build 230215: Updated VDMJUnit framework to use the new VDMJ analysis plugins
Build 230228: Added QuickCheck plugin to distribution and vdmj.sh script.
Build 230301: Added an installation section to the User Guide to describe the distribution ZIP.
Build 230303: Added LSP plugins command and missing precision command for high-precision.
Build 230910: Updated QuickCheck command.
Build 230911: More QuickCheck updates.
Build 230912: Added vscode.sh script to distribution and updated QuickCheck again.
Build 230916: Added more QuickCheck defences and POG tweaks for SL example specs.
Build 231023: Merged the 'maximal' changes from overturetool/language#50
Build 231024: Some @T related fixes for QC
Build 231031: Linked QuickCheck counterexamples with VSCode message/problem display.
Build 231101: Added overturetool.vdm-vscode-1.3.7-patch.vsix, patched with latest VDMJ jars
Build 231105: Updated VSIX patch with POG fixed from PGL.
Build 231106: Added proof explanation/witnesses and updated VSIX
Build 231110: Prevent breakpoint processing within QC for efficiency
Build 231124: Added "qcrun" command for VDMJ, updated VSIX.
Build 231126: Correct curried function measures to be curried.
Build 231127: Some qc and qcrun corrections for VDM++ and multi-module specs.
Build 231128: Add @NoPOG to stdlib sources, sort folder loaded files, add "qr" as an alias for "qcrun".
Build 231202: Fixed qcrun to work with polymorphic functions.
Build 231203: Added QC -i option and expanded help output. Fixed a bug with opaque record patterns in SL.
Build 231209: Added QC -v option to give more verbose output for processing.
Build 231217: Enable operation POs in some cases, add missing CT commands.
Build 231218: Skip "trivial" QC strategy if a PO has obligations itself.
Build 231219: Say "Obligation is always false" when no bindings, fix bug with missing bindings.
Build 231220: Refactor QC binding internals and allow QCRun to execute more cases.
Build 231221: Suppress some operation pre/post related POs for OO dialects.
Build 231222: More "qr" related fixes.
Build 231223: More "qc" related fixes - correct operation pre_op state name to "oldstate".
Build 231228: Add QC "direct" strategy.
Build 231229: Some POG improvements.
Build 240101: Added direct strategy support for cases-exhaustive.
Build 240102: Better version of cases-exhaustive direct strategy
Build 240103: Add counterexample context for direct cases failure
Build 240104: Changed PROVED to PROVABLE :-)

The new distribution packages come with a simple vdmj.sh bash shell script that starts VDMJ with a classpath that includes all of the appropriate jars from the distribution. Unzip the distribution and then add the root folder to your $PATH. Then you can use the script:

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 -vdmpp -i test.vpp 
Parsed 2 classes in 0.057 secs. No syntax errors
Warning 5000: Definition 'a' not used in 'A' (test.vpp) at line 4:8
Type checked 2 classes in 0.135 secs. No type errors and 1 warning
Initialized 2 classes in 0.156 secs. No init errors
Interpreter started
> p 1+1
= 2
Executed in 0.015 secs. 
> 

The latest distribution ZIP file includes a Quick Check tool, abbreviated to qc, which can sometimes find counterexamples to disprove proof obligations. For more information about QuickCheck, see the wiki. For example:

> help
...
quickcheck [-help][<options>][<POs>] - lightweight PO verification
qcrun <PO number> - execute counterexample/witness
...

> qc -help
Usage: quickcheck [-?|-help][-q|-v][-t <secs>][-i <status>]*[-s <strategy>]* [-<strategy:option>]* [<PO numbers/ranges/patterns>]

  -?|-help           - show command help
  -q|-v              - run with minimal or verbose output
  -t <secs>          - timeout in secs
  -i <status>        - only show this result status
  -s <strategy>      - enable this strategy (below)
  -<strategy:option> - pass option to strategy
  PO# numbers        - only process these POs
  PO# - PO#          - process a range of POs
  <pattern>          - process PO names or modules matching

Enabled strategies:
  fixed [-fixed:file <file> | -fixed:create <file>][-fixed:size <size>]
  search (no options)
  finite [-finite:size <size>]
  trivial (no options)
  direct (no options)

Disabled strategies (add with -s <name>):
  random [-random:size <size>][-random:seed <seed>]
> 

> qc
PO# 1, FAILED in 0.001s: Counterexample: a = -10
f: subtype obligation in 'DEFAULT' (test.vdm) at line 2:5
(forall a:real &
  is_nat((a + 1)))

> qr 1
=> print f(-10)
Error 4065: Value -10 is not a nat in 'DEFAULT' (console) at line 1:1
MainThread> q

You can download a patched version of the VDM-VSCode extension (below) that includes the latest VDMJ jars and plugins. To install or update an extension from a VSIX, type CTRL-SHIFT-Pin VSCode and select "Extensions: Install from VSIX" from the list that appears.

To use the QuickCheck plugin in VSCode, you have to add the following to the settings.json file in the project or workspace concerned. Note that you must change the "jar" pathname to point to the location of your own installation:

{
    "vdm-vscode.server.plugins": [
        {
            "classname": "quickcheck.plugin.QuickCheckLSPPlugin",
            "dialects": [ "vdmsl", "vdmpp", "vdmrt" ],
            "jar": "<YOUR INSTALL PATH>/.vscode/extensions/overturetool.vdm-vscode-1.3.7/resources/jars/plugins/quickcheck-4.5.0-SNAPSHOT.jar",
            "name": "QuickCheck Plugin"
       }
    ]
}

4.4.6 Release

This release formally includes all of the functionality of the 4.4.5-SNAPSHOT. There was a bug in the 4.4.5 release POMs, which required us to release a 4.4.6 fix immediately. Sorry for the confusion. You should not use 4.4.5 (a Maven build will fail).

The release has been packaged to allow it to be distributed from Maven Central. This required a groupId change, so rather than being part of "com.fujitsu", the new dependency is as follows:

<dependency>
  <groupId>dk.au.ece.vdmj</groupId>
  <artifactId>vdmj</artifactId>
  <version>4.4.6</version>
</dependency>

For a full list of component dependencies on Maven Central, see here.

4.4.4 Release

This is the formal release of the 4.4.4 and 4.4.4-P versions of VDMJ. They are included in VDM VSCode version 1.3.0.

One important change in this release concerns the use of standard library functions (IO, MATH etc). The native Java methods for these functions used to be in the main VDMJ jar. But these have now been moved to the stdlib jar, which also contains the sources for the libraries. To use the libraries therefore, you need to put both the VDMJ jar and the stdlib jar onto the classpath.

Another change is that you do not have to have your own local copy of (say) MATH.vdmsl in the project. You can simply refer to "MATH.vdmsl" on the command line, and as long as the stdlib jar is on the classpath, the source will be extracted into a temporary file and included for you. The temporary file is deleted when you quit the session.

Note that you have to use the -cp argument to Java, rather than -jar if you include more than one jar in the classpath.

$ java -cp vdmj-4.4.4.jar:stdlib-4.4.4.jar com.fujitsu.vdmj.VDMJ -vdmsl -i MATH.vdmsl
Parsed 1 module in 0.092 secs. No syntax errors
Type checked 1 module in 0.246 secs. No type errors
Initialized 1 module in 0.196 secs.
Interpreter started
> files
/tmp/tmp4596293493271508371MATH.vdmsl
> p sin(MATH`pi/4)
= 0.7071067811865475
Executed in 0.005 secs.
>

4.4.3 Release

This release adds important improvements to the LSP/DAP protocol implementation, most significantly structured outlines and the linkage of outlines to the editor and breadcrumbs. Also, the "order" option in the command line will write in Graphviz DOT format, if the output filename ends in ".dot".

The release is now included in VDM VSCode version 1.2.0.

4.4.2 Release

Release 4.4.2 adds significant functionality to the LSP/DAP server which supports the VDM VSCode extension.

4.4.2 Build 210113, Initial release.
4.4.2 Build 210202, Various updates from VDM VSCode testing
4.4.2 Build 210211, Final release.

The latest artifacts are available below.

4.4.1 VS Code Client Release

This is the first release to be included in the VS Code Client. It includes changes to the LSP/DAP subsystem to support this, as well as other fixes and improvements in the language engine.

4.4.1 Build 201120, Initial release
4.4.1 Build 210104, Fixed "stop" bug #21 in debugger, move DBGP into a separate module/jar.
4.4.1 Build 210105, Updated vdmjc client for separate DBGP jar. Updated user guide for threads.
4.4.1 Build 210106, Renamed VDMJC to DBGPC and moved documentation.
4.4.1 Build 210107, Added break, trace, list and remove commands to debugging environment, issue #41.
4.4.1 Build 210113, Final release, used in VS Code Client.

The latest assets are attached to this release.