Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Coherence Spaces and Uniform Continuity Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

Equational Theories of Abnormal Termination Based on Kleene Algebra

verfasst von : Konstantinos Mamouras

Erschienen in: Foundations of Software Science and Computation Structures

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We study at an abstract level imperative while programs with an explicit fail operation that causes abnormal termination or irreparable failure, and a try-catch operation for error handling. There are two meaningful ways to define the semantics of such programs, depending on whether the final state of the computation can be observed upon failure or not. These two semantics give rise to different equational theories. We investigate these two theories in the abstract framework of Kleene algebra, and we propose two simple and intuitive equational axiomatizations. We prove very general conservativity results, from which we also obtain decidability and deductive completeness of each of our calculi with respect to the intended semantics.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Algebra, Coalgebra, and Minimization in Polynomial Differential Equations
Nächstes Kapitel Companions, Codensity and Causality
Literatur
1.
Aceto, L., Hennessy, M.: Termination, deadlock and divergence. In: Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1989. LNCS, vol. 442, pp. 301–318. Springer, New York (1990). doi:10.​1007/​BFb0040264 CrossRef
2.
3.
Anderson, C.J., Foster, N., Guha, A., Jeannin, J.B., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: semantic foundations for networks. In: Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014), pp. 113–126 (2014)
4.
Antimirov, V.: Partial derivatives of regular expressions and finite automaton constructions. Theor. Comput. Sci. 155(2), 291–319 (1996)MathSciNetCrossRefMATH
5.
6.
Delbianco, G.A., Nanevski, A.: Hoare-style reasoning with (algebraic) continuations. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP 2013), pp. 363–376 (2013)
7.
8.
Goncharov, S., Schröder, L., Mossakowski, T.: Kleene monads: handling iteration in a framework of generic effects. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 18–33. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-03741-2_​3 CrossRef
9.
Grathwohl, N.B.B., Kozen, D., Mamouras, K.: KAT + B! In: Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, pp. 44:1–44:10 (2014)
10.
Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284–303. Springer, Heidelberg (2000). doi:10.​1007/​3-540-46428-X_​20 CrossRef
11.
12.
Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110(2), 366–390 (1994)MathSciNetCrossRefMATH
13.
Kozen, D.: Kleene algebra with tests. Trans. Programm. Lang. Syst. 19(3), 427–443 (1997)CrossRefMATH
14.
Kozen, D.: Automata on guarded strings and applications. Matématica Contemporânea 24, 117–139 (2003)MathSciNetMATH
15.
Kozen, D.: Nonlocal flow of control and Kleene algebra with tests. In: Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008), pp. 105–117 (2008)
16.
Kozen, D.: On the coalgebraic theory of Kleene algebra with tests. Technical report, Computing and Information Science, Cornell University, March 2008
17.
Kozen, D., Mamouras, K.: Kleene algebra with equations. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014. LNCS, vol. 8573, pp. 280–292. Springer, Heidelberg (2014). doi:10.​1007/​978-3-662-43951-7_​24
18.
Kozen, D., Mamouras, K., Petrişan, D., Silva, A.: Nominal Kleene coalgebra. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 286–298. Springer, Heidelberg (2015). doi:10.​1007/​978-3-662-47666-6_​23
19.
Kozen, D., Mamouras, K., Silva, A.: Completeness and incompleteness in nominal Kleene algebra. In: Kahl, W., Winter, M., Oliveira, J.N. (eds.) RAMICS 2015. LNCS, vol. 9348, pp. 51–66. Springer, Cham (2015). doi:10.​1007/​978-3-319-24704-5_​4 CrossRef
20.
Kozen, D., Smith, F.: Kleene algebra with tests: completeness and decidability. In: Dalen, D., Bezem, M. (eds.) CSL 1996. LNCS, vol. 1258, pp. 244–259. Springer, Heidelberg (1997). doi:10.​1007/​3-540-63172-0_​43 CrossRef
21.
22.
23.
Mamouras, K.: On the Hoare theory of monadic recursion schemes. In: Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, pp. 69:1–69:10 (2014)
24.
Mamouras, K.: Extensions of Kleene algebra for program verification. Ph.D. thesis, Cornell University, Ithaca, NY, August 2015
25.
26.
Mamouras, K.: The Hoare logic of deterministic and nondeterministic monadic recursion schemes. ACM Trans. Comput. Logic (TOCL) 17(2), 13:1–13:30 (2016)MathSciNetCrossRef
27.
Mamouras, K.: Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism. Log. Methods Comput. Sci. 12(3), 1–41 (2016)MathSciNet
28.
29.
von Oheimb, D.: Hoare logic for Java in Isabelle/HOL. Concurr. Comput. Pract. Exp. 13(13), 1173–1214 (2001)CrossRefMATH
30.
Plotkin, G., Power, J.: Computational effects and operations. ENTCS 73, 149–163 (2004)MATH
31.
32.
Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: Proceedings of the 17th IEEE Annual Symposium on Foundations of Computer Science (FOCS 1976), pp. 109–121 (1976)
33.
Saabas, A., Uustalu, T.: A compositional natural semantics and Hoare logic for low-level languages. Theor. Comput. Sci. 373(3), 273–302 (2007)MathSciNetCrossRefMATH
34.
Tan, G., Appel, A.W.: A compositional logic for control flow. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 80–94. Springer, Heidelberg (2005). doi:10.​1007/​11609773_​6 CrossRef
Metadaten
Titel
Equational Theories of Abnormal Termination Based on Kleene Algebra
verfasst von
Konstantinos Mamouras
Copyright-Jahr
2017
Verlag
Springer Berlin Heidelberg
Buch
Foundations of Software Science and Computation Structures

Print ISBN: 978-3-662-54457-0

Electronic ISBN: 978-3-662-54458-7

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-662-54458-7_6

Premium Partner

    Bildnachweise