Skip to content

Commit

Permalink
Update Net-Meeting-142.md
Browse files Browse the repository at this point in the history
nickbattle authored Nov 17, 2024
1 parent 1fede93 commit 1839d65
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion _netmeetings/Net-Meeting-142.md
Original file line number Diff line number Diff line change
@@ -43,7 +43,7 @@ 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.
* 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.

0 comments on commit 1839d65

Please sign in to comment.