fact: Definition unionS_spec := DECLARE _unionS WITH sh: wshare, g: UFGraph, x: pointer_val, y: pointer_val PRE [tptr (Tstruct _Node noattr), tptr (Tstruct _Node noattr)] PROP (vvalid g x; vvalid g y ; uf_under_bound g ; vlabel_in_bound g) PARAMS (pointer_val_val x; pointer_val_val y) GLOBALS () SEP (whole_graph sh g) POST [ Tvoid ] EX g': UFGraph, PROP (uf_union g x y g' ; uf_under_bound g') LOCAL() SEP (whole_graph sh g').
imports: CertiGraph.unionfind.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.unionfind.spatial_graph_glist