NetMeeting Default Template

Review Status of the Action List

See Net Meeting Actions

Overture Language Board Status

See associated minutes.

Status of ViennaTalk Development

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.

Status of the Overture Components

VDMJ

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?).

VSCode Extension

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.

LSP Server

The QuickCheck extension mentioned above works for VSCode too, but only via the execution console.

Release Planning

Community Development

The web appearance of VDM

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.

Overture Traffic

See download stats on number of installs.

OVT-22

Webpage created.

Publications Status and Plans

Also see Planned Publications.

It was agreed that people should review and update this page with their planned papers.

Any Other Business