Skip to content

Latest commit

 

History

History
139 lines (115 loc) · 6.16 KB

README.md

File metadata and controls

139 lines (115 loc) · 6.16 KB
Raw

Dafny Examples ⬆

Dafny project Directory examples\ contains Dafny code examples coming from various websites - mostly from the Dafny project.
It also includes build scripts (Bash scripts, batch files, Make scripts) for experimenting with Dafny on a Windows machine.

Fibonacci

This example has the following directory structure :

> tree /f /a . | findstr /v /b [A-Z]
|   build.bat
|   build.sh
\---src
        Fib.dfy

Command build.bat-verbose clean run 1 generates and executes the Dafny program target\Fib.exe :

> build -verbose clean run
Delete directory "target"
Build Dafny program "target\Fib.exe"

Dafny program verifier finished with 3 verified, 0 errors
Execute Dafny program "target\Fib.exe"
fib(10)=55

Note: The Dafny command can generate several targets besides the native executable presented above. Command option --target <name>

Name Target language PATH at build time
cs C#
js JavaScript
go Go + %GOROOT%\bin;%GOBIN% 2
java Java + %JAVA_HOME%\bin
py Python
cpp C++
lib Dafny Library (.doo)
rs Rust
dfy ResolvedDesugaredExecutableDafny

For instance, we generate the file target\Fib.jar when targetting Java :

> build -debug -target:java clean run
[build] Options    : _TARGET=java _VERBOSE=0
[build] Subcommands:  clean compile run
[build] Variables  : "DAFNY_HOME=C:\opt\dafny"
[build] Variables  : "GIT_HOME=C:\opt\Git"
[build] Variables  : "JAVA_HOME=C:\opt\jdk-temurin-17.0.10_7"
[build] rmdir /s /q "F:\examples\Fibonacci\target"
[build] "%DAFNY_HOME%\dafny.exe" build --target java --output  "F:\examples\Fibonacci\target\Fib.jar"  "F:\examples\Fibonacci\src\Fib.dfy"
Dafny program verifier finished with 3 verified, 0 errors
[build] "%JAVA_HOME%\bin\java.exe" -jar "F:\examples\Fibonacci\target\Fib.jar"
fib(10)=55
[build] _EXITCODE=0

GettingStarted

This example has the following directory structure :

> tree /f /a . | findstr /v /b [A-Z]
|   00download.txt
|   build.bat
|   build.sh
\---src
        GettingStarted.dfy

Command build.bat-verbose clean run generates and executes the Dafny program target\GettingStarted.exe:

> build -verbose clean run
Delete directory "target"
Build Dafny program "target\GettingStarted.exe"

Dafny program verifier finished with 2 verified, 0 errors
Execute Dafny program "target\GettingStarted.exe"
GettingStarted: Abs(-3)=3

Footnotes ▴

[1] Missing .NET Framework 6 ↩

> 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] Missing goimports command ↩

> where go
C:\opt\go\bin\go.exe
 
> go install golang.org/x/tools/cmd/goimports@latest
go: downloading golang.org/x/tools v0.26.0
go: downloading golang.org/x/mod v0.21.0
go: downloading golang.org/x/sync v0.8.0

mics/December 2024 ▲