This thesis is about proving the functional correctness and
incorrectness of imperative, object-oriented programs. One of the main
approaches for the first item is deductive program verification,
whereas the second item is traditionally handled by techniques like
testing. In this thesis, we show how both correctness and
incorrectness can be covered by dynamic logic for Java (a program
logic) and be handled using similar techniques. The theorem prover
KeY, which provides an implementation of dynamic logic for Java, was
used for experiments and was extended for this purpose.
We introduce the concept of taclets, which is the rule language that
is used to implement the calculus for Java dynamic logic in KeY.
Apart from a detailed introduction of the language and complete
definitions of the semantics of taclets, reasoning about the
correctness of taclets is discussed. This part of the thesis is the
most complete account on taclets so far.
The concept of updates is described, which is the central component
for performing symbolic execution in Java dynamic logic. Updates are
systematically developed as an imperative programming language that
provides the following constructs: assignments, guards, sequential
composition and bounded as well as unbounded parallel composition.
The language is equipped both with a denotational semantics and a
correct rewriting system for execution, whereby the latter is a
generalisation of the syntactic application of substitutions. The
normalisation of updates is discussed.