Repository of various VDM-SL developments.
- Colleciton of interesting VDM-SL experiments.
- Collection of manually translated VDM-SL to Isabelle/HOL.
- Collection of minimal examples highlighting tool issues/errors.
- Reported to and fixed by corresponding tool builders.
- Overture code generator issues.
- Overture / VDMJ type checker (and occasionally parsing) issues.
- VSCode LSP related issues.
- Collection of VDMJ scripts useful for seemless VDMJ updates.
- Works for Linux/Mac (TODO: adapt for Windows!).
Repository of VDMJ plugins. Under the expected (latest) VDMJ version, they will run inside the VDMJ interpreter as console commands.
To build call:
mvn clean install
Collection of VDMJ annotation extensions.
VDM QuickCheck extension with strategies inspired by common patterns in Isabelle/HOL proofs for VDM-SL models.
ANTLR4 version of the VDM-SL EBNF embedded as an extension/substitution to VDMJ's native parser.
Various VDMJ plugs related to VDM-SL (VDM10) translation to Isabelle/HOL (2021-RC1), see corresponding README.MD.
vdm2isa VSCode LSP extension to enable vdm2isa within VDM-VSCode.
Various VDM-SL libraries. These are available both directly on the VDMJ command line, as well as within VSCode, if jars are in place.