fact: Definition pq_edit_priority_spec := DECLARE _pq_edit_priority WITH pq : val, h : heap, key : Z, newpri : int PRE [tptr t_pq, tint, tint] PROP (In key (proj_keys h)) PARAMS (pq; Vint (Int.repr (key)); Vint newpri) GLOBALS () SEP (valid_pq pq h) POST [tvoid] EX h': heap, PROP (Permutation (heap_items h') (update_pri_by_key (heap_items h) key newpri); heap_capacity h' = heap_capacity h) LOCAL () SEP (valid_pq pq h').
imports: VST.floyd.proofauto CertiGraph.binheap.binary_heap_Zmodel CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.env_binary_heap_pro