NetMeeting 142


Deadline	24 November 2024, 12:00 CEST
Participants	See git log

Review Status of the Action List

Improvements on on-the-fly testing

On-the-fly testing triggers both unit tests and traces at every modification to the source specification.
Failed/error tests can be debuged on Smalltalk debugger.

Improvements on slicing

Improvements on EpiLogue

VDMJ 4.6.0 and VDM-VSCode 1.5.0 released. Work is now proceeding against the 4.7.0-SNAPSHOT.
The most significant development work is better production of proof obligations for operations (as opposed to functions). This requires the tracking of possible updates to mutable variables (state, or dcl declarations) and limits the POs that can be discharged with QuickCheck easily. But many more operation POs are now checkable, rather than being “Unchecked” - for example, ~40% of POs in the Overture example suite were Unchecked; now that is down to ~14%. The work is currently only sensible in VDM-SL, since the object state in VDM++/RT is much harder to reason about.
In connection with the changes above, a new code lens is now produced by the POG, labelling failed obligations inline. When these lenses are clicked, they work like the regular “Launch/Debug” lenses, but substitute counterexample arguments that have been discovered by the QuickCheck process. This allows counterexamples to be debugged very easily.
Leo has been using the above to check some very large models - including the VDM_Toolkit and some confidential models from Newcastle. Feedback here has led to many bug fixes(!) and improvements.
Markus is working on updates to the GUI front end. If anyone wants to try the new POG/GUI, let me know - we produce patch VSIX files for people to try, but development is ongoing.

See download stats on number of installs.

Will happen in June 2025 co-located with INTO-CPS workshop in Aarhus, Denmark

The Strategic Research Agenda is reviewed every other NetMeeting.

In addition there is a physical meeting at OVT-23 as planned.