fact: Definition insert_nc_spec := DECLARE _insert_nc WITH pq : val, h : heap, i : val, iv : heap_item PRE [tptr t_pq, tptr t_item] PROP (heap_size h < heap_capacity h) PARAMS (pq; i) GLOBALS () SEP (valid_pq pq h; hitem iv i) POST [tvoid] EX h', PROP (heap_capacity h = heap_capacity h'; Permutation (iv :: heap_items h) (heap_items h')) LOCAL () SEP (valid_pq pq h'; hitem iv i).
imports: RelationClasses Sorting VST.floyd.proofauto CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel CertiGraph.binheap.binary_heap CertiGraph.binheap.env_binary_heap