fact: Definition dijkstra_spec := DECLARE _dijkstra WITH sh: rshare, g: DijkGG, graph_ptr : pointer_val, addresses : list val, dist_ptr : pointer_val, prev_ptr : pointer_val, src : V PRE [tptr (tptr tint), tint, tptr tint, tptr tint, tint, tint] PROP (vvalid g src; 12 * size <= Int.max_unsigned; connected_dir g src) PARAMS (pointer_val_val graph_ptr; Vint (Int.repr src); pointer_val_val dist_ptr; pointer_val_val prev_ptr; Vint (Int.repr size); Vint (Int.repr inf)) GLOBALS () SEP (@SpaceAdjMatGraph size CompSpecs sh id g (pointer_val_val graph_ptr) addresses; data_at_ Tsh (tarray tint size) (pointer_val_val dist_ptr); data_at_ Tsh (tarray tint size) (pointer_val_val prev_ptr)) POST [tvoid] EX prev: list V, EX dist: list V, PROP (forall dst, vvalid g dst -> @inv_popped size inf g src (VList g) prev dist dst) LOCAL () SEP (@SpaceAdjMatGraph size CompSpecs sh id g (pointer_val_val graph_ptr) addresses; data_at Tsh (tarray tint size) (map Vint (map Int.repr prev)) (pointer_val_val prev_ptr); data_at Tsh (tarray tint size) (map Vint (map Int.repr dist)) (pointer_val_val dist_ptr)).
imports: CertiGraph.graph.SpaceAdjMatGraph1 CertiGraph.dijkstra.dijkstra_env CertiGraph.binheap.binary_heap_malloc_spec CertiGraph.binheap.spec_binary_heap_pro CertiGraph.dijkstra.MathDijkGraph CertiGraph.dijkstra.dijkstra_spec_pure CertiGraph.dijkstra.dijkstra1