|Date||26 February 2023, 12:00 CEST|
|Participants||PGL, TO, KP, LF Minutes by TO.|
Anne, Hugo, Ken, Leo, Nick, and Tomo are elected as language board memers.
No major changes.
Added a wiki to the GitHub site. Rather than being a separate version of the PDF documentation, it’s presented as a conversation about the PDF documents, with links to them.
Converted VDMJ internals to use the same plugin architecture as the LSP Server. So you can add new functionality (analyses and commands) by including a jar on the classpath.
Added a “QuickCheck” plugin (see above) example project for VDMJ that attempts to use value ranges to make explicit tests of proof obligations that include type binds (ie. most of them). This is also available as an LSP plugin. It should be regarded as experimental for now! Here’s how you use it:
functions f: real -> nat f(a) == a + 1; Interpreter started > p f(1) = 2 Executed in 0.161 secs. > qc -c Created 1 default ranges in ranges.qc. Check them! Then run 'qc' > qc Ranges expanded in 0.081s PO# 1, FAILED in 0.003s: Counterexample: a = 0.1 f: subtype obligation in 'DEFAULT' (test.vdm) at line 2:5 (forall a:real & is_nat((a + 1))) > qc -? Usage: quickcheck [-c <file>]|[-f <file>] [<PO numbers>] >
We have two MSc students looking at a new release pipeline and how to use DevOps to improve the integration of different components into the extension.
Tested the LSP Server with the Kate editor, and added a wiki page for its configuration.
New release will include recent changes to VDMJ (e.g. quick check). It will test a new DevOps approach to the releases under development at AU.
See download stats on number of installs.
OVT-21 is already under way. Reviews sent to authors this week.
Also see Planned Publications.
It was agreed that people should review and update this page with their planned papers.