「Dafny雜記」修訂間的差異
跳至導覽
跳至搜尋
Tankianting（討論 | 貢獻） |
Tankianting（討論 | 貢獻） |
||
| 行 39： | 行 39： | ||
Hello，汝好 | Hello，汝好 | ||
</pre> | </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)} | |||
x == old(x) 是 P ê Precondition，PostCondition sī x > old(x)。 | |||
</pre> | |||
Tsit pîng無講siūnn tsē，只是tsit ê輔助：dafny 驗證ê時陣，著先指定下kha三項假設，koh請程式驗證正確無： | |||
# Precondition | |||
# Costcondition | |||
# Loop Invariant（循環無變式）：佇loop內底逐kái執行，無變ê表達式。虛擬碼ê例：<code>for (var i=0 to 4){print(i);};</code>，<code>i<=4 & i>=0</code>就是 loop invatriant。 | |||
== 參考 == | == 參考 == | ||
於 2023年8月10日 (四) 02:27 的修訂
安裝
- Ubuntu 系Linux：先灌 .NET 6.0
sudo apt install dotnet-sdk-6.0 - 下載最新版本，解壓縮 (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請程式驗證正確無：
- Precondition
- Costcondition
- Loop Invariant（循環無變式）：佇loop內底逐kái執行，無變ê表達式。虛擬碼ê例：
for (var i=0 to 4){print(i);};，i<=4 & i>=0就是 loop invatriant。
參考
- https://dafny.org/dafny/Installation
- Tutorial: Making a start in Dafny by Albert Nymeyer