fact: Definition adjustWeight_spec {CS: compspecs} := DECLARE _adjustWeight WITH pq: val, vertex : Z, newWeight : Z, priq_contents: list Z PRE [tint, tint, tptr tint] PROP (0 <= vertex < size; size <= Int.max_signed; @weight_inrange_priq newWeight) PARAMS (Vint (Int.repr vertex); Vint (Int.repr newWeight); pq) GLOBALS () SEP (data_at Tsh (tarray tint size) (map Vint (map Int.repr priq_contents)) pq) POST [tvoid] PROP () LOCAL () SEP (data_at Tsh (tarray tint size) (upd_Znth vertex (map Vint (map Int.repr priq_contents)) (Vint (Int.repr newWeight))) pq).
imports: VST.floyd.proofauto CertiGraph.lib.find_lemmas CertiGraph.priq.is_empty_lemmas CertiGraph.priq.priq_arr