/ 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...


Begriffe
KB IB clear
Programmierenprogramming

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.

Verweise auf dieses Kapitel 1
Verweise von diesem Kapitel 11
2005200620072008200920102011201220132014201520162017