本文共 1371 字，大约阅读时间需要 4 分钟。

2018.4.31

method Heapify(a: array
   
    )                              modifies a;                              requires a != null;                              requires a.Length > 0;                              ensures heap(a, a.Length - 1);                              ensures multiset(a[..]) == multiset(old(a[..]));                            {
                                 var i := 1;                                                          while (i < a.Length)                              invariant 0 < i <= a.Length;                              invariant heap(a, i - 1);                              invariant multiset(a[..]) == multiset(old(a[..]));                              {
                                   var j := i;                                                            while (j > 0 && a[(j - 1) / 2] < a[j]) // Bubble up                                invariant 0 <= j <= i;                                invariant heapExceptJParent(a, i, j);                                invariant multiset(a[..]) == multiset(old(a[..]));                                {
                                     Swap(a, (j - 1) / 2, j);                                  j := (j - 1) / 2;                                }                                                            i := i + 1;                              }                            }
   

转载地址：http://clwai.baihongyu.com/