fact: Definition find_spec := DECLARE _find WITH sh: wshare, g: Graph, x: pointer_val PRE [ _x OF (tptr (Tstruct _Node noattr))] PROP (vvalid g x) LOCAL (temp _x (pointer_val_val x)) SEP (whole_graph sh g) POST [ tptr (Tstruct _Node noattr) ] EX g': Graph, EX rt : pointer_val, PROP (findS g x g' /\ uf_root g' x rt) LOCAL (temp ret_temp (pointer_val_val rt)) SEP (whole_graph sh g').
imports: CertiGraph.sample_mark.env_unionfind CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.subgraph2 CertiGraph.graph.graph_relation CertiGraph.graph.reachable_computable CertiGraph.msl_application.Graph CertiGraph.msl_application.UnionFindGraph CertiGraph.msl_application.GList CertiGraph.msl_application.GList_UnionFind CertiGraph.floyd_ext.share CertiGraph.sample_mark.spatial_graph_glist