-
Notifications
You must be signed in to change notification settings - Fork 26
Installing and Running VerCors
The installation and running instructions can be found on the Github homepage of this project.
When writing a program in PVL, the Prototypal Verification Language of VerCors, syntax highlighting can be obtained in the following way:
VerCors provides syntax highlighting support for PVL in TextMate 2 (MacOS X) and Sublime Text (Linux and Windows) as a TextMate Bundle. The bundle is located at ./util/VercorsPVL.tmbundle
. On MacOS X for TextMate 2 you can simply double click the .tmbundle
file to install it. Sublime Text requires you to copy the bundle content to some directory:
- In Sublime Text, click on the
Preferences > Browse Packages…
menu. - Create a new directory and name it
VercorsPVL
. - Move the contents of
VercorsPVL.tmbundle
(that is, the./Syntaxes
directory) into the directory you just created. - Restart Sublime Text.
Visual Studio Code (VS Code) also has support for TextMate bundles to do syntax highlighting (VS Code runs on Windows, Linux and OSX). Click here for instructions on how to install this (this has not been tested however).
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