「Dafny雜記」修訂間的差異
跳至導覽
跳至搜尋
Tankianting（討論 | 貢獻） （建立內容為「{{Nav|程式語言、邏輯學}} == 安裝 == # Ubuntu 系Linux：先灌 .NET 6.0 <code>sudo apt install dotnet-sdk-6.0</code> # 下載最新版本，解壓縮 (…」的新頁面） |
Tankianting（討論 | 貢獻） |
||
| 行 16： | 行 16： | ||
method Main(){ // 記得大寫 | method Main(){ // 記得大寫 | ||
var a := 1 + 1; // 局域變數用 := 設定值 | var a := 1 + 1; // 局域變數用 := 設定值 | ||
print " | print "Hello，汝好\n"; | ||
assert a == 2; // 斷言 a == 2，編譯會過 | assert a == 2; // 斷言 a == 2，編譯會過 | ||
}</pre> | }</pre> | ||
| 行 28： | 行 28： | ||
編譯結果，沒有錯誤： | |||
<pre> | <pre> | ||
於 2023年8月10日 (四) 01:59 的修訂
安裝
- 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，汝好