dafny : 微軟推出的形式化驗證語言
dafny是一種可驗證的程式語言，由微軟推出，現已經開源。
dafny能夠自我驗證，可以在VS Code中進行開發，在編輯演算法時，寫好前置條件和後置條件，dafny驗證器就能實時驗證演算法是否正確。
在官方的例子中，以Abs絕對值函數來進行說明，程式碼如下：
點擊查看程式碼
method Abs(x: int) returns(y: int)
ensures y >= 0 && (|| y == x || y == -x)
{
return if x > 0 then x else -x;
}
Abs是方法名，x為形參，類型為int， y為返回值，類型為int。
Abs沒有前置條件，只有一個後置條件ensures y >= 0 && (|| y == x || y == -x)，這樣Abs返回值必須非負且y = x 或者 y = -x，定義了Abs的規約條件。
方法內就是具體的演算法，根據x與0的比較，返回不同的值。
dafny語言裡面有一個非常重要的後置條件寫法，那就是loop。
下面舉一個例子：
Verify the program in Algorithm 1. Note that you cannot change the existing implementation.
Algorithm 1 Find an element in array
點擊查看程式碼
method Find(a: array<int>, v: int) returns(index: int)
ensures 0 <= index ==> index < a.Length && a[index] == v
ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != v
{
var i : int := 0;
while i < a.Length
invariant 0 <= i <= a.Length
invariant forall k :: 0 <= k < i ==> a[k] != v
{
if a[i] == v {
return i;
}
i := i + 1;
}
return -1;
}
這個演算法是要找數組裡面的某個數，找到了就返回下標，否則返回-1。
這個演算法有兩個後置條件，分比對應找到了目標值和沒有找到目標值，
找到了目標值，返回為非負值，返回值必須小於數組長度且數組對應值與目標值相等。
ensures 0 <= index ==> index < a.Length && a[index] == v
沒有找到目標值，返回為負值，這就意味著數組裡的所有值與目標值都不相等。
ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != v
這種寫法用了形式化語言進行了規約。
演算法實現很簡單，while循環需要增加後置條件，
一個是i的範圍，i的初值為0，循環退出時，i的值為數組長度。
invariant 0 <= i <= a.Length
while循環的另外一個後置條件，對於i，數組i前面的數字都與目標值不相等。
invariant forall k :: 0 <= k < i ==> a[k] != v
while循環第二個後置條件，保障了Find函數第二個後置條件。
vscode的編輯器能實時驗證演算法是否正確，這對於編寫dafny程式碼十分有利。
