Imandra is both a programming language and a reasoning engine with which you can analyse and verify properties of your programs. This VSCode plugin allows you to develop files which can be analysed by Imandra, and also incorporates a specific merlin extension which provides information on underlying types and completions.
It is necessary that the Imandra installation instructions are followed in order for the asynchronous verification, and integration with Imandra-specific merlin to function properly. All the required components are installed automatically by following the instructions provided here. If you have any question about the installation or using Imandra, please ask us on our Discord server.
In order for the
This plugin provides both an interface to the Imandra reasoning engine, and also to the merlin type checker and development environment, specific to Imandra's
Please see the documentation to learn more about how to write verification goals and perform counter-example checking in Imandra.
Asynchronous verification with Imandra
As an Imandra file is edited, the plugin communicates with Imandra and updates the status of definitions, verification goals and bounded model-checking statements. Statements which are admissible receive a green Imandra icon in the left margin, and those that fail either receive a red Imandra icon - in the case of an unverfiable goal, or an instance not being found. An error is displayed for statements which are inadmissible by Imandra, such as those which cannot be shown to be terminating, or which are declared as theorems but cannot be proved. Please view the below gifs as examples of the plugin in use.
This extension provides a syntax highlighter is provided for Imandra files with extension
The merlin integration for this VSCode extension builds on the existing excellent OCaml and Reason IDE for Reason and OCaml files. It provides a mirror of the environment variables for each of the possible commands, and code actions function exactly the same as from this repository. By default, merlin uses specific readers to analyse
At present the
All code actions and commands are inherited from the OCaml and Reason IDE extension, but the behaviour of merlin is specific to Imandra.