Abstraktion und Wiederverwendung von formalen Programmentwicklungen

点击翻译按钮获取中文摘要

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.