CHANGELOG.md

2.0.1

2.0.0

• Added:
  • QuickCheck integration in the POG view
  • Toolbar button to run POG on entire project
  • Hover panel with QuickCheck details
  • Inline editor warnings for PO results
  • PO #nnn CodeLens for counterexample/witness execution
  • Dep POs CodeLens for dependency filtering
  • Copy button for proof obligations
  • Function breakpoints support
  • Automatic typechecking on interpreter cold start
  • Launch|Debug CodeLens support for curried and polymorphic functions
  • Draggable divider in RT Log View
• Changed:
  • Improved POG generation workflow and UX
  • Enhanced handling of large POG executions (progress bar and cancel support)
  • Outline view now refreshed automatically on save
  • Improved navigation for missing proof obligations
• Fixed:
  • Various stability improvements
  • Multiple crash handling fixes

VDMJ 4.7.0 Release Features:

• Various minor bug fixes
  • VDMUnit has @NoPOG annotation
  • forall and exists expressions now work with undefined values
  • Bugs #76 and #77 fixed
• New features:
  • @TypeBind, @MaximalTypes and @SetProperty annotations added
  • "RemoteControl" example added
  • MATH`defined function added
• POG developments:
  • Operation POG considerably improved
  • Adds @LoopInvariant, @LoopMeasure and @OperationMeasure
  • New "constants", "reasons" and "undefined" QC strategies
  • POG support for specification statements and implicit func/ops
  • QC counterexamples now listed within the PO listing
  • "pogdep" command added
  • QC timeout is now in milliseconds
• VDM-VSCode support:
  • Stacks show hidden variables correctly
  • lsp.IgnoreWarnings property added for unused files
  • "pog" and "pogdep" commands added
  • New "Free Variables" scope in stack of lambda expressions
  • Support for POG GUI progress and cancel
  • New "Dep POs" code lens to list dependent obligations
  • New "PO #n" code lens to launch counterexamples

1.5.1

• Add support for PO code lenses.
• Subsequent launches of polymorphic code lenses now prefill type arguments.
• Fix "Debug example" in QuickCheck panel of PO view in workspaces with multiple modules.
• Add postfix helper text in launch configuration input prompt.
• Scope transfer of type arguments to function name.

1.5.0

• 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.

1.4.0

• Updates to VDMJ:
  • Added the slsp/POG/quickcheck processing to support the GUI button
  • Better support for disconnect and terminate (faster)
  • Use a "quickcheck.json" configuration file
  • Rationalise the LSP plugin architecture
  • Prohibit certain VDM-RT operators during initialization
  • Improved stack trace display for object oriented dialects
  • Support for improved annotation and plugin configuration in UI
  • Various minor bug fixes.
• Include QuickCheck plugin as default plugin in extension.
• Rewrite of Proof Obligation View that adds integration with QuickCheck tool.
• Improvements to the management of VDMJ plugins, libraries and annotations.
• Add the ability to read VDMJ enhancements from external VS Code extensions.
• Fix name of generated debug configuration (issue #214).
• Fix code lenses on polymorphic functions (issue #188).

1.3.7

• Hotfix to VDMJ to support Java 19
• Updates UML Plugin jar to 0.1.1 including typing abstraction

1.3.6

• Hotfix to uml plugin jar: fixes stereotypes not translating correctly to VDM

1.3.5

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

1.3.4

• Added Real-Time-Logger View
• Fixed Hover of variables in the debug
• Added groups to settings
• Added high precision 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
• Added extracting of embedded VDM in external sources

1.3.3

• 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

1.3.2

• Added additional options and buttons to the combinatorial testing view
• Added partly migration to Web extension
• Improved the inline coverage display
• Improved the look of the POG view
• Changed library import to support dynamic inclusion from jar files
• Changed logging to console output
• Large refactoring of SLSP features
• Fixed POG view update bug
• Fixes to VDMJ

1.3.1

• Added VDMUnit lib
• Added translation settings
• Changed POG View's "proved" with "status"
• Improved completion suggestions
• Improved Server logging
• Improved Debug Watch
• Improved file encoding support
• Removed dependency on portfinder
• Fixes to VDMJ

1.3.0

• Added Launch and Debug code lenses
• Added code snippets (template expansion)
• Added support for Remote Control class
• Added coverage reporting to Latex
• Added Java Gen. options
• Improved breakpoint support
• Improved import example interface
• Changed annotations path setting to class path setting, and improved UI in settings
• Changed names for server related settings
• Correction to IO lib
• Fixes to VDMJ

1.2.1

• Fixes to debug launching
• Added dependency graph generation
• Improved CT result filtering

1.2.0

• Improved outline view
• Fixes to MATH lib
• Added import example projects
• Added CSV lib support
• Added more debug configuration snippets

1.1.3

• Added keywords to syntax highlighting
• Fixes to VDMJ

1.1.2

• Add library functionality
• Add coverage decorations
• Fixes to VDMJ

1.1.1

• Allow multiple JVM settings
• Minor correction to location of values
• Improvement to module initialization retries
• Added VDMJ "order" plugin to help create ordering files (VDMJ only)
• Add POG mapping for "ext" clauses
• Correct trace execution context bug
• Fix bug with free variables for type invariant functions
• Improve UI focusing on exceptions and breakpoints
• Allow trace inits to use cached data (experimental)
• Enable F12 goto definition for ext, errs and specification statements

1.1.0

• Updated license
• Warning for unused imports
• Removed duplicate type checking errors
• Allow nested comments
• Added scheme to control parse ordering

1.0.5

• Added logging of server stdio to a file or terminal, this allows annotations to be printed during CT execution
• Specifications with "Too many type checking errors" handled sensibly
• Maintain synchronisation between client and server on folder deletion
• Improved handling of types that are imported
• Better watch variable output when variables are not in scope
• Allow manipulation of breakpoints while stopped at a breakpoint

1.0.4

• Fixes to syntax highlighting
• Initialization and execution are asynchronous and can now be interrupted or paused using the VSC controls (fixes bug #11)
• Output to the console make more consistent use of stdout and stderr
• Better console messages when specifications are terminated or interrupted
• Allow changed "set" settings to take effect on restart
• Several F12 definition location corrections (see bug #6)
• Advice is to use "continue" to exit debug sessions that catch exceptions, rather than the stop button (see bug #9)
• Improved handling for Java internal errors, like OutOfMemory

1.0.3

• Updated language server

1.0.2

• Changed launch file configurations

1.0.1

• Added icon to extension

1.0.0

• Initial Release