Zusammenfassung
Ein Bindeglied zwischen Programm und Graph ist das Flußdiagramm. Es unterscheidet zwischen den einzelnen Programmschritten und dem Ablauf eines Programms. Programmiersprachliche Aspekte treten bei solcher Betrachtungsweise in den Hintergrund. Damit verschwinden viele der allein in der textlichen Darstellung von Programmen begründeten Probleme. Soweit sich hier eine programmiersprachliche Darstellung nicht umgehen läßt, verwenden wir eine sparsame Form, ohne jedoch deren Syntax formal zu definieren:
-
Hintereinanderschaltung E; F von Programmschritten,
-
Verzweigung if b then E else F fi,
-
nichtdeterministische mit den Prädikaten b und c bewachte Verzweigung ⌈ b: E ❙ c: F ⌋ zu den Programmschritten E und F, wobei im Fall b = c = true auch E ❙ F steht,
-
Schleifen while b do E od und repeat E until b,
-
Sprungbefehl goto M.
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.
Literaturhinweise
Arbib MH, Alagić S: Proof rules for gotos. Acta Informat. 11 (1979) 139–148.
Bakker JW de, Meertens LGLT: On the completeness of the inductive assertion method. J. Comput. Syst. Sci. 11 (1975) 323–357.
Berghammer R, Schmidt G: A relational view on gotos and dynamic logic. In: Schneider HI, Göttler H (eds.): Proc. 8th Conf. on Graphtheoretic Concepts in Computer Science (WG 82), Neunkirchen a. Br. (Germany), June 16–18, 1982, Hanser, München, 1982, 13–24.
Berghammer R, Zierer H: Relational algebraic semantics of deterministic and nondeterministic programs. Theoret. Comput. Sci. 43 (1986) 123–147.
Clint M, Hoare CAR: Program proving: Jumps and functions. Acta Informat. 1 (1972) 214–224.
Floyd RW: Assigning meaning to programs. In: Schwartz JT (ed.): Mathematical Aspects of Computer Science. Amer. Math. Soc. Proc. Symp. in Appl. Math. XIX 1966, Providence, R. I. 1967, 19–32.
Goguen JA: On homomorphisms, correctness, termination, unfoldrnents and equivalence of flow diagram programs. J. Comput. System Sci. 8 (1974) 333–365.
Harel D: First-order dynamic logic. Lecture Notes in Computer Science 68, Springer, Berlin, 1979.
Hoare CAR: An axiomatic basis for computer programming. Comm. ACM 12 (1969) 576–580, 583.
Manna Z: Verification of sequential programs: Temporal axiomatization. In: Broy M, Schmidt G (eds.): Theoretical foundations of programming methodology. Lecture Notes of an International Summer School at Marktoberdorf, 1981, Reidel, Dordrecht, 1982, 53–102.
Sanderson JG: A relational theory of computing. Lecture Notes in Computer Science 82, Springer, Berlin, 1980.
Schmidt G: Programme als partielle Graphen. Habil. Schrift, Techn. Univ. Miinchen, 1977.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Schmidt, G., Ströhlein, T. (1989). Programme: Korrektheit und Verifikation. In: Relationen und Graphen. Mathematik für Informatiker. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-83608-4_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-83608-4_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50304-0
Online ISBN: 978-3-642-83608-4
eBook Packages: Springer Book Archive