Abstraktion und Wiederverwendung von formalen Programmentwicklungen

• Applicant: Professor Dr. Christoph Lüth
• Subject Area: Software Engineering and Programming Languages
• Term: from 2000 to 2010
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Research Grants
• Participating Person: Professor Dr. Bernd Krieg-Brückner