Oscar SlotoschRefinements in HOLCF: Implementation of Interactive Systems
Forschungsergebnisse zur Informatik, Band 32
Hamburg 1997, 296 Seiten
ISBN 978-3-86064-625-0 (Print)
Zum Inhalt
Verfeinerung (Refinement) ist ein Konzept zur mathematischen Modellierung von Software und Systementwicklung. Dabei werden die Softwaresysteme in einer Logik formal beschrieben und durch die Verfeinerungsrelation in Beziehung gesetzt. Mit Verfeinerungen läßt sich die Korrektheit von Systemen bezüglich einer Spezifikation beweisen. Es gibt unterschiedliche Verfeinerungsbegriffe für unterschiedliche Entwicklungsmethoden und unterschiedliche Logiken.
HOLCF ist eine Logik höherer Stufe, die es erlaubt berechenbare Funktionen wie in LCF darzustellen. HOLCF eignet sich besonders gut für die Modellierung verteilter und Interaktiver Systeme. Mathematisch gesehen ist HOLCF eine konservative und damit korrekte Erweiterung von HOL um die Bereichskonzepte von LCF. HOLCF ist im Beweissystem Isabelle realisiert und steht damit als Tool für die Korrektheitsbeweise von Softwareentwicklungen zur Verfügung.
Die Implementierung ist eine spezielle, besonders schwierige Verfeinungsrelation, die es erlaubt Softwaresysteme mit unterschiedlichen Schnittstellen gemeinsam zu entwickeln. Technisch gesehen besteht die Implementierung aus Subtyping und Quotienten.
Schlagworte
Beweissystem IsabelleHOLCFInformatikKorrektheitQuotientenRefinementSubtypenVerfeinerungVerifikationIhr Werk im Verlag Dr. Kovač
Möchten Sie Ihre wissenschaftliche Arbeit publizieren? Erfahren Sie mehr über unsere günstigen Konditionen und unseren Service für Autorinnen und Autoren.
Weiteres Buch des Autors
Oscar SlotoschAnalogieschlüsse beim automatischen Beweisen
Hamburg 1992, ISBN 978-3-86064-006-7 (Print)