Вопрос о моем Дафном коде о сортировке вставок - PullRequest
Новая
       14

Вопрос о моем Дафном коде о сортировке вставок

0 голосов
/ 29 февраля 2020 
predicate perm(a:array?<int>, b:array?<int>)
    requires a != null && b != null
    reads a,b
{
    multiset(a[..]) == multiset(b[..])
}

predicate sorted(a:array?<int>, min:int, max:int)
    requires a != null
    requires 0 <= min <= max <= a.Length 
    reads a
{
    forall i,j | min <= i < j < max :: a[i] <= a[j] 
}
method sort(a:array?<int>)
    requires a != null
    requires a.Length >= 1
    modifies a
    ensures perm(a,old(a))
    ensures sorted(a, 0, a.Length)

{
    var i := 1;
    while i < a.Length 
        invariant perm(a,old(a))
        invariant 1 <= i <= a.Length
        invariant sorted(a, 0, i)       
        decreases a.Length-i
    {
        var j := i;

        while j > 0 && a[j-1] > a[j] 
            invariant perm(a,old(a))
            invariant 1 <= i <= a.Length-1
            invariant 0 <= j <= i
            invariant sorted(a,0,j)
            invariant sorted(a,j,i+1) //MIGHT NOT BE MAINTAINED IF I REMOVE THE NEXT INVARIANT
            invariant forall m,n | 0 <= m < j < n <= i :: a[m] <= a[n]
            decreases j
        {
            a[j], a[j-1] := a[j-1], a[j];
            j := j-1;
        }
        i := i+1;
    }
}

Я просто новый ученик. Я не могу найти ошибку в моем текущем коде. И я не знаю, как express подробно описать мою ошибку.

Кто-нибудь может мне помочь, пожалуйста?

(Пожалуйста, пропустите мою китайскую аннотацию. Мне нужно заранее в следующий вторник, ах!)

...