Я пишу HeapInsert в Dafny, но не могу доказать правильность кода.
Пробовал писать по такому алгоритму: Я использую этот алгоритм:
heap_size++;
int i = heap_size - 1;
harr[i] = k;
while (i != 0 && harr[parent(i)] <= harr[i])
{
swap(&harr[i], &harr[parent(i)]);
i = parent(i);
}
но я понятия не имею, что такое инвариант цикла, и доказать это довольно сложно.
Мне нужно написать HeapInsert в dafny со спецификациями и доказательством.
Спасибо за ответ, я закодировал родителя следующим образом: метод Parent(i: nat) возвращает (k: nat) { return (i-1)/2; }
Мне нужно доказать все от начала до конца, это заданная спецификация: метод HeapInsert(a: array<int>, heapsize: nat, x: int) требует heapsize < a.Length требует hp(a[..] , heapsize) гарантирует, что hp(a[..], heapsize+1) гарантирует, что multiset(a[..heapsize+1]) == multiset(old(a[..heapsize])+[x]) изменяет
не могли бы вы отредактировать вопрос, включив в него спецификацию и код, который у вас есть? например, &
недействителен Dafny, поэтому код, который у вас есть в вопросе, больше похож на псевдо-C, чем на Dafny. это мешает вам помочь.
Вы можете прояснить вопрос, показав нам, что у вас есть на данный момент в Дафни? например, как вы кодируете
parent
? какие свойства кода вы хотите доказать?