dafny是一種可驗(yàn)證的編程語言商架，由微軟推出与纽，現(xiàn)已經(jīng)開源侣签。
dafny能夠自我驗(yàn)證塘装，可以在VS Code中進(jìn)行開發(fā)急迂，在編輯算法時(shí)，寫好前置條件和后置條件蹦肴，dafny驗(yàn)證器就能實(shí)時(shí)驗(yàn)證算法是否正確僚碎。
在官方的例子中，以Abs絕對(duì)值函數(shù)來進(jìn)行說明阴幌，代碼如下：
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沒有前置條件，只有一個(gè)后置條件ensures y >= 0 && (|| y == x || y == -x)懒闷，這樣Abs返回值必須非負(fù)且y = x 或者 y = -x十减，定義了Abs的規(guī)約條件。
方法內(nèi)就是具體的算法愤估，根據(jù)x與0的比較帮辟，返回不同的值。
dafny語言里面有一個(gè)非常重要的后置條件寫法玩焰，那就是loop由驹。
下面舉一個(gè)例子：
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;
}
這個(gè)算法是要找數(shù)組里面的某個(gè)數(shù)，找到了就返回下標(biāo)昔园，否則返回-1蔓榄。
這個(gè)算法有兩個(gè)后置條件，分比對(duì)應(yīng)找到了目標(biāo)值和沒有找到目標(biāo)值蒿赢，
找到了目標(biāo)值润樱，返回為非負(fù)值，返回值必須小于數(shù)組長度且數(shù)組對(duì)應(yīng)值與目標(biāo)值相等羡棵。
ensures 0 <= index ==> index < a.Length && a[index] == v
沒有找到目標(biāo)值壹若，返回為負(fù)值，這就意味著數(shù)組里的所有值與目標(biāo)值都不相等皂冰。
ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != v
這種寫法用了形式化語言進(jìn)行了規(guī)約店展。
算法實(shí)現(xiàn)很簡單，while循環(huán)需要增加后置條件秃流，
一個(gè)是i的范圍赂蕴，i的初值為0，循環(huán)退出時(shí)舶胀，i的值為數(shù)組長度概说。
invariant 0 <= i <= a.Length
while循環(huán)的另外一個(gè)后置條件，對(duì)于i嚣伐，數(shù)組i前面的數(shù)字都與目標(biāo)值不相等糖赔。
invariant forall k :: 0 <= k < i ==> a[k] != v
while循環(huán)第二個(gè)后置條件，保障了Find函數(shù)第二個(gè)后置條件轩端。
vscode的編輯器能實(shí)時(shí)驗(yàn)證算法是否正確放典，這對(duì)于編寫dafny代碼十分有利。
