A Sequent Calculus for First-order Dynamic Logic with Trace Modalities
Bernhard Beckert and Steffen Schlager
The modalities of Dynamic Logic refer to the final state of a program
execution and allow to specify programs with pre- and post-conditions.
In this paper, we extend Dynamic Logic with additional trace modalities
"throughout" and "at least once", which refer to all the states a
program reaches. They allow to specify and verify invariants and safety
constraints that have to be valid throughout the execution of a program.
We give a sound and (relatively) complete sequent calculus for this
extended Dynamic Logic.