Oscar Slotosch Refinements in HOLCF: Implementation of Interactive Systems

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.