Developer

This page is used to write down things to remember when developing the code base for VDM VS Code. The idea is to make sure that the development style stays consistent with time as other collaborators are included in the development. This is not set in stone and you are more than welcome to suggest changes, the important part is that everyone is aware of the changes.

License

For the VDM VS Code project, we use the GNU General Public License v3.0. Thus, when creating a new file remember to include the SPDX License Identifier at the top of the file, like:

// SPDX-License-Identifier: GPL-3.0-or-later

Formatting

When developing on the extension please use the Prettier - Code formatted with the settings from .vscode/settings.json. This will ensure a consistent format across all the source files of the project.

Other handy extensions to use while developing for the extension are:

• Better Comments
• Todo Tree
• Version Lens
• vscode-icons
• VS Code CSS Theme Completions (If working with styling of webviews)

Repository Management

When developing the project please create a new branch from the development branch. When you are finished with the changes, create a pull request with a description of the changes. Furthermore, all commits should be bound to an issue, to keep track of the changes and the reason for them, this is done by adding the issue number to the commit message, e.g.:

git commit -m "#94 Changed client log to console output"

When creating an issue please use the labels, as this helps organize them.

The milestones are assigned according to the priority of an issue

• Soon: Scheduled for the next release
• Soonish: Scheduled for an upcoming release
• Backlog: Not currently scheduled for any release

SLSP Development

The Specification Language Server Protocol (SLSP) protocol is meant to extend the Language Server Protocol (LSP), this means that we follow the same goal and format as they use. Therefore, protocol types and messages should be independent of the language, such that they can apply to multiple languages. Here is a link to the documentation from Microsoft on how to contribute to the LSP protocol, which we try to adhere to.

It takes careful consideration to not make the protocol VDM specific, but this is important as the SLSP protocol is meant as a step towards a unified protocol for all specification languages. More information on this can be found in our papers: Visual Studio Code VDM Support and The Specification Language Server Protocol: A Proposal for Standardised LSP Extensions.

When adding new client features that use the SLSP protocol, please follow the software design described in the design section.

GUI Testing Checklist

Before VDM-VSCode is released it must be checked that all of the basic operations of the tool are sound. The following is a check-list for testing the GUI.

• Creating projects
  • For each type: SL, PP, RT
    • File/New/Project
    • Check inclusion of libraries
  • Check creation of new files in a project
  • Check vdmignore file behaviour
  • Check delete of files in a project
• Editor
  • Check for syntax errors as you type
  • Check for type checking as you save
  • Check editor matches Outline view and Outline navigation works
  • Check problems appear in Problems view and link with editor
• Execution
  • Creation of a launcher
  • Check entry point, remote control and Console modes
  • Check generate coverage, including PDF output
  • Check runtime launch settings
  • Check output appears in Console
  • Check the RemoteControl (Conway) example project
• Debugging
  • Check the layout of the perspective
  • Create a breakpoint and check stack
  • Check single stepping, step into, step over and stop
  • Debug multi-threaded spec with breakpoints
  • Check that invariant failures trap into debugger
  • Check that deadlock traps into debugger
  • Check variable displays at breakpoint, including history counters
  • Try skip all breakpoints
  • Create some "watches" and check they are evaluated at breaks
  • Try some function, and conditional breakpoints
• Combinatorial Testing
  • Check the layout of the perspective
  • Perform a basic CT test and check results
  • Perform a large CT test and check nesting of results
  • Perform a CT test with filtering and check results
  • Debug a failed/successful test
• Proof Obligations
  • Check the layout of the perspective
  • Generate a reasonable set of POs and check display, including "cancel"
  • Check linked navigation in Editor view
  • Check QuickCheck results and navigation, including "cancel"
  • Run QuickCheck over the example suite and check for errors
• Workspace Settings
  • Check VDMTools integration
• Code Generation
  • Check basic generation works
• Miscellaneous
  • Check basic VSCode functions, like Find in Files, Search, F12, Shift-F12, type hierarchy etc.

Release Checklist

1. Update VDMJ jars based on the master and highprecision branches. Write to Nick to make sure that everything has been merged.
2. Check that the wiki is up-to-date (remember to update Usage GIFs and Settings)
3. Bump version number in package.json
4. Update CHANGELOG.md
   1. Add changes to the client from closed issues/developments
   2. Add changes from VDMJ (Ask Nick...)
5. Close fixed issues
6. Create a new .vsix file with the extension and delete the old one
   1. Run npm install -g vsce
   2. Run npm run enableWebpack
   3. Run vsce package
   4. Run npm run disableWebpack
7. Merge all changes that should be included in the release to the main branch
8. Create a release specific milestone and move the related issues
9. Create a new release on Github
   1. Create a new tag with the format vX.Y.Z, e.g. v1.3.0
   2. Target: main
   3. Write a description that links to the milestone and shows the highlights of that release
   4. Attach the .vsix file containing the extension
10. Upload the .vsix file to the VS Code marketplace

Feature Matrix

Feature	Overture	VDMJ/VDM VSCode
Syntax highlighting	X	X
Syntax check	X	X
Type check	X	X
Evaluation	X	X
Debugging	X	X
POG	X	X
Combinatorial Testing	X	X
Translate to LaTex	X	X
Translate to Word		X
Extract VDM from Word	X	X
Code completion	(x)	(x)
Template expansion	X	X
Standard library import	X	X
Go-to definition	(x)	X
Coverage display	X	X
VDM to Java	X	(x)
VDM to XMI (UML)	X
Dependency graph generation	X	X
VDM to Isabelle		(x)
VDM Example Import	X	X
Real-time log viewer for VDM-RT	X	X
Launch in VDMTools	X	X
FMU wrapper	X
VDM to C	(x)
VDM to LLVM
VDM to Python