2018.2.29
最编程
2024-08-11 20:39:00
...
2018.2.29
predicate valid_heap(h: Heap)
reads h.a
{
h.a != null && h.a.Length == h.capacity + 1 && 0 <= h.size <= h.capacity &&
forall i :: 1 < i <= h.size ==> h.a[i] <= h.a[i / 2]
}
推荐阅读