/ en / Traditional / mobile

Beats Biblionetz - Texte

Programmieren und Beweisen

Experimente mit dem Programmverifizierer NPPV
H. Peter Gumm
Publikationsdatum:
Zu finden in: Informatik und Schule (Seite 94 bis 107), 1999     
Erste Seite des Textes (PDF-Thumbnail)

iconZusammenfassungen

Anhand von Fallbeispielen zeigen wir den Einsatz unseres Programmverifizierers NPPV für abstrakte Fragestellungen zwischen Mathematik und Informatik. Aus einem gegebenen und mit Invarianten annotierten Programmschema erzeugt das System automatisch logische Bedingungen für dessen Korrektheit.

Der Verifizierer wurde zum Einsatz im Informatikunterricht konzipiert. Er nimmt dem Benutzer die immer wiederkehrende Berechnung trivialer Verifikationsbedingungen ab und richtet die Aufmerksamkeit und die Kreativität auf das Wesentliche - aussagekräftige Invarianten, Axiome der verwendeten Datenstrukturen, Existenz von Funktionen mit bestimmten Eigenschaften.

Der Schwerpunkt liegt auf der Verifikation abstrakter Programme (Pro-grammschemata), z.B. zur Transformation zwischen rekursiven und ite-rativen Programmen. Selbst die Äquivalenz zwischen einem abstrakten Induktionsbeweis und der Verifikation eines Programmes, welches ein Gegenbeispiel zur Behauptung sucht, läßt sich mit NPPV interaktiv er-kunden.

im Konferenz-Band Informatik und Schule im Text Programmieren und Beweisen (1999)

iconDieses Kapitel erwähnt...

iconDieses Kapitel erwähnt nicht... Eine statistisch erstelle Liste von nicht erwähnten (oder zumindest nicht erfassten) Begriffen, die aufgrund der erwähnten Begriffe eine hohe Wahrscheinlichkeit aufweisen, erwähnt zu werden.

icon
Nicht erwähnte Begriffe
Informatik-Didaktik

iconTagcloud

iconAnderswo finden

icon

iconVolltext dieses Dokuments

LokalAuf dem WWW Programmieren und Beweisen Experimente mit dem Programmverifizierer NPPV: Artikel als Volltext bei Springerlink (lokal: PDF, 1533 kByte; WWW: Link OK )

iconAnderswo suchen Auch im Biblionetz finden Sie nicht alles. Aus diesem Grund bietet das Biblionetz bereits ausgefüllte Suchformulare für verschiedene Suchdienste an. Biblionetztreffer werden dabei ausgeschlossen.

iconBiblionetz-History Dies ist eine graphische Darstellung, wann wie viele Verweise von und zu diesem Objekt ins Biblionetz eingetragen wurden und wie oft die Seite abgerufen wurde.