A Program Logic for Handling Java Card's Transaction Mechanism
Bernhard Beckert and Wojciech Mostowski
In this paper we extend a program logic for verifying Java Card
applications by introducing a "throughout" operator that allows us to
prove "strong" invariants. Strong invariants can be used to ensure
"rip out" properties of Java Card programs (properties that are to be
maintained in case of unexpected termination of the program). Along
with introducing the "throughout" operator, we show how to handle the
Java Card transaction mechanism (and, thus, conditional assignments)
in our logic. We present sequent calculus rules for the extended
logic.