Playing with Dafny on Windows

This repository gathers Dafny code examples coming from various websites. It also includes several build scripts (bash scripts, batch files, Make scripts) for experimenting with Dafny on a Windows machine.

Ada, Akka, C++, COBOL, Dart, Deno, Docker, Flix, Go, GraalVM, Haskell, Kafka, Kotlin, LLVM, Modula-2, Node.js, Rust, Scala 3, Spark, Spring, Standard ML, TruffleSqueak, WiX Toolset and Zig are other topics we are continuously monitoring.

Project dependencies

• Dafny 4.10 (release notes)
• Git 2.48 (release notes)
• Microsoft .NET 6.0 SDK¹ (release notes)

Optionally one may also install the following software:

• ConEmu 2023 (release notes)
• Dafny for Visual Studio Code 3.4 (release notes)
• Go 1.24 (release notes)
• Temurin OpenJDK 17 LTS (release notes, bug fixes, Java 17 API)
• Visual Studio Code 1.97 (release notes)

☛ Installation policy
When possible we install software from a Zip archive rather than via a Windows installer. In our case we defined C:\opt\ as the installation directory for optional software tools (in reference to the /opt/ directory on Unix).

For instance our development environment looks as follows (February 2025) ²:

C:\opt\ConEmu\                        ( 26 MB)
C:\opt\dafny\                         (135 MB)
C:\opt\Git\                           (393 MB)
C:\opt\go\                            (246 MB)
C:\opt\jdk-temurin-17.0.14_7\         (302 MB)
C:\opt\VSCode\                        (381 MB)
C:\Program Files\dotnet\sdk\6.0.428\  (329 MB)

🔎 Git for Windows provides a Bash emulation used to run git from the command line (as well as over 250 Unix commands like awk, diff, file, grep, more, mv, rmdir, sed and wc).

Directory structure ▴

This project is organized as follows:

bin\
docs\
examples\{README.md, Competition, Fibonacci, ..}
README.md
RESOURCES.md
setenv.bat

where

• directory bin\ contains utility tools.
• directory docs\ contains Dafny related documents.
• directory examples\ contains Dafny code examples (see README.md file).
• file README.md is the Markdown document for this page.
• file RESOURCES.md is the Markdown document presenting external resources.
• file setenv.bat is the batch command for setting up our environment.

Batch commands ▴

setenv.bat

We execute command setenv once to setup our development environment; it makes external tools such as git.exe and sh.exe directly available from the command prompt.

> setenv
Tool versions:
   cargo 1.84.0, rustc 1.84.0, dafny 4.10.0,
   javac 17.0.14, code 1.97.2, go 1.24.0, goimports v0.29.0,
   git 2.48.1, diff 3.10, bash 5.2.37(1)

> where git sh
C:\opt\Git\bin\git.exe
C:\opt\Git\mingw64\bin\git.exe
C:\opt\Git\bin\sh.exe
C:\opt\msys64\usr\bin\sh.exe
C:\opt\Git\usr\bin\sh.exe

Command setenv-verbose also prints :

• the tool paths.
• the environment variables defined in the current session.
• the path associations (globally defined).

> setenv -verbose
Tool versions:
   cargo 1.84.0, rustc 1.84.0, dafny 4.10.0,
   javac 17.0.14, code 1.97.2, go 1.24.0, goimports v0.29.0,
   git 2.48.1, diff 3.10, bash 5.2.37(1)
Tool paths:
   %USERPROFILE%\.cargo\bin\cargo.exe
   %USERPROFILE%\.cargo\bin\rustc.exe
   C:\opt\dafny\Dafny.exe
   C:\opt\jdk-temurin-17.0.14_7\bin\javac.exe
   C:\opt\VSCode\bin\code.cmd
   C:\opt\go\bin\go.exe
   %USERPROFILE%\go\bin\goimports.exe
   C:\opt\Git\bin\git.exe
   C:\opt\Git\usr\bin\diff.exe
   C:\opt\Git\bin\bash.exe
Environment variables:
   "CARGO_HOME=%USERPROFILE%\.cargo"
   "DAFNY_HOME=C:\opt\dafny"
   "GIT_HOME=C:\opt\Git"
   "GOBIN=%USERPROFILE%\go\bin"
   "GOPATH=C:\Users\michelou\go"
   "GOROOT=C:\opt\Go"
   "JAVA_HOME=C:\opt\jdk-temurin-17.0.14_7"
   "VSCODE_HOME=C:\opt\VSCode"
Path associations:
   G:\: => %USERPROFILE%\workspace-perso\dafny-examples

Footnotes ▴

[1] Missing .NET Framework 6 ↩

Dafny requires the Microsoft .NET Framework 6.0 to be installed; otherwise the following runtime error occurs :

> c:\opt\dafny\Dafny.exe run src\Fib.dfy
 
Dafny program verifier finished with 3 verified, 0 errors
It was not possible to find any compatible framework version
The framework 'Microsoft.NETCore.App', version '6.0.0' was not found.
  - The following frameworks were found:
      2.1.12 at [C:\Program Files\dotnet\shared\Microsoft.NETCore.App]
      2.1.13 at [C:\Program Files\dotnet\shared\Microsoft.NETCore.App]
      2.1.26 at [C:\Program Files\dotnet\shared\Microsoft.NETCore.App]
      2.1.30 at [C:\Program Files\dotnet\shared\Microsoft.NETCore.App]
      3.1.32 at [C:\Program Files\dotnet\shared\Microsoft.NETCore.App]
      5.0.17 at [C:\Program Files\dotnet\shared\Microsoft.NETCore.App]
 
You can resolve the problem by installing the specified framework and/or SDK.
 
The specified framework can be found at:
  - https://aka.ms/dotnet-core-applaunch?framework=Microsoft.NETCore.App&framework_version=6.0.0&arch=x64&rid=win10-x64

[2] Downloads ↩

In our case we downloaded the following installation files (see section 1):

dafny-4.10.0-x64-windows-2019.zip                 ( 60 MB)
dotnet-sdk-6.0.428-win-x64.exe                    (198 MB)
go1.24.0.windows-amd64.zip                        ( 70 MB)
OpenJDK17U-jdk_x64_windows_hotspot_17.0.14_7.zip  (188 MB)
PortableGit-2.48.1-64-bit.7z.exe                  ( 55 MB)
rust-init.exe                                     (  8 MB)
VSCode-win32-x64-1.97.2.zip                       (131 MB)

---

mics/February 2025 ▲