Реализация вставки кучи через Dafny (со спецификациями) - PullRequest
Новая
       10

Реализация вставки кучи через Dafny (со спецификациями)

0 голосов
/ 12 февраля 2019

Я пишу 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 со спецификациями и доказательствами.

...