Software is often not designed for formal specification using method contracts (without source refactoring). As solution, we propose dependent assertions, a generalization of method contracts. Our formalization uses the propositional dynamic logic PDL but with Dijkstra’s dynamic indices instead of programs inside modal operators. For deductive verification based on a new symbolic execution approach, we outline a sequent calculus to prove basic dependent assertions, including loop invariants. Finally, we can use any (D)PDL solver to prove modular contracts from basic dependencies and other contracts.