|03 Sep 2023, 12:00 CEST
|HDM, PGL, NB, TO, KP Minutes by HDM
See associated minutes.
Specification slicing based on the static program slicing technique is under development. A slice Slice[S, op, (v1,…,vn)] is a pruned AST of the specification S that produces the same state with regard to the state variables $v1,…,vn$ by the operation $op$. Slicing is expected to be used in the impact analysis of modification on a specification, debugging, and reading support. A major version will be released after the implementation of specification slicing is finished.
No change in VDMTools.
Many improvements made to the QuickCheck plugin for VDMJ (and VSCode console), allowing more efficient value expansions, a “random” value strategy and a “search” strategy that looks for specific expression patterns in each PO that can be turned into counterexamples. Strategies are “pluggable”, so groups can develop their own and add them to a collection.
Looked at several SMT solvers, with the intention of using them to find counterexamples for POs (or prove there are none) via a QC strategy - in particular, alt-ergo, cvc4 and cvc5 (via SMTLIB), Z3, Choco-solver, Mini-zinc and Prolog. All of them are capable of finding counterexamples for simple cases, but the “theories” supported by them are not easily capable of expressing something as rich as a VDM-SL PO, in general. It’s possible that simple cases might work though (like specs that just involve ints and linear arthmetic; useful in teaching, if not for serious use?).
There would be extension and SLSP protocol work required to enhance the PO dialog to invoke something like QuickCheck on the server and display the results in a helpful way.
The QuickCheck extension mentioned above works for VSCode too, but only via the execution console.
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.
Also see Planned Publications.
It was agreed that people should review and update this page with their planned papers.