LOPEX - Konstruktion logikgestützter Programmierumgebungen aus formalen Sprachbeschreibungen

This page contains information about Logic-based Programming Environments Constructed from Formal Language Specifications, LOPEX for short.

Members

  • Prof. Dr. Arnd Poetzsch-Heffter, TU Kaiserslautern, AG Softwaretechnik

Abstract

General Aims

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.

Realization

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 (Synthesizer 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 angepassten Hoare-Logik Beweisverpflichtungen generiert und an einen Beweiser weitergereicht.

Als Beweiser können gängige Systeme wie PVS oder Isabelle/HOL 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.

Researchers in AG Softech

  • Prof. Dr. Arnd Poetzsch-Heffter
  • Dipl.-Inform. Peter Müller
  • Dipl.-Inform. Jörg Meyer

Funding

Completion Status

This project is completed.