Eine reflexive Architektur zur Darstellung von Beweis- und Softwareentwicklungsschritten in Typtheorie

Zusammenfassung

Inhalt der vorliegenden Arbeit ist die Integration einer formalen Metasprache in das Spezifikations- und Verifikationssystem Typelab. Bei dem vorgestellten Ansatz wird Typelab in sich selbst kodiert. Diese Kodierung konstituiert die formale Metaebene, auf der sowohl Objekte syntaktisch manipuliert als auch Aussagen über Beweisbarkeit getroffen werden können. Die Verbindung von Objekt- und Metabene geschieht durch Erweiterung des Regelkalküls um sogenannte Reflexionsprinzipien. Die Implementierung des Typelab-Beweisers wurde durch entsprechende Befehle zur Anwendung dieser Regeln ergänzt. Dies erlaubt es, während eines Beweises beliebig zwischen Objekt- und Metaebene zu wechseln und so Metatheoreme im Ableitungsprozeß einzusetzen. Auf der Metaebene lassen sich Beweisschritte abstrakt formulieren und zu komplexen Beweisbefehlen kombinieren. Die Implementierung eines Taktikmechanismus stellt die korrekte Anwendung dieser Beweisprozeduren sicher. Durch Metafunktionen kann die Funktionalität des Typelab-Systems auf sichere Art und Weise erweitert werden. Dies wird anhand eines Metaoperators demonstriert, der aus einer Datentypbeschreibung eine umfangreiche Spezifikation des Typs, sowie die entsprechende Implementierung erzeugt. Darüber hinaus wird gezeigt, wie auf der Metaebene generisch Beweise für bestimmte Theoreme erzeugt werden können, indem Struktureigenschaften von Objekten ausgenutzt werden.

Online Kopie

Erhältlich als komprimierte Postscript-Datei (213KB).

BibTeX Eintrag

@MastersThesis{Pfe95, author = "Holger Pfeifer", title = "{Eine reflexive Architektur zur Darstellung von Beweis- und Softwareentwicklungsschritten in Typtheorie}", school = "Universit{\"a}t Ulm", year = 1995}