Handling Java's Abrupt Termination in a Sequent Calculus for Dynamic Logic

Bernhard Beckert, Bettina Sasse


In Java, the execution of a statement can terminate abruptly (besides
terminating normally and terminating not at all). Abrupt termination
either leads to a redirection of the control flow after which the
program execution resumes (for example if an exception is caught), or
the whole program terminates abruptly (if an exception is not caught).
Within the KeY project, a Dynamic Logic for Java Card has been
developed, as well as a sequent calculus for that logic, which can be
used to verify Java Card programs. In this paper, we describe how abrupt
termination is handled in that calculus. The ideas behind the rules we
present can easily be adapted to other program logics (in particular
Hoare logic) for Java.