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，汝好

Án-tsuánn 用 Dafny 做驗證？

通常驗證tsit 段程式，ē當用 Hoare 邏輯來驗證（通參考中央研究院ê FLOLAC投影片）。若是驗證一段（tsi̍t tsuā以上）ê程式P，著知影precondition（執行進前ê條件）、postsondition（執行了後ê情況，寫做：

{PreCondition}{P}{PostCondition}

例：

{x == old(x)}{x := x + 1}{x > old(x)}

其中，x == old(x) 是 P ê Precondition，PostCondition sī x > old(x)。

Tsit pîng無講siūnn tsē，只是tsit ê輔助：dafny 驗證ê時陣，著先指定下kha三項假設，koh請程式驗證正確無：

1. Precondition
2. Costcondition
3. Loop Invariant（循環無變式）：逐kái執行loop，tī tsit ê loop ê「逐位」lóng無變ê表達式。虛擬碼ê例：for (var i=0 to 4){print(i);};，i<=4 & i>=0就是 loop invatriant。

例：

/* add1ToN(n) = 1 + 2 + ... + n, n>0 */
method add1ToN(n : nat) returns (res: nat) //n : input value; res : return value
    requires n > 0 // define the precondition
    ensures res > res - 10// define the  postcondition
{
    res := 0;
    var i : nat := 1; // the item of while

    // loop
    while (i < n)
    // set the invariant of the loop
    /* bacause when i = n-1 into the loop, it'll become n after Flag A.
    so the invariant is "1 <= i <= n" */
        invariant 1 <= i <= n 

        // the loop expression n-i is decreasing
        decreases n-i
        {
            res := res + i;
            i := i + 1; // Flag A

        }

    res := res + n;

    return res; // return x

}

參考

• https://dafny.org/dafny/OnlineTutorial
• https://dafny.org/dafny/Installation
• Tutorial: Making a start in Dafny by Albert Nymeyer