Page Content
Publications
| 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 |
Zusatzinformationen / Extras
Quick Access:
Schnellnavigation zur Seite über Nummerneingabe