/ en / Traditional / help

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  local web 
Erste Seite des Textes (PDF-Thumbnail)
Diese Seite wurde seit 6 Jahren inhaltlich nicht mehr aktualisiert. Unter Umständen ist sie nicht mehr aktuell.

iconZusammenfassungen

Informatik und Schule

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 vermutlich 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

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

iconBeat und dieses Kapitel

Beat war Co-Leiter des ICT-Kompetenzzentrums TOP während er Dieses Kapitel ins Biblionetz aufgenommen hat. Die bisher letzte Bearbeitung erfolgte während seiner Zeit am Institut für Medien und Schule. Beat besitzt kein physisches, aber ein digitales Exemplar. Eine digitale Version ist auf dem Internet verfügbar (s.o.). Aufgrund der wenigen Einträge im Biblionetz scheint er es nicht wirklich gelesen zu haben. Es gibt bisher auch nur wenige Objekte im Biblionetz, die dieses Werk zitieren.

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.