Skip to main content

Rechnergestützte Programmkonstruktion und -verifikation mit formalen Regeln

  • Chapter

Zusammenfassung

Der Einsatz formaler Techniken ist die Grundlage, um einige wichtige Eigenschaften von Software systematisch erreichen zu können. Ein Ziel ist, die Konsistenz zwischen Aufgabenstellung und -lösung sicherzustellen und diese Beziehung rigoros zu demonstrieren. Konstruktion bedeutet, daß die Software — Entwicklung nach Regeln vorgenommen wird, die gleichzeitig als Beweisregeln für den Nachweis der Konsistenzbeziehung dienen. Am Ende eines Konstruktionsvorgangs liegt somit zusammen mit der Lösung ein solcher Konsistenzbeweis vor. Die Abstützung auf ein formales Regelsystem erlaubt eine mit der Lösungskonstruktion schritthaltende Kontrolle und vielfältige maschinelle Unterstützung.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Literatur

  1. Bauer, F.L., Broy, M. (Eds.): Program Construction — International Summer School, Springer-Verlag, Berlin-Heidelberg-New York, 1979

    MATH  Google Scholar 

  2. Brix, H.: System zur rechnergestützten Konstruktion und Verifikation von Programmen aus prädikatenlogischen Aufgabenstellungen, Abschlußbericht an das Bundesministerium für Forschung und Technologie, 1984

    Google Scholar 

  3. Brix, H.: “Software — Entwicklung durch Konstruktion” in: Molzberger, P., Zemanek, G.V.(Hrsg..):Software-Entwicklung: Kreativer Prozeß oder formales Problem? Berichte des German Chapter of the ACM 22, Teubner, Stuttgart, 1985, pp. 59–77

    Google Scholar 

  4. Brix, H.: “Formal specification and construction techniques for the development of programs with guaranteed properties”, Proc. 6th European Summer School on Computing Techniques in Physics, North Holland (to appear)

    Google Scholar 

  5. Dietl, A.: Beweismakros als Hilfsmittel zur Deduktion formaler Beweise in einer interaktiven Umgebung, Diplomarbeit, 1984

    Google Scholar 

  6. Dijkstra, E.W.: A Discipline of Programming, Prentice-Hall, Englewood Cliffs, 1976

    MATH  Google Scholar 

  7. Rosser, J.B.: Logic for Mathematicians, McGraw-Hill, New York, 1953

    MATH  Google Scholar 

Download references

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Brix, H., Dietl, A. (1986). Rechnergestützte Programmkonstruktion und -verifikation mit formalen Regeln. In: Schwärtzel, H. (eds) Informatik in der Praxis. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-93336-3_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-93336-3_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-93337-0

  • Online ISBN: 978-3-642-93336-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics