fact: Definition find_spec := DECLARE _find WITH sh: share, g: UFGraph, subsets: pointer_val, i: Z PRE [tptr vertex_type, tint] PROP (writable_share sh; vvalid g i) PARAMS (pointer_val_val subsets; Vint (Int.repr i)) GLOBALS () SEP (whole_graph sh g subsets) POST [tint] EX g': UFGraph, EX rt: Z, PROP (uf_equiv g g' ; uf_root g' i rt) LOCAL (temp ret_temp (Vint (Int.repr rt))) SEP (whole_graph sh g' subsets).
imports: CertiGraph.unionfind.env_unionfind_arr CertiGraph.graph.graph_model CertiGraph.graph.UnionFind CertiGraph.msl_application.ArrayGraph CertiGraph.floyd_ext.share VST.floyd.library CertiGraph.unionfind.spatial_array_graph