pred binomial-heap (Loc arg0) = ite(arg0 = nil, true, ((order arg0) >= 0) & (binomial-tree arg0) & (binomial-heap (sibling arg0)) & ((order arg0) > (order (sibling arg0))) ) pred binomial-tree (Loc arg0) = ite(arg0 = nil, ((order arg0) = 0), (binomial-heap (children arg0)) & (full-list (children arg0)) & ((order arg0) > 0) & ((order arg0) = ((order (children arg0)) + 1)) & ((msingleton (key arg0)) <=m (keys (children arg0))) ) pred full-list (Loc arg0) = ite(arg0 = nil, true, (full-list (sibling arg0)) & ((order arg0) = ((order (sibling arg0)) + 1)) ) mset keys (Loc arg0) = ite(arg0 = nil, emptymset, (((msingleton (key arg0)) Um (keys (children arg0))) Um (keys (sibling arg0))) ) Loc find-minimum(Lox x) { @ requires binomial-heap(x) & x =/= NIL @ ensures result =/= NIL & binomial-heap(result.sibling) & binomial-tree(result) & keys(result) = old_keys(x) & {result.key} <= keys(result) & (result.sibling = x | result.sibling = x.old_sibling) if (x.sibling = NIL) return x; else { Loc y := find-minimum(x.sibling); if (x.key <= y.key) { return x; } else { x.sibling := y.sibling; y.sibling := x; return y; } } } Loc merge(Loc x, Log y) { @ requires binomial-heap(x) & binomial-heap(y) @ ensures binomial-heap(result) & keys(result) = old_keys(x) U old_keys(y) & ((x.order = y.order & x=/=NIL & result.order=x.order) | (x.order = y.order & x.order=NIL & result.order=x.order+1) | (x.order =/= y.order & result.order = max(x.order,y.order)) | (x.order =/= y.order & result.order = max(x.order,y.order)) + 1 ) if (x = NIL) return y; else if (y = NIL) return x; else if (x.order = y.order) { Loc z := merge(x.sibling, y.sibling); if (x.key <= y.key) { y.sibling := x.children; x.children := y; x.sibling := z; x.order := x.order + 1; return x; } else { x.sibling := y.children; y.children := x; y.sibling := z; y.order := y.order + 1; return y; } } else if (x.order > y.order) { Loc z := merge(x.sibling, y); if (x.order = z.order & z.key <= x.key) { x.sibling := z.children; z.children := x; z.order := z.order + 1; return z; } else if (x.order = z.order & z.key > x.key) { x.sibling := z.sibling; z.sibling := x.children; x.children := z; x.order := x.order + 1; return x; } else { x.sibling := z; return x; } } else { Loc z := merge(y.sibling, x); if (y.order = z.order & z.key <= y.key) { y.sibling := z.children; z.children := y; z.order := z.order + 1; return z; } else if (y.order = z.order & z.key > y.key) { y.sibling := z.sibling; z.sibling := y.children; y.children := z; y.order := y.order + 1; return y; } else { y.sibling := z; return y; } } } Loc delete-minimum(Lox x) { @ requires binomial-heap(x) & x =/= NIL @ ensures binomial-heap(result) & old_keys(x) - keys(result) <= old_keys(x) & old_keys(x) - keys(result) =/= emptyset Loc y := find-minimum(x); return merge(y.children, y.sibling); }