Думаю, мне могут понадобиться дополнительные инварианты, чтобы убедить Дафни в том, что код работает. Я пробовал несколько, но не смог пройти.
method BubbleSort(arr: array<int>)
ensures forall k, k' :: 0 <= k < k' < arr.Length ==> arr[k] <= arr[k']
modifies arr
{
var i := arr.Length;
while i > 0
invariant 0 <= i <= arr.Length
// Violating the invariant next line
invariant forall k, k' :: i <= k < k' < arr.Length ==> arr[k] <= arr[k']
decreases i
{
var j := 0;
while j < i - 1
invariant 0 <= j < i
invariant forall k :: 0 <= k < j ==> arr[j] >= arr[k]
decreases i - j
{
if arr[j] > arr[j+1] {
arr[j], arr[j+1] := arr[j+1], arr[j];
}
j := j + 1;
}
i := i - 1;
}
}
Среди этих заметок я нашел этот пример проверенной пузырьковой сортировки.
https://www.cs.cmu.edu/~mfredrik/15414/lectures/17-notes.pdf
predicate sorted ( a : array <int > , l : int , u : int)
reads a
{
forall i , j :: 0 <= l <= i <= j <= u < a . Length ==> a [ i ] <= a [ j ]
}
predicate partitioned ( a : array <int > , i : int)
reads a
{
forall k , k' :: 0 <= k <= i < k' < a . Length ==> a [ k ] <= a [k']
}
method BubbleSort(a: array<int>) returns (b: array<int>)
requires a.Length!=0
modifies a
ensures sorted(a,0,a.Length-1)
{
var i:=0;
var j:=0;
var temp:=0;
var n:=a.Length;
i:=n-1;
b:=a;
while i>0
invariant i<0 ==> a.Length==0
invariant -1<=i<n
invariant sorted (a , i , a . Length -1)
invariant partitioned(a,i)
{
j:=0;
while j<i
invariant 0<=j<=i
invariant 0<=i<n
invariant sorted(a , i , a . Length -1)
invariant forall k :: 0 <= k <j ==> a[j] >= a[k]
invariant partitioned(a,i)
{ if a[j]>a[j+1]
{
temp:=a[j];
a[j]:=a[j+1];
a[j+1]:=temp;
}
j:=j+1;
}
i:=i-1;
}
b:=a;
}
Я думаю, чтобы полностью зафиксировать тот факт, что наибольшее число всплывает на каждой итерации. Как именно? Я не знаю, я мог придумать только отсортированный инвариант, и я застрял там.
Инвариант sorted(a, i, a. Length -1) должен сохраняться при уменьшении i. Инвариант partioned(a, i) гарантирует это, так как подразумевает a[i-1] <= a[i]. Причина того, что он сильнее этого, заключается в том, что иначе его инвариантность нельзя было бы доказать.
Примечание: partitioned(a, i) говорит, что a[k] <= a[l] для всех k <= i и i < l .
А вы знаете, зачем нужен
partitioned
?