Release 2.0.0

VDM-VSCode 2.0.0 is a major release bundling VDMJ 4.7.0, introducing a significantly improved workflow for Proof Obligation Generation (POG) and a closer integration with QuickCheck, alongside multiple usability improvements and stability fixes.

Major Highlights

• Closer QuickCheck integration in the POG view
• New support for POs generated from VDM-SL operations
• Improved interaction with Proof Obligations (hover info, inline feedback, code lenses)
• Better performance and usability for large POG executions
• Enhanced debugging and editor integrations

QuickCheck Integration in the POG View

This release brings a closer integration of QuickCheck into the POG view. The POG can now be invoked in two ways: by right-clicking a file in the Explorer and selecting VDM, then Run Proof Obligation Generation, or via the new editor toolbar button to run it on the entire project.

The QuickCheck button invokes the lightweight check on the obligations filtered, which may change their status to Failed, Provable, or Maybe, indicating that the PO is definitely falsifiable, probably provable, or that we cannot be certain either way. After a QuickCheck, hovering over the Status will display a panel with extra information. Failed POs may also be displayed in-line in the editor as a warning. A PO #nnn code lens appears in the editor above any PO that has a counterexample or witness: clicking them launches an execution using those values, just like a Launch|Debug lens.

Additional POG view improvements in this release

• Counterexamples are now expanded as comments within the PO listing to show which bindings are required at which levels to falsify the expression. For example:
  (forall a:nat & --> a = 7 (a - 7) <> 0) --> returns false
• A progress bar is displayed while PO generation is in progress. For projects with more than 20 POs, a Cancel button is also available to interrupt the process.
• When POs are missing from the view (e.g. when an operation generates too many alternative paths through its body), a warning indicator in shown at the top of the view and in the editor, along with a Go to definition button to navigate to the related definition. An inlay hint then gives more information/advice in context.
• A new Dep POs code lens appears above preconditions, postconditions and invariants, after POG. Selecting it filters the view to show only those POs directly affected by the chosen constraint.
• A copy button on each PO lets you copy the obligation source to the clipboard.

Operation POG

• Proof Obligations are generated for most VDM-SL operations, as well as functions.
• This uses new @LoopInvariant, @OperationMeasure and @LoopMeasure annotations.
• This also supports implicit operations and specification statements.

Other Improvements

• Function breakpoints are now supported - set a breakpoint by function name from the + button in the Breakpoints panel header.
• The interpreter now correctly supports cold starts; if started without first opening a VDM file, a full typecheck is triggered automatically before the session begins.
• Launch and Debug lenses now work for curried and polymorphic functions.
• The Outline view is now automatically refreshed on save. Double-clicking outline entries correctly highlights the definition concerned.
• Class hierarchies can now be displayed in VDM++/RT, via the Show Type Hierarchy menu option.
• A Quick Interpreter can be opened from the VDM menu, to evaluate stand alone expressions.
• Variable hiding is handled correctly in stack views and a new Free Variables context is available in lambda evaluations.
• Undefined value handling (LPF logic) is extended to include forall and exists exoressions.
• A draggable divider has been added to the RT Log View.
• New @TypeBind, @SetProperty and @MaximalTypes annotations are available (see Annotation Guide).
• Various stability and crash handling improvements.

VDMJ Engine

This release uses VDMJ 4.7.0, which introduces improvements to POG, QuickCheck strategies, annotations, and overall engine stability.

Release 1.5.1-SNAPSHOT

This pre-release adds support for proof obligation code lenses and contains various improvements to the QuickCheck integration.

Release 1.5.0

This release stabilizes the addition of the QuickCheck integration and updates the VDMJ JARs to the new stable 4.6.0 version. The changes in this release include:

• Update VDMJ JARs to stable 4.6.0 release.
• Fix default enabled plugins not always being enabled for users updating from an earlier version of the extension.
• Enable uml as default plugin.
• Minor improvements to Proof Obligation view.
• Add extension configuration of VDMJ release mode. Classic release can now be enabled.

Release 1.4.0-beta

v1.4.0-beta.14

• Fix default enabled plugins not always being enabled for users updating from an earlier version of the extension.
• Enable uml as default plugin.
• Improve alignment of filter and buttons in Proof Obligation View.
• Improve warning message added in 1.4.0-beta.12, so it only displays when proof obligation fails.

v1.4.0-beta.13

• Change extension configuration of VDMJ release to be an enumeration of "vdm10" and "classic"
• Add workspace settings.json to all classic examples

v1.4.0-beta.12

• Add extension configuration to enable VDM classic release.
• Change PO view title to also include file name if PO generation was run on a single file, as opposed to the entire workspace folder.
• Add a warning message in the PO view if no POs are available.
• Fix bug in multi-root workspaces, where QuickCheck requests would be sent to the incorrect VDMJ instance.

v1.4.0-beta.11 (released onto the VS Code Marketplace as 1.4.0)

• Fix incorrect highlighting of character literals by reverting changes to syntax highlighting.

v1.4.0-beta.10

• QuickCheck panel UI improvements
  • Static position at bottom of PO view.
  • Utilize space in panel more efficiently
  • Make UI more stable
• Increase default QuickCheck timeout to 5 seconds.
• Enable QuickCheck plugin by default.

v1.4.0-beta.9

• Annotation management improvements, show built-in annotations in UI.
• Fix: add annotations.json to built-in annotations jar so it is detected.

v1.4.0-beta.8

• Update VDMJ plugin jars - add plugin.json metadata to UML plugin/
• Add/update VDMJ HP jars and QuickCheck plugin.
• Add annotation management UI.
• Clean up handling of VDMJ extensions, i.e. libraries, plugins, annotations. They all share common search path now.

v1.4.0-beta.7

• Update VDMJ plugin jars - add plugin.json metadata to QuickCheck plugin
• Add plugin management UI.
• Improve library addition functionality to also show user-defined libraries.

v1.4.0-beta.6

• Update VDMJ jars.
• Fix bug that would cause POG view to blank on QuickCheck results without launch command.

v1.4.0-beta.5

• Show incremental progress during QuickCheck runs.

v1.4.0-beta.4

• Add visual progress indicator when QuickCheck is running.
• Show cancel button instead of "Run QuickCheck" during long-running QuickCheck.

v1.4.0-beta.3

This pre-release includes improvements and bug-fixes to the QuickCheck integration:

• QuickCheck now only runs on the visible subset of proof obligations.
• Fixed bug where QuickCheck info would become stale when changing settings and subsequently running QuickCheck.

v1.4.0-beta.2

This pre-release includes improvements to the QuickCheck integration as well as multiple bug-fixes.

• Fix char literals syntax highlighting (issue #190)
• Fix name of generated debug configuration (issue #214)
• Fix code lenses on polymorphic functions (issue #188)
• Add the ability to configure QuickCheck using JSON

v1.4.0-beta.1

This is the first pre-release leading up to version 1.4.0 that will feature support for the QuickCheck plugin. Changes include:

• Updated VDMJ jars to 4.6.0-SNAPSHOT
• Added QuickCheck plugin jar 4.6.0-SNAPSHOT
• Rewrite of Proof Obligation webview using React.
• Added QuickCheck functionality into Proof Obligation view.

Release 1.3.7

This release includes the latest additions to VDMJ, a hotfix to comply with Java 19, and the new UML translator jar.

Release 1.3.6

This release is a hotfix to the UML plugin jar.

Release 1.3.5

This release includes the latest additions to VDMJ including a fully fledged plugin architecture, a real time logger view among others:

• Added VDM to (Plant) UML translation feature
• Added VDMJ 1.5.0 features (Analysis plugins,...)

Release 1.3.4

This release includes the latest additions to including a real time logger view among others:

• Added Real-Time-Logger View
• Fixed Hover of variables in the debug
• Added groups to settings
• Added highprecision indicator to the status bar
• Added tracing of DAP messages in the terminal
• Added precision to the launch configuration settings
• Added default file nesting for sources like word files

Release 1.3.3

This release addresses these issues. Below is a highlight of some of the new features.

• Updated the publisher name (Breaks settings! Workaround: Replace 'jonaskrask.xyz' to 'overturetool.xyz')
• Added Open in VDMTools Feature
• Added FMI Import/Export features (Port from Overture codebase)
• Added "Change Project Wide VDMJ Properties" Command
• Added a .vscode/vdmignore file to ignore selected files
• Enabled user-provided commands for the debug console
• Added a "state init" proof obligation
• Added support for doc, docx, odt and adoc and md source files
• Added Shift-F12 "find references" functionality

Hotfix v1.3.2

This hotfix release addresses these issues. Below is a highlight of some of the new features.

Improvement to the inline coverage report
The inline coverage report now colours parts that have not been executed in red and the parts that have been executed in green.
The strength of the green colour is assigned according to how many times that piece of the specification has been executed.

New buttons for CT view
The CT view has been improved with new buttons that change the way you switch between workspace folders.

Improved library import
The library import has been changed to support the inclusion of user-defined libraries.

Partly migration to web
A part of the extension has been migrated to web VS Code. However, it is only the client-side features (syntax highlighting and snippets) that are enabled in the web extension.

Refactoring
Large refactoring of SLSP related features. See the wiki for more information on the new design.

General fixes
Fixes to the client and VDMJ to ensure smoother operation of the extension