Abstract
The modalities of Dynamic Logic refer to the final state of a program execution and allow to specify programs with pre- and postconditions. 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 one 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. © Springer-Verlag Berlin Heidelberg 2001.
Cite
CITATION STYLE
Beckert, B., & Schlager, S. (2001). A sequent calculus for first-order dynamic logic with trace modalities. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2083 LNAI, pp. 626–641). Springer Verlag. https://doi.org/10.1007/3-540-45744-5_51
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
