fact: Definition heapsort_spec := DECLARE _heapsort WITH sh : share, arr : val, arr_contents : list (reptype t_struct_edge) PRE [tptr t_struct_edge, tint] PROP (readable_share sh; writable_share sh; 0 <= Zlength arr_contents <= Int.max_signed; Forall def_wedgerep arr_contents) PARAMS (arr; Vint (Int.repr (Zlength arr_contents))) GLOBALS () SEP (data_at sh (tarray t_struct_edge (Zlength arr_contents)) arr_contents arr) POST [tvoid] EX arr_contents' : list (reptype t_struct_edge), PROP (Permutation arr_contents arr_contents'; forall i j, 0 <= i -> i <= j -> j < Zlength arr_contents' -> wedge_le (Znth i arr_contents') (Znth j arr_contents')) LOCAL () SEP (data_at sh (tarray t_struct_edge (Zlength arr_contents')) arr_contents' arr).
imports: CertiGraph.unionfind.env_unionfind_arr CertiGraph.unionfind.uf_arr_specs VST.floyd.library RelationClasses CertiGraph.binheap.binary_heap_model CertiGraph.binheap.binary_heap_Zmodel Sorting CertiGraph.kruskal.WeightedEdgeListGraph CertiGraph.kruskal.env_kruskal_edgelist CertiGraph.kruskal.spatial_wedgearray_graph CertiGraph.graph.graph_model CertiGraph.floyd_ext.share