Abstraktion und Wiederverwendung von formalen Programmentwicklungen

• Antragsteller: Professor Dr. Christoph Lüth
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung von 2000 bis 2010
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5253630

Zur Entwicklung korrekter Programme aus einer Spezifikation sind eine Vielzahl von formalen Methoden entwickelt worden. Mit dem beantragten Projekt wird ein bislang ungenutztes Potential der formalen Methoden erschlossen: die Wiederverwendung und Abstraktion von Entwicklungen. Weil eine formale Entwicklung wie die Entwicklung eines Programmes aus einer Spezifikation oder der Beweis bestimmter Eigenschaften eines Programmes selbst ein formales Objekt ist, können wir Wiederverwendung und Verallgemeinerung von Entwicklungen formal beschreiben. Durch die Wiederverwendung der Entwicklung wird der gesamte Entwicklungsprozess wiederverwendet, wodurch eine größere Mächtigkeit als bei der Wiederverwendung des Produktes erreicht wird. Zentraler Bestandteil des Projektes ist die Implementierung der entwickelten Konzepte auf der Basis des modernen Theorembeweisers "Isabelle". Wichtig hierbei ist der Aspekt der Generizität: Die Konzepte zur Wiederverwendung und Abstraktion sollen nicht nur in einer speziellen formalen Methode betrachtet werden, sondern für jede formale Methode angewandt werden können.

• DFG-Verfahren: Sachbeihilfen
• Beteiligte Person: Professor Dr. Bernd Krieg-Brückner