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"
       }
    ]
}