Dafny雜記

導航：首頁 > 程式語言、邏輯學> Dafny雜記

安裝

1. Ubuntu 系Linux：先灌 .NET 6.0 sudo apt install dotnet-sdk-6.0
2. 下載最新版本，解壓縮 (unzip) 後，dafny/dafny 就是執行檔了。

• 註：這東西打包到 appimage 失敗。可能不適合用 appimage 打包成獨立程式檔。

測試

Hello World

hello.dfy

method Main(){ // 記得大寫
    var a := 1 + 1; // 局域變數用 := 設定值
    print "Hello，汝好\n";
    assert a == 2; // 斷言 a == 2，編譯會過
}

編譯並執行：

dafny/dafny /compile:3 /path/to/hello.dfy

（其中/compile:1 變成 /compile:1是純編譯）

編譯結果，沒有錯誤：

$ dafny/dafny /compile:3 /path/to/hello/a.dfy

Dafny program verifier finished with 1 verified, 0 errors
Compiled assembly into a.dll
Running...

Hello，汝好