dafny-training
Some examples of Dafny code to support training sessions
Install Dafny/VSCode
You should install the Dafny VsCode plugin.
The installer may prompt you to agree to install Dafny 3.0.0, Z3 and change some permissions.
You may configure the plugin to verify on save
only (set the Dafny plugin settings in VSCode) as otherwise live and continuous verification can alter performance.
Dafny CLI
In the session we may use the CLI (e.g. for compile/run).
You can use the Dafny executubla bundled in the plugin located
at $HOME/.vscode/extensions/correctnesslab.dafny-vscode-1.4.0/out/dafnyLanguageServer/Dafny.dll
.
To run the .dll
on non-windows system, you'll have to install dotnet
.
You can then create an alias
for dafny
alias dafny=`dotnet ../../.vscode/extensions/correctnesslab.dafny-vscode-1.4.0/out/dafnyLanguageServer/Dafny.dll`
Alternatively, you can install the Dafny 3.0.0 latest release for your system which provide a dafny
executable (the VSCode plugin also runs Dafny 3.0.0).
There is no conflict between the plugin version and another one that you install manually. The plugin configuration defaults to use the Dafny executables bundled with the plugin.
Make sure you add the path to the Dafny executable to your paths.
Checking your installation
Checking Plugin
- Clone/fork this repository.
- Open the file
training1.dfy
in session1 - The
Problems
tab should display a couple of information (decreases
and another related totriggers
). If this is the case you should be all set.
Checking CLI
In a terminal, the command dafny /help
should output something like:
% dafny -version
Dafny 3.0.0.30203
You can cd
to the sessions
directory and try the following commands:
% dafny /dafnyVerify:1 /compile:0 /trace training1.dfy
On my computer this results in (path names may differ on your system):
Parsing training1.dfy
Coalescing blocks...
Inlining...
Running abstract interpretation...
[0.060479 s]
[TRACE] Using prover: /Users/franck/local/dafny3.0.0/z3/bin/z3
Verifying Impl$$_module.__default.abs ...
[0.465 s, 1 proof obligation] verified
Verifying Impl$$_module.__default.max ...
[0.068 s, 1 proof obligation] verified
Verifying Impl$$_module.__default.ex1 ...
[0.070 s, 3 proof obligations] verified
Verifying Impl$$_module.__default.find ...
[0.070 s, 6 proof obligations] verified
Verifying CheckWellformed$$_module.__default.sorted ...
[0.067 s, 2 proof obligations] verified
Verifying Impl$$_module.__default.unique ...
[0.064 s, 1 proof obligation] verified
Verifying Impl$$_module.__default._default_Main ...
[0.076 s, 6 proof obligations] verified
Dafny program verifier finished with 7 verified, 0 errors
Note
On MacOSX, if you have manually installed the Dafny 3.0.0 release you may encounter some permission issues on MacOSX. In that case, you may have to allow several files to be executable (this is via the Security widget in the Preferences.)
Dafny Reference Manual
The current versions of the Dafny Reference Manual should be: