Abstract
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 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
W. Ahrendt, T. Baar, B. Beckert, M. Giese, E. Habermalz, R. Hähnle, W. Menzel, and P. H. Schmitt. The KeY approach: Integrating object oriented design and formal verification. In M. Ojeda-Aciego, I. P. de Guzman, G. Brewka, and L. M. Pereira, editors, Proceedings, Logics in Artificial Intelligence (JELIA), Malaga, Spain, LNCS 1919. Springer, 2000.
K. R. Apt.Ten years of Hoare logic: A survey-part I. ACM Transactions on Programming Languages and Systems, 1981.
B. Beckert. A Dynamic Logic for the formal verification of Java Card programs. In Proceedings, Java Card Workshop (JCW), Cannes, France, LNCS 2014. Springer, 2001.
D. Harel. First-order Dynamic Logic. LNCS 68. Springer, 1979.
D. Harel. Dynamic Logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, Volume II: Extensions of Classical Logic. Reidel, 1984.
D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. MIT Press, 2000.
M. Heisel, W. Reif, and W. Stephan. A Dynamic Logic for program verification. In A. Meyer and M. Taitslin, editors, Proceedings, Logic at Botic, Pereslavl-Zalessky, Russia, LNCS 363. Springer, 1989.
D. Hutter, B. Langenstein, C. Sengler, J. H. Siekmann, and W. Stephan. Deduction in the Verification Support Environment (VSE). In M.-C. Gaudel and J. Woodcock, editors, Proceedings, International Symposium of Formal Methods Europe (FME), Oxford, UK, LNCS 1051. Springer, 1996.
D. Kozen and J. Tiuryn. Logic of programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 14, pages 89–133. Elsevier, 1990.
V. R. Pratt. Semantical considerations on Floyd-Hoare logic. In Proceedings, 18th IEEE Symposium on Foundation of Computer Science, pages 109–121, 1977.
V. R. Pratt. Process logic: Preliminary report. In Proceedings, ACM Symposium on Principles of Programming Languages (POPL), San Antonio/TX, USA, 1979.
W. Reif. The KIV-approach to software verification. In M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software-Final Report, LNCS 1009. Springer, 1995.
S. Schlager. Erweiterung der Dynamischen Logik um temporallogische Operatoren. Studienarbeit, Fakultät für Informatik, Universität Karlsruhe, 2000. In German. Available at: ftp://i12ftp.ira.uka.de/pub/beckert/schlager.ps.gz.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beckert, B., Schlager, S. (2001). A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_51
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_51
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive