direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Page Content

Publications

Structural Simulation Proofs based on ASMs even for Non-Terminating Programs
Citation key GlesnerZimmermannASM2001
Author Sabine Glesner and Wolf Zimmermann
Title of Book Proceedings of the ASM-Workshop, Eight International Conference on Computer Aided Systems Theory EUROCAST 2001
Pages 235-238
Year 2001
Address IUCTC Universidad de Las Palmas de Gran Canaria, Spain
Abstract Beim Transformieren von Programmen, wie z.B. in Übersetzern, muss man häufig deren Semantik erhalten. Um eine solche Anforderung formal zu garantieren, sind formale Beweise erforderlich. Man will deshalb Simulationsbeweise durchführen, die zeigen, dass die Zustandsübergänge, die im ursprünglichen Programm durchlaufen werden, dieselben sind wie im transformierten Programm. In einem ersten Anlauf könnte man versuchen, das durch einen induktiven Beweis über die Anzahl der Zustandsübergänge nachzuweisen. Aber dieser Ansatz ist, wie wir hier zeigen, im allgemeinen Fall nicht anwendbar. Denn Induktion ist nur solange anwendbar, wie die betrachteten Programme terminieren. Für nicht-terminierende Programme brauchen wir koinduktive Beweistechniken, mit denen derartige Simulationsbeweise leicht geführt werden können.
Bibtex Type of Publication Conference Article
Download Bibtex entry

Zusatzinformationen / Extras

Quick Access:

Schnellnavigation zur Seite über Nummerneingabe