: Refinements in HOLCF: Implementation of Interactive Systems

Refinements in HOLCF: Implementation of Interactive Systems

Forschungsergebnisse zur Informatik, Band 32

Hamburg , 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.

Ihr Werk im Verlag Dr. Kovač

Bibliothek, Bücher, Monitore

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

: Analogieschlüsse beim automatischen Beweisen

Analogieschlüsse beim automatischen Beweisen

Hamburg , ISBN 978-3-86064-006-7 (Print)

Nach oben ▲