|Date||21 May 2023, 12:00 CEST|
|Participants||TO, KP, HDM Minutes by HDM|
Closed #49 and #50.
We need some experts to check the added RM50 Tord modifications. The changes are available for experimentation in the “maximal” branch of VDMJ. Please follow Nick guidance here.
Released a new major version Firenze based on the new release of Pharo 11.
Currently the implementation of AST is being refactored so that AST-level analysis will be easily implemented later.
VDMJ has an experimental “QuickCheck” plugin (development branch) that attempts to disprove proof obligations by direct evaluation, giving a counterexample if it can. For example here checking 7 POs from a small spec, failing on the last one (because 4 does not meet the invariant of T):
> qc Expanding 2 ranges: .. Ranges expanded in 0.049s PO# 1, PASSED in 0.018s PO# 2, PASSED in 0.001s PO# 3, PASSED in 0.001s PO# 4, PASSED in 0.0s PO# 5, PASSED in 0.002s PO# 6, PASSED in 0.003s PO# 7, FAILED in 0.008s: Counterexample: a = 4 f: subtype obligation in 'DEFAULT' (test.vdm) at line 9:5 (forall a:T & inv_T((if (a = 0) then 1 else (a * f((a - 1))))) and (is_nat((if (a = 0) then 1 else (a * f((a - 1))))))) >
The QuickCheck plugin is available for VSCode too, but is only a command line tool. Once this feature is stable or useful, it should be integrated with the VSCode client and POG “view”, with updates to the SLSP protocol to support it.
We agreed on a community effort, where members should open issues and make corrections by making pull requests that should later be considered in the next core meeting. Issues Please make a note on the issue/pull request in case a simple deletion of outdated content is not enough. We will consider those in the core meeting to evaluate whether we should make a new version of the material.
See download stats on number of installs.
Planning to have a rolling deadline to have journal first submissions… Hugo to make a call for papers for OVT-22.
Also see Planned Publications.
It was agreed that people should review and update this page with their planned papers.