Formale Programmentwicklung mit dynamischer Logik
- PDF / 22,377,351 Bytes
- 296 Pages / 439.37 x 666.142 pts Page_size
- 69 Downloads / 183 Views
Maritta Heisel
Formale Programmentwicklung mit dynamischer Logik
Maritta Heisel Formale Programmentwicklung mit dynamischer Logik
Maritta Heisel
Formale Programm· entwicklung mit dynamischer Logik
Springer Fachmedien Wiesbaden GmbH
Die Deutsche Bibliothek - CIP-Einheitsaufnahme
Heisel, Maritta: Formale Programmentwicklung mit dynamischer logik 1 Moritta Heisel.- Wiesbaden: Dt. Univ.-Verl., 1992 (DUV : lnformatik} Zugl.: Karlsruhe, Univ., Diss., 1992 ISBN 978-3-8244-2031-5
Der Deutsche Universităts-Verlag ist ein Unternehmen der Verlogsgruppe Bertelsmann International.
©
Springer Fachmedien Wiesbaden 1992
UrsprOnglich erschienen bei Deutscher Universităts-Verlag GmbH, Wiesbaden 1992
Das Werk einschlieBiich aller seiner Teile ist urheberrechtlich geschOtzt. Jede Verwertung auBerhalb der engen Grenzen des Urheberrechtsgesetzes ist ohne Zustimmung des Verlags unzulassig und strafbar. Dos gilt insbesondere for Vervielfăltigungen, Obersetzungen, Mikroverfilmungen und die Einspeicherung und Verorbeitung in elektronischen Systemen.
ISBN 978-3-8244-2031-5 ISBN 978-3-663-14621-6 (eBook) DOI 10.1007/978-3-663-14621-6
Danksagungen Ich danke Herrn Prof. Dr. W. Menzel für seine Unterstützung und seine konstruktive Kritik bei der Erstellung dieser Arbeit. Auch die anregenden Diskussionen zum weiteren Umfeld des Themas haben wesentlich zum Gelingen der Arbeit beigetragen. Herrn Prof. Dr. S. Jähnieben danke ich für die Übernahme des Koreferates dieser Dissertation und seine nützlichen und ermutigenden Kommentare. Auch den Kollegen aus dem KIV-Projekt, Wolfgang Reif, Werner Stephan und Andreas Wolpers bin ich zu großem Dank verpflichtet. Die Arbeit ist aus diesem Projekt heraus entstanden und wäre ohne das so geschaffene Umfeld nicht möglich gewesen. Sie alle standen mir stets mit Rat und Tat zur Seite. Den Studierenden Martin Gelfort und Thomas Santen danke ich für die Implementierung der hier geschilderten Verfahren und ihre Anregungen zur Verbesserung des Systems. Norbert Lindenberg und Thomas Santen haben mit ihren Kommentaren zu früheren Versionen der Arbeit wesentlich zur Verbesserung der Präsentation beigetragen.
Inhalt 1 Einleitung
1
2 Bisherige Ansätze zur Programmentwicklung
5
2.1 Der Software-Engineering-Ansatz 2.2 Programmiermethodik mit formaler Grundlage 2.3 Deduktive Ansätze 2.3.1 Deduktive Programmsynthese nach Manna und Waldinger 2.3.2 Syntaxgesteuerte, semantikunterstützte Programmsynthese 2.3.3 Automatische Synthese von Skaiernfunktionen 2.3.4 Programmsynthese mit intuitionistischer Typentheorie 2.4 Transformationelle Ansätze 2.4.1 Transformation von rekursiven Programmen 2.4.2 CIP 2.4.3 Programmsynthese mit Termersetzungssystemen 2.4.4 Der Bird/Meertens-Formalismus 2.4.5 Ein informeller Ansatz 2.5 Ein problemorientierter Ansatz 2.6 Der mit der vorliegenden Arbeit verfolgte Ansatz
3 Das KIV -System als Werkzeug für die formale Programmentwicklung 3.1 Die KIV-Logik 3.1.1 Syntax 3.1.2 Semantik 3.1.3 Ein Sequenzenkalkül für die dynamische Logik 3.2 Die Metasprache PPL 3.2.1 Erzeugung von Bewe
