First-Order Dynamic Logic is an extension of First-Order Predicate
Logic that enables propositions about programs to be made in a natural
way. The adherence of a program to certain properties---like
preserving invariants or compliance with pre-/postconditions---can be
translated into the statement that a particular formula of Dynamic
Logic is valid, which can be proved mechanically using
calculi. Accordingly, dealing with programs that violate a formal
specification leads to the investigation of invalid formulas. We
consider a dynamic logic for \Java\ and describe an approach for
proving formulas invalid that works by reduction to the validity
problem. Furthermore, the method allows us to derive concrete
counterexamples for validity, which could be a useful tool for
debugging programs or specifications.