Skip to main content
SpringerLink
Log in

Machine-Assisted Program Construction and Modification

  • Conference paper
GWAI-89 13th German Workshop on Artificial Intelligence

Part of the book series: Informatik-Fachberichte ((2252,volume 216))

  • 112 Accesses

Zusammenfassung

In this paper we present two calculi, one for the construction of programs in the spirit of Martin-Löf, and the other for the verification of program transformations. Both are derived from a general axiomatization of Dynamic Logic and thus provide a unifying framework suitable for combining the derivation, modification and verification of programs.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bauer, F. L., Broy, M. (eds.): Program construction.LNCS, Vol. 69. Springer (1979)

    Google Scholar 

  2. Burstall, R. M., Darlington, J.: A transformation system for developing recursive programsJ. ACM 24,1 (Jan. 1977), 44–67

    Article  MathSciNet  MATH  Google Scholar 

  3. Burstall, R.M. Program Proving as Hand Simulation with a little Induction. Information Processing 74, North-Holland Publishing Company (1974)

    Google Scholar 

  4. Gordon,M/Milner,R./Wadsworth,C. Edinburgh LCF. Springer LNCS 78 (1979)

    Google Scholar 

  5. Goldblatt, R. Axiomatising the Logic of Computer Programming. Springer LNCS 130 (1982)

    MATH  Google Scholar 

  6. Gries, D. The Science of Programming, Springer-Verlag (1981)

    MATH  Google Scholar 

  7. Heisel, M. A Formalization and Implementation of Gries’s Program Development Method within the KIV Environment. Int. Bericht 3/89, Fak. für Informatik, Univ. Karlsruhe

    Google Scholar 

  8. Heisel,M./Reif, W./Stephan, W. Program Verification by Symbolic Execution and Induction. Proc. 11-th GWAI, K. Morik (ed), Informatik Fachberichte 152, Springer-Verlag (1987)

    Google Scholar 

  9. Heisel,M./Reif, W./Stephan, W. Implementing Verification Strategies in the KIV Sys-tem. Proc. 9-th CADE, E. Lusk/R. Overbeek (eds), Springer LNCS 310 (1988), pp. 131–140

    Google Scholar 

  10. Martin-Löf, P. Intuitionistic Type Theory, Bibliopolis (1984)

    MATH  Google Scholar 

  11. Manna, Z., Waldinger, R.: Is “Sometime” Sometimes Better than “Always”? Comm. ACM 21,2 (Febr. 1978), 159–172

    Google Scholar 

  12. Nordström, B. Programming in Constructive Set Theory: Some Examples. JACM (1981)

    Google Scholar 

  13. Reif, W. Vollständigkeit einer modifizierten Goldblatt-Logik und Approximation der Omegaregel durch Induktion. Diplomarbeit, Universität Karlsruhe (1984)

    Google Scholar 

  14. Stephan, W. Axiomatising Recursive Procedures in Dynamic Logic. Forthcoming (1989)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Logik, Komplexität und Deduktionssysteme, Universität Karlsruhe, Postfach 6980, D-7500, Karlsruhe, Germany

    M. Heisel, W. Reif & W. Stephan

Authors
  1. M. Heisel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. W. Reif
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. W. Stephan
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computerlinguistik, Universität Bielefeld, Postfach 8640, D-4800, Bielefeld 1, Germany

    Dieter Metzing

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Heisel, M., Reif, W., Stephan, W. (1989). Machine-Assisted Program Construction and Modification. In: Metzing, D. (eds) GWAI-89 13th German Workshop on Artificial Intelligence. Informatik-Fachberichte, vol 216. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-75100-4_39

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-75100-4_39

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51743-6

  • Online ISBN: 978-3-642-75100-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation