Date | 26 Nov 2023, 12:00 CEST |
Participants | PGL, LF, KP, TO, NB Minutes by NB |
No progress on issue #38 (Links to documentation repo). Carried forward.
RM #50 is now complete, awaiting updates to the LRM.
Currying in VDMJ will be aligned with VDMTools per previous discussions, which needs a small LRM change.
There is a new ongoing discussion about recursive measures.
Specification slicing has been implemented on Refactoring Browser, and we are preparing for the next major release.
Most work on VDMJ has been in support of the QuickCheck tool, testing it with ever larger sets of specifications and improving the LSP protocol support in anticipation of GUI changes to display/interact with counterexamples. Currently, if you run QC on the command line in VSCode, any counterexamples will be highlighted in the spec as warnings; in future, we hope to be able to automatically launch execution of these counterexamples, to let the user explore why they violate a proof obligation.
A new qcrun
command has been added, which allows a failed QuickCheck run to easily make a “debug” function call, using the arguments discovered in a counterexample.
No change, but Jonas Lund has joined the effort here to improve the GUI interface for proof obligations (see above).
See above.
Status. We keep with the previous plan. All members are requested to open issues on improving opportunities and we as a community should also improve the pages.
See download stats on number of installs.
Workshop submission to be sent to FM Organization by mid December. LF agreed to prepare a the proposal.
Also see Planned Publications.
It was agreed that people should review and update this page with their planned papers.
The OVT 21 proceedings is out in arXiv. https://arxiv.org/abs/2311.07120
None.
Hugo: It is an honour to do this role, but I have been more involved in teaching @ AU, thus less able to be on top of my community tasks. Next year, the challenge continues. With record student enrolment at AU, my workload will double, the Systems Engineering student pool will reach ~200s and the Programming Linear Algebra course I coordinate will serve ~150s students. And I have also major roles in two other massive courses at least. Thus, I think it is only fair to disclose in advance the following:
If I continue my role as Overture convener, I will be able to coordinate the calls to the core meetings and have a major role on OVT workshop organization, but I foresee less and less input from my side in the community tasks and activities.