-
Notifications
You must be signed in to change notification settings - Fork 26
IDE Import
This document gives instructions on how to configure a development environment for VerCors, using either Intellij IDEA or Visual Studio Code. Most VerCors developers use Intellij IDEA. Although VerCors supports Windows, MacOs and other unixen, most developers use a Linux distribution, so the development experience is tested more thoroughly on Linux.
This section describes how to install the prerequisites in more detail. The instructions after the shared setup were however tested only under these conditions:
- A fresh installation of Ubuntu 22.04
Install required dependencies:
apt install curl git openjdk-17-jdk-headless
Note that VerCors will also work with later jdks – it is not necessary to install an older one.
openjdk-17-jdk
includesopenjdk-17-jdk-headless
.
Clone the VerCors repository (~500MB):
git clone ssh://[email protected]/utwente-fmt/vercors.git
If you get an error about access rights, please ensure:
~/.ssh/id_rsa.pub
or another public key exists. If not, runssh-keygen
;- The key in
~/.ssh/id_rsa.pub
is associated to your github account. If not, visit https://github.com/settings/keys;- You have push access to the VerCors repository. If not, contact a member of the team.
You can also simply clone VerCors as read-only:
git clone https://github.com/utwente-fmt/vercors.git
Move into the repository:
cd vercors
Compile VerCors:
./mill -j 0 vercors.compile
Run an example to verify your setup works:
./bin/vct examples/concepts/arrays/array.pvl
That's it! 🥳
Yet to be written...
Yet to be written...
Install IntelliJ IDEA if you do not have it yet:
snap install --classic intellij-idea-community
Note: intellij-idea-ultimate is free for educational use. See e.g. here. It includes features that are useful to us, such as a profiler.
Tutorial
- Introduction
- Installing and Running VerCors
- Prototypical Verification Language
- Specification Syntax
- Permissions
- GPGPU Verification
- Axiomatic Data Types
- Arrays and Pointers
- Parallel Blocks
- Atomics and Locks
- Process Algebra Models
- Predicates
- Inheritance
- Exceptions & Goto
- VerCors by Error
- VeyMont
- Advanced Concepts
- Annex
- Case Studies
Developing for VerCors