Important note: This is an experimental fork of the official Motoko VS Code extension. Please disable the official extension if you run into any unexpected behavior.
Motoko-san
Background
Motoko is a high-level smart contract language for the Internet Computer.
This extension makes it possible to write code specifications (such as actor-level invariants) for Motoko programs. The assertions are automatically checked, at compile time, by Viper Viper, a formal verifier developed at ETH Zurich.
Usage
To enable formal verification, insert // @verify at the top of your Motoko file.
Example
// @verify
actor {
var claimed = false;
var count = 0 : Int;
assert:invariant count == 0 or count == 1;
assert:invariant not claimed implies count == 0;
public shared func claim() : async () {
if (not claimed) {
claimed := true;
await async {
assert:1:async (claimed and count == 0);
count += 1;
};
};
};
}
Building from Source
- Clone vscode-motoko with
following command:
git clone https://github.com/dfinity/vscode-motoko -b viper --recurse-submodules
- In your terminal, run
cd vscode-motoko
- Install the
npm modules needed as dependencies: npm install
- Run
npm run package (this will rebuild the compiler bindings)
- Right-click the generated
/motoko-viper-*.vsix file and select "Install extension VSIX"
Tracking dfinity/motoko
The submodule motoko usually tracks the master branch of the official Motoko repo
and needs periodical updates here to adjust the pin in order to absorb features and bugfixes.
Execute the following commands from toplevel to obtain updates:
git branch --show-current
git submodule update --remote
git diff
git commit -am 'track `motoko` ToT'
git push
Further reading
A more detailed overview of Motoko-san is available here.
