fact: Definition prim_spec := DECLARE _prim WITH g: G, garbage: list V, gptr : pointer_val, r: Z, parent_ptr : pointer_val, addresses : list val PRE [tptr (tptr tint), tint, tint, tint, tptr tint] PROP ( writable_share Tsh; vvalid g r; size * (4 * size) <= Int.max_signed; inf < Int.max_signed ) PARAMS ( pointer_val_val gptr; (Vint (Int.repr size)); (Vint (Int.repr inf)); (Vint (Int.repr r)); pointer_val_val parent_ptr) GLOBALS () SEP (@SpaceAdjMatGraph' size CompSpecs Tsh (@graph_to_symm_mat size g) (pointer_val_val gptr) addresses; data_at Tsh (tarray tint size) (map (fun x => Vint (Int.repr x)) garbage) (pointer_val_val parent_ptr) ) POST [ tvoid ] EX mst: G, EX fmst: FiniteGraph mst, EX parents: list V, PROP ( @minimum_spanning_forest size inf mst g; Permutation (EList mst) (map (fun v => eformat (v, Znth v parents)) (filter (fun v => Znth v parents <? size) (nat_inc_list (Z.to_nat size)))) ) RETURN () SEP (@SpaceAdjMatGraph' size CompSpecs Tsh (@graph_to_symm_mat size g) (pointer_val_val gptr) addresses; data_at Tsh (tarray tint size) (map (fun x => Vint (Int.repr x)) parents) (pointer_val_val parent_ptr) ).
imports: CertiGraph.prim.prim_env CertiGraph.priq.priq_arr_specs CertiGraph.graph.MathUAdjMatGraph CertiGraph.graph.SpaceUAdjMatGraph1 CertiGraph.prim.prim1