Algebraische Gesetze aus Imperativen Programmen

08.12.98


Zum Starten hier klicken


Inhaltsverzeichnis

Algebraische Gesetze aus Imperativen Programmen

Elemente eines Programmes

Elemente eines Programmes

Elemente eines Programmes

Elemente eines Programmes

Datenstrukturen

Datenstrukturen

Bedingte Gleichungen

Bedingte Gleichungen

Programme beschreiben Zustandstransformationen

Programme beschreiben Zustandstransformationen

Programme beschreiben Zustandstransformationen

Programm als Zustandstransformation

Programm als Zustandstransformation

Elementare Programme

Elementare Programme

Elementare Programme

Elementare Programme

Elementare Programme

Kontrollstrukturen

Kontrollstrukturen

Kontrollstrukturen

Kontrollstrukturen

Algorithm = Data Structure + Control

Algorithm = Data Structure + Control

Spezifikationen

Partial correctness assertions

Regel für “;”

Regel für “;”

Regel für “;”

Regel für “;”

Regel für “;”

Regel für “;”

Rückwärts-Beweis

Rückwärts-Beweis

Rückwärts-Beweis

Rückwärts-Beweis

Schleifenregel

Schleifenregel

Schleifenregel

Schleifenregel

Schleifenregel

Zuweisungsregel

Zuweisungsregel

Zuweisungsregel

Zuweisungsregel

Zuweisungsregel

Zuweisungsregel

Beweis eines Programms

Beweis eines Programms

Beweis eines Programms

Beweis eines Programms

Beweis eines Programms

Beweis eines Programms

Beweis eines Programms

Beweis eines Programms

Beweis eines Programms

Zuweisungsregel

Zuweisungsregel

Programm Verifizerer

New Paltz Program Verifier

New Paltz Program Verifier

New Paltz Program Verifier

New Paltz Program Verifier

New Paltz Program Verifier

Terminierung

Terminierung

Variablenvertauschung

Variablenvertauschung

Variablenvertauschung

Variablenvertauschung

Variablenvertauschung

Data structure = Algorithm - Control

Data structure = Algorithm - Control

Data structure = Algorithm - Control

Data structure = Algorithm - Control

Abstrakte Programme

Abstrakte Programme

Abstrakte Programme

Abstrakte Programme

Lineare Rekursion

Lineare Rekursion

Lineare Rekursion

Lineare Rekursion

Nachweis der Unvollständigkeit

Nachweis der Unvollständigkeit

Wand's Beispiel

Wand's Beispiel

Wand's Beispiel

Wand's Beispiel

Wand's Beispiel

Wand's Beispiel

Dicke und dünne Mengen

Dicke und dünne Mengen

Dicke und dünne Mengen

Dicke und dünne Mengen

Quantoren Elimination

Quantoren Elimination

Quantoren Elimination

Quantoren Elimination

Programmieren = Beweisen

Programmieren = Beweisen

Programmieren = Beweisen

Programmieren = Beweisen

Programmieren = Beweisen

Programmieren = Beweisen

Programmieren = Beweisen

Autor:H.Peter Gumm

E-Mail: gumm@mathematik.uni-marburg.de

Homepage: www.mathematik.uni-marburg.de/~gumm