FoPras und Diplomarbeiten
The same information in English
LOPEX steht für Logic-based Programming Environments Constructed from Formal Language Specifications.
Zielsetzung
Neben den klassischen, meist syntaxorientierten Fähigkeiten sollen Programmierumgebungen in Zukunft Spezifikations- und Verifikationsunterstützung leisten. Dazu müssen sie die Spezifikation von Modulschnittstellen in die Programmbearbeitung integrieren und benutzerfreundliche Beweiswerkzeuge anbieten. Ohne eine solche Logikunterstützung wird der Korrektheitsnachweis umfangreicher, realistischer Programme auch in Zukunft zu aufwendig und unwirtschaftlich bleiben.
In diesem Projekt sollen generative Konstruktionstechniken für derartige logikgestützte Programmierumgebungen entwickelt werden. Ein Projektschwerpunkt ist es, mit Hilfe dieser Techniken eine prototypische logikgestützte Programmierumgebung für eine objektorientierte Sprache zu konstruieren.
Durchführung
In der ersten Phase des LOPEX-Projekts soll eine logikgestützte Programmierumgebung für die Sprache Java entwickelt werden. Diese besteht aus einem Annotierungseditor, einem Beweiser und einer Verwaltungskomponente.
Der Annotierungseditor ermöglicht die Erstellung von Java-Programmen und deren Anreicherung um sog. Annotationen (Vor- und Nachbedingungen von Methoden sowie Klasseninvarianten). Der Editor soll mit einem Werkzeug zur Generierung von Struktureditoren ( Sythesizer Generator) realisiert werden.
Zur Spezifikation der Programme wird eine Annotationssprache eingesetzt. Sie ermöglicht eine deklarative Beschreibung von Programmeigenschaften durch Angabe von Vor- und Nachbedingungen für Methoden und von Klasseninvarianten. Die Annotationssprache erlaubt insbesondere Datenabstraktion und die Modulierung von sharing-Eigenschaften, wie sie bei der Programmierung mit Verweisen auftreten.
Auch die Durchführung der Korrektheitsbeweise erfolgt überwiegend im Annotierungseditor. Dazu werden aus den Annotationen unter Anwendung einer erweiterten und an unsere Bedürfnisse angepaßten Hoare-Logik Beweisverpflichtungen generiert und an einen Beweiser weitergereicht.
Als Beweiser können gängige Systeme wie PVS oder HOL Isabelle eingesetzt werden. Sie erlauben die Spezifikation abstrakter Datentypen und erleichtern den Beweis programmunabhängiger Lemmata.
Die Verwaltungskomponente dient schließlich der Organisation der verschiedenen Bestandteile eines verifizierten Programms. Hierzu zählen z.B. Programmtext, Annotationen, abstrakte Datentypen und Beweise.
Sie sind der . Besucher dieser Seite seit dem 29. Oktober 1996.