fact: Definition pq_insert_nc_spec := DECLARE _pq_insert_nc WITH pq : val, h : heap, priority : Z, data : int PRE [tptr t_pq, tint, tint] PROP (heap_size h < heap_capacity h) PARAMS (pq; Vint (Int.repr priority); Vint data) GLOBALS () SEP (valid_pq pq h) POST [tuint] EX h' : heap, EX key : Z, PROP (heap_capacity h = heap_capacity h'; Permutation (((key, Int.repr priority, data): heap_item) :: heap_items h) (heap_items h')) LOCAL (temp ret_temp (Vint (Int.repr key))) 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