fact: Definition Gprog : funspecs := ltac:(with_library prog [exch_spec; less_spec; swim_spec; sink_spec; pq_remove_min_nc_spec; pq_insert_nc_spec; pq_size_spec; capacity_spec; mallocN_spec; freeN_spec; pq_make_spec; pq_free_spec; pq_edit_priority_spec]).
imports: RelationClasses VST.floyd.proofauto CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel CertiGraph.binheap.binary_heap_pro CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.env_binary_heap_pro CertiGraph.binheap.spec_binary_heap_pro