Übersetzen von rekursiven Funktionen von VDM nach Isabelle/HOL

Dieser Artikel handelt von einer Methode zum Übersetzen rekursiver Definitionen aus einem System namens VDM in ein anderes System, das als Isabelle/HOL bekannt ist. Ziel ist es, Vorlagen zu erstellen, die viele verschiedene Arten von Definitionen in VDM automatisch verarbeiten können. Diese Methode konzentriert sich darauf, sicherzustellen, dass die Übersetzungen klar sind und so viel wie möglich des Beweisprozesses automatisiert wird.

VDM und Isabelle/HOL haben einige Unterschiede, besonders in der Art und Weise, wie sie das Konzept der Terminierung in rekursiven Funktionen handhaben. Terminierung ist wichtig, weil sie sicherstellt, dass eine Funktion nicht endlos ohne Stopp läuft. Der Artikel wird erörtern, wie wir rekursive Definitionen übersetzen können, während wir diese Unterschiede berücksichtigen.

Mit dieser Übersetzungsmethode bieten wir eine Erweiterung bestehender Werkzeuge, die Benutzern helfen, VDM-Definitionen nach Isabelle/HOL zu konvertieren. Isabelle ermöglicht es Benutzern, Spezifikationen, Beweise und Dokumentationen an einem Ort zu schreiben. Die vollständigen Details zu den Quellen und Beweisen sind in einem spezifischen Toolkit-Repository zu finden.

Die nächsten Abschnitte bieten Hintergrundinformationen zu VDM und Isabelle, gefolgt von Diskussionen über die Übersetzung grundlegender Typen, Rekursion und die allgemeine Übersetzungsstrategie.

#Hintergrund

Der Übersetzer von VDM nach Isabelle/HOL deckt eine breite Palette von Strukturen ab, die in VDM zu finden sind. Er kann verschiedene Ausdrücke, Muster, Typen und Spezifikationen in VDM verwalten. Das Ziel ist sicherzustellen, dass die meisten Muster in VDM effektiv übersetzt werden können und wenn nicht, wird es eine äquivalente Möglichkeit geben, sie darzustellen.

Ein wichtiger Fokus dieser Übersetzung liegt auf dem Umgang mit rekursiv definierten Funktionen. In VDM müssen Benutzer eine Massfunktion definieren, um sicherzustellen, dass die Rekursion terminieren wird. Diese Massfunktion generiert Beweisverpflichtungen, die Anforderungen sind, um zu bestätigen, dass die Rekursion wie beabsichtigt funktioniert.

Die verwendete Übersetzungsstrategie folgt einem spezifischen Ansatz, der als Grössenänderungs-Terminierung (SCT) bezeichnet wird. Dieser Ansatz überprüft, ob eine rekursive Funktion bewiesen werden kann, dass sie anhand der produzierten Werte terminieren wird. Wenn jede Berechnung zu einem kleineren Wert führt, kann sichergestellt werden, dass die Rekursion letztendlich stoppt.

#VDM Grundtypen in Isabelle

In Isabelle werden natürliche Zahlen als Datentyp mit zwei Teilen dargestellt: der Zahl null und einer Nachfolgerfunktion, die eins hinzufügt. Isabelle definiert auch ganze Zahlen und andere numerische Typen, indem diese natürlichen Zahlen verwendet werden. Typkonversionen sind verfügbar, um Benutzern den Übergang zwischen Typen zu erleichtern, aber es gibt keine impliziten Regeln, die Typen automatisch erweitern.

In VDM haben grundlegende Typen wie natürliche Zahlen und ganze Zahlen spezifische Erweiterungsregeln, die berücksichtigt werden müssen. Zum Beispiel, wenn beide Typen natürliche Zahlen sind, könnte das Ergebnis eine ganze Zahl sein. Unsere Übersetzungsstrategie behandelt VDM natürliche Zahlen speziell als Typ-Synonym in Isabelle, was hilft, den Prozess zu vereinfachen und die Notwendigkeit komplizierter Typumwandlungen zu vermeiden.

Das bedeutet jedoch, dass die Kodierung rekursiver Funktionen unter Verwendung natürlicher Zahlen komplexer sein kann als erwartet, da die Darstellung in Isabelle sich von der in VDM unterscheidet.

Selbst mit diesen Komplikationen findet Rekursion über ganze Zahlen, Mengen oder Karten in VDM statt, da diese Typen in Isabelle keine einfache konstruktive Definition haben.

#Rekursion in VDM und Isabelle

Jede rekursive Definition benötigt einen Weg, um zu rechtfertigen, dass sie terminieren wird. Andernfalls könnte die Rekursion in einer Endlosschleife enden. In VDM kommt diese Begründung von der rekursiven Massnahme, die die gleichen Eingaben wie die rekursive Definition annimmt und eine natürliche Zahl zurückgibt, die mit jedem rekursiven Aufruf sinken muss.

Nehmen wir als Beispiel eine einfache rekursive Funktion, die die Fakultät einer natürlichen Zahl berechnet. Die Massfunktion verwendet die Eingabe selbst, und die Rekursion stoppt, wenn diese Eingabe null erreicht. In diesem Fall generiert VDM drei Beweisverpflichtungen, die in Isabelle bestätigt werden müssen.

Isabelle hingegen ermöglicht rekursive Definitionen durch primitive Rekursion oder allgemeine Funktionsdefinitionen, die Beweisverpflichtungen erzeugen. Die Herausforderung besteht darin, sicherzustellen, dass die Parameter mit den definierten Mustern übereinstimmen und dass die rekursiven Aufrufe ordnungsgemäss terminieren.

Isabelles rekursive Funktionsdefinitionen können mit zwei Arten von Syntax ausgedrückt werden: einer, die versucht, automatisch die Terminierung zu beweisen, und einer anderen, die von den Benutzern verlangt, manuell einen Beweis der Terminierung zu liefern. Letzteres wird oft in Fällen benötigt, in denen die rekursive Funktion komplexer ist.

Die Terminierungsrelation muss auch wohlgegründet sein, was bedeutet, dass sie eine ordentliche Struktur haben muss, um sicherzustellen, dass die Rekursion terminieren wird. Diese Anforderung fügt dem Übersetzungsprozess eine weitere Schicht der Komplexität hinzu.

#VDM Rekursion Übersetzungsstrategie

Ziel der Übersetzungsstrategie ist es, die Probleme im Zusammenhang mit Rekursion über grundlegende Typen, Mengen, Sequenzen und Karten, einschliesslich gegenseitiger Rekursion, anzugehen. Wir beginnen damit, alle rekursiven Funktionen in VDM zu kennzeichnen, selbst die ohne eine explizite Massnahme, um die Übersetzung unter Verwendung von Isabelles Funktionen zu erleichtern.

Wenn Isabelle die notwendige Terminierung nicht automatisch beweisen kann, kann der Benutzer eine Annotation bereitstellen, die eine wohlgegründete Massrelations definiert. Dies hilft, die Beziehung zwischen den rekursiven Aufrufen zu etablieren und sicherzustellen, dass die Übersetzung erfolgreich ist.

Während der Übersetzung überprüft das Tool die Annotation, um sicherzustellen, dass sie korrekt definiert ist. Dieser Prozess beinhaltet die Übersetzung der Annotationen in Isabelle-Definitionen, um den Beweis der Terminierung zu unterstützen.

Die Übersetzungsstrategie verlangt auch, dass VDM-Überprüfungen ausdrücklich als Prädikate angegeben werden. Zum Beispiel müssen VDM-Mengen endlich sein, und ihre Typinvarianten müssen für jedes Element gelten.

#Rekursion über VDM Grundtypen

Für grundlegende Typen wie natürliche Zahlen richtet die Übersetzungsstrategie zunächst eine Vorbedingung ein, die darauf besteht, dass der Parameter ein gültiger Typ ist. Als nächstes definieren wir die rekursive Funktion, die einen undefinierten Wert zurückgibt, wenn die Vorbedingung fehlschlägt. Die Beweise für die Kompatibilität und Vollständigkeit der Muster werden dann nach den Standardmethoden von Isabelle etabliert.

Die Wohlgegründetheit der Rekursion kann oft unter Verwendung der bestehenden Maschinen von Isabelle hergestellt werden, was den Prozess reibungsloser macht. Wir definieren auch neue Lemmata, um bei der Beweissuche zu helfen, was die Last für den Benutzer verringert.

#Rekursion über VDM Mengen

Der nächste Schritt in der Übersetzungsstrategie besteht darin, VDM-Mengen zu behandeln. Ein häufiges Beispiel ist eine Funktion, die die Elemente einer Menge summiert. Die Funktion prüft, ob die Menge leer ist, bevor sie mit der Summe fortfährt, und wählt ein beliebiges Element, das in der Rekursion verwendet wird.

Wir definieren eine Vorbedingung für die Funktion, die sicherstellt, dass die Menge nur gültige Zahlen enthält und endlich ist. Wie bei den grundlegenden Typen stellen wir die rekursive Funktion in Isabelle auf und überprüfen die Vorbedingung, bevor wir die Summe ausführen.

Die Massrelation muss die beteiligten Prozesse widerspiegeln, und Isabelles Werkzeuge können verwendet werden, um die Wohlgegründetheit der Relation zu validieren. Der Terminierungsbeweis basiert ebenfalls auf vorherigen Vorbedingungen und Filterbedingungen.

#Rekursion über VDM Karten

Rekursion über Karten ist ähnlich wie Rekursion über Mengen. Eine Funktion, die die Werte einer Karte summiert, verwendet ähnliche Techniken, indem sie überprüft, ob die Karte leer ist, und, wenn nicht, einen Schlüssel auswählt, um den damit verbundenen Wert zu summieren.

Wie zuvor stellen die Vorbedingungen sicher, dass sowohl der Bereich als auch der Wertebereich der Karte die notwendigen Eigenschaften erfüllen. Der Übersetzungsprozess überprüft die Kernbedingungen für Wohlgegründetheit und konstruiert die geeignete Massrelation, um den Terminierungsbeweis zu unterstützen.

#Rekursion mit komplexen Massnahmen

Wir können denselben Übersetzungsansatz auch auf komplexere rekursive Definitionen anwenden. Diese Definitionen erfordern jedoch oft, dass Benutzer detailliertere Annotationen und zusätzliche Lemmata bereitstellen, um den Beweisprozess zu unterstützen.

Betrachten wir zum Beispiel die bekannte Ackermann-Funktion, die für ihre komplexe Rekursion bekannt ist. Die Funktion erfordert, dass beide Parameter auf eine bestimmte Weise verarbeitet werden, was zusätzliche Massnahmen bedeutet, die in VDM definiert werden müssen. Benutzer müssen Annotationen bereitstellen, um Isabelle zu helfen, die Beziehungen zwischen den rekursiven Aufrufen korrekt abzuleiten.

Die in der VDM-Version verwendeten Massnahmen unterscheiden sich von den typischerweise in Isabelle gesehenen, daher ist es wichtig, eine klare Verbindung zwischen beiden herzustellen, damit die Übersetzung funktioniert.

#Schwierige Beispiele

Einige Beispiele sind herausfordernder und erfordern eine ausgefeiltere Einrichtung für den Beweis. Zum Beispiel zeigt die Permutationsfunktion, wie sie zwischen abnehmenden Parametern vertauschen kann, und die Takeuchi-Funktion demonstriert innere Rekursion.

Diese komplexen Beispiele offenbaren oft, wie Beweis Systeme in ihren Anforderungen unterschiedlich sein können. Benutzer müssen spezifische Massnahmen bereitstellen und oft manuelle Eingriffe vornehmen, um Isabelle bei der Erstellung der notwendigen Beweise zu unterstützen.

#Gegenseitige Rekursion

Schliesslich berücksichtigt die Übersetzung auch die gegenseitige Rekursion, bei der VDM Definitionen erlaubt, die einander aufrufen. Wir können Algorithmen aus VDMs Typprüfer verwenden, um diese Beziehungen zu identifizieren und die notwendigen Massnahmen abzuleiten.

Wenn der Rekursionsgraph nicht automatisch entdeckt werden kann, müssen Benutzer eine Annotation für eine der gegenseitig rekursiven Definitionen bereitstellen, um die erwarteten Funktionsnamen anzugeben.

Im Grunde erfordert diese Interaktion, dass alle verwandten Funktionen zusammen definiert werden, um eine ordnungsgemässe Verknüpfung in der Beweis Einrichtung sicherzustellen.

#Fazit

Dieser Artikel hat eine Methode zur Übersetzung rekursiver Funktionen von VDM nach Isabelle/HOL skizziert, die sich auf grundlegende Typen, Mengen, Karten und gegenseitige Rekursion konzentriert. Die besprochenen Strategien erlauben eine Vielzahl von rekursiven Definitionen, einschliesslich komplexer Beispiele, die zusätzliche Massnahmen und Benutzerinteraktionen erfordern.

Während wir diese Übersetzungsstrategie weiter verfeinern, wird sie ein wertvolles Werkzeug für Benutzer darstellen, die ihre VDM-Definitionen nach Isabelle/HOL konvertieren müssen, während sie die Korrektheit und Terminierung ihrer rekursiven Funktionen sicherstellen. Zukünftige Arbeiten beinhalten die weiterführende Implementierung dieser Strategien in bestehenden Tools, um die Benutzerfreundlichkeit und Automatisierung für Benutzer zu verbessern.