檢視 Dafny雜記的原始碼

{{Nav|程式語言、邏輯學}}

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

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

== 測試 ==

===Hello World===

hello.dfy

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


編譯並執行：

<pre>dafny/dafny /compile:3 /path/to/hello.dfy</pre>

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


編譯結果，沒有錯誤：

<pre>
$ 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，汝好
</pre>

==Án-tsuánn 用 Dafny 做驗證？==
通常驗證tsit 段程式，ē當用 Hoare 邏輯來驗證（通參考[https://flolac.iis.sinica.edu.tw/flolac12/lib/exe/flolac12.pdf 中央研究院ê FLOLAC投影片]）。若是驗證一段（tsi̍t tsuā以上）ê程式P，著知影precondition（執行進前ê條件）、postsondition（執行了後ê情況，寫做：

{PreCondition}{P}{PostCondition}


例：

<pre>{x == old(x)}{x := x + 1}{x > old(x)}</pre>

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

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

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

== 參考 ==
* https://dafny.org/dafny/Installation
* [https://www.cse.unsw.edu.au/~anymeyer/2011/refs/GettingStarted.pdf Tutorial: Making a start in Dafny] by Albert Nymeyer

[[category:資訊]]