Automatic Validation of Transformation Rules for Java Verification
against a Rewriting Semantics

Wolfgang Ahrendt, Andreas Roth, and Ralf Sasse

This paper presents a methodology for automatically validating program
transformation rules that are part of a calculus for Java source code
verification. We target the Java Dynamic Logic calculus which is
implemented in the interactive prover of the KeY system. As a basis
for validation, we take an existing SOS style rewriting logic
semantics for Java, formalized in the input language of the Maude
system. That semantics is `lifted' to cope with schematic programs
like the ones appearing in program transformation rules. The rewriting
theory is further extended to generate valid initial states for
involved program fragments, and to check the final states for
equivalence. The result is used in frequent validation runs over the
relevant fragment of the calculus in the KeY system.