ART Modularisierung von Induktionsbeweisen über Gleichungsspezifikationen

  • Das System ART (ASF RRL Translation) stellt im wesentlichen eine Umgebung dar,in welcher die Modularisierbarkeit von Beweisen (Induktionsbeweisen über Gleichungs-spezifikationen) untersucht werden kann. Es wurde die bereits bestehende Spezifikati-onsprache ASF (siehe [BeHeKl89]), in welcher modularisierte Spezifikationen möglichsind, so erweitert, daß zusätzlich auch Beweisaufgaben spezifiziert werden können. Imfolgenden wird diese erweiterte Spezifikationsprache auch ASF genannt. Als Bewei-ser für die Beweisaufgaben einer Spezifikation wurde RRL (siehe [KaZh89]) gewählt.RRL kann sowohl Kommandos aus einem File abarbeiten, wie auch Sitzungsprotokolleanfertigen, mit deren Hilfe sich die Beweisverläufe und Benutzereingaben der entspre-chenden RRL-Sitzung rekonstruieren lassen. In ART kann nun eine ASF-Spezifikation,die Beweisaufgaben umfassen kann, in ein File übersetzt werden, welches von RRLabgearbeitet werden kann. Dies wird im folgenden kurz mit 'Übersetzung von ASF nach RRL' bezeichnet. Bei der Abarbeitung eines solchen Files wird von RRL ein Sit-zungsprotokoll angelegt. ART kann dieses Sitzungsprotokoll dazu heranziehen, neueErgebnisse, wie etwa den erfolgreichen Beweis einer Beweisaufgabe, zu ermitteln, umdiese Ergebnisse der ursprüngliche Spezifikation hinzuzufügen. Dies wird im folgendenkurz mit 'Rückübersetzung von RRL nach ASF' bezeichnet. Im Kern besteht ART alsoaus einer Komponente zur Übersetzung von ASF nach RRL und aus einer Komponentezur Rückübersetzung von RRL nach ASF.

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Robert Eschbach
URN (permanent link):urn:nbn:de:hbz:386-kluedo-3965
Serie (Series number):SEKI Report Working Papers (1994,3 )
Document Type:Preprint
Language of publication:German
Year of Completion:1999
Year of Publication:1999
Publishing Institute:Technische Universität Kaiserslautern
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $