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.

• 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 QuickCheck
• A new code lens has been added for launching PO counterexamples "inline"
• The QC timeout is now in milliseconds - remember to update your .vscode/quickcheck.json
• MAYBE QC results now check for PO variables that may not have been reasoned about, as a warning.
• The MAYBE heuristic above is added to a "reasons" strategy for QC
• A new "constants" QC strategy uses PO constants to bias counterexample searching.
• VSCode stack traces now correctly show location of lower frames, and hidden variables are displayed correctly.
• Operation POs are now considerably improved, generating multiple POs for alternative paths.
• A new @LoopInvariant obligation produces POs for while loops.
• Operation postcondition POs are now handled correctly, with old/new state values.
• A new lsp.noIgnoreWarnings property has been added to suppress ignored file warnings from LSP.
• Corrected non-deterministic statement POContext handling.
• Improved support for @LoopInvariant annotation and POs.
• Extended "undefined" boolean handling to cover forall and exists expressions.
• Improved POG coverage of various loop types.
• Added @LoopGhost annotation for for-all and for-pattern loop statements.
• Added @TypeBind annotation for manually instrumenting forall and exists expressions, as QC does for POs.
• Added @LoopMeasure annotation for loop termination checks.
• Added a pog command to the VDM-VSCode console, for convenience.
• Added a remote example project for the RemoteControl interface, based on the Conway GUI.
• Added MATH'defined: ? +> bool to help with undefined booleans.
• Updated POG to replace (some) op call ambiguous cases with forall contexts.
• Fixed bug #76
• Updated POG to cover most op calls with forall contexts.
• Increased the POG GUI timeout to 5s, to allow for longer operation PO checking.
• Tolerate various QC exceptions in VDM++/RT and treat as MAYBE results.
• Added @MaximalTypes and @SetProperty annotations.
• Fixed bug #77 - to rationalise the quoting convention for toStrings throughout.
• Added a "Free Variables" scope in the stack display of lambda value executions.
• Removed @LoopGhost and allow other loop annotations to pass a ghost name.
• Corrected loop POs to include a path where the loop is not entered.
• Calculate transitive closure of operations' updates to state to generate better POs.
• Better POG support for specification statements
• Limit POG path expansion for very complex operations
• Fixed QC of implicit function calls and some PP/RT constructor cases
• Added @OperationMeasure annotation
• Support mutual recursive loops with @OperationMeasure
• Added a more detailed display of counterexample steps
• Interleave counterexample analysis with PO source after QC.
• Add pogdep command to display POs dependent on a constraint symbol
• POG generation has progress and cancel button in VSCode
• New Dep POs code lens to filter POG to the POs that are dependent on constraints
• New button for opening POG directly
• The source of POs can now be copied in VSCode
• Various changes to support VSCode POG improvements